Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

refactor(CategoryTheory/SmallObject): generalization of the definitions #20256

Open
wants to merge 43 commits into
base: master
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
43 commits
Select commit Hold shift + click to select a range
b5c4880
feat(CategoryTheory/SmallObject): very basic API for the iteration of…
joelriou Oct 23, 2024
73f3517
feat(CategoryTheory/SmallObject): construction of a morphism between …
joelriou Oct 23, 2024
9a2e020
Update Mathlib.lean
joelriou Oct 23, 2024
f497043
fix Mathlib.lean
joelriou Oct 23, 2024
46bf440
feat(CategoryTheory/SmallObject/Iteration): the unique morphism (limi…
joelriou Oct 23, 2024
ba501fa
Merge remote-tracking branch 'origin' into small-object-4
joelriou Oct 26, 2024
295d8df
fixes, using interval notation
joelriou Oct 26, 2024
8d33372
Merge remote-tracking branch 'origin/small-object-4' into small-object-5
joelriou Oct 26, 2024
26405bd
fix
joelriou Oct 26, 2024
c60220e
Merge remote-tracking branch 'origin/small-object-5' into small-object-6
joelriou Oct 26, 2024
ecdbc60
Update Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
joelriou Oct 27, 2024
0ed84bf
Merge remote-tracking branch 'origin' into small-object-5
joelriou Oct 27, 2024
9a446f2
Merge remote-tracking branch 'origin/small-object-5' into small-object-6
joelriou Oct 27, 2024
64c0674
fix
joelriou Oct 27, 2024
6d4fc10
fix
joelriou Oct 27, 2024
bb49cdf
Merge remote-tracking branch 'origin/small-object-5' into small-object-6
joelriou Oct 27, 2024
3d76917
Merge remote-tracking branch 'origin' into small-object-6
joelriou Nov 12, 2024
f8a7628
s/refine/exact/
joelriou Nov 12, 2024
3398597
wip
joelriou Nov 14, 2024
322c0f1
Merge remote-tracking branch 'origin' into small-object-7
joelriou Nov 19, 2024
95f5310
cleaning up
joelriou Nov 19, 2024
943044b
fixing imports
joelriou Nov 19, 2024
638cb34
wip
joelriou Nov 19, 2024
659a203
wip
joelriou Nov 19, 2024
e6b64b3
Merge remote-tracking branch 'origin' into small-object-8
joelriou Nov 20, 2024
b394a49
wip
joelriou Nov 20, 2024
9c6f1e6
fixed Mathlib.lean
joelriou Nov 20, 2024
7318f01
cleaning up
joelriou Nov 20, 2024
c3bdd8f
Merge remote-tracking branch 'origin' into small-object-8
joelriou Nov 30, 2024
1b87f3e
added functorofcocone
joelriou Nov 30, 2024
95eb0cb
Merge remote-tracking branch 'origin' into small-object-functor-of-co…
joelriou Dec 20, 2024
ae206be
Merge remote-tracking branch 'origin/small-object-functor-of-cocone' …
joelriou Dec 20, 2024
e0a256f
Update Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
joelriou Dec 20, 2024
4ff2995
Merge remote-tracking branch 'origin' into small-object-8
joelriou Dec 21, 2024
fabd79f
fix docstrings
joelriou Dec 21, 2024
7f28baf
Merge remote-tracking branch 'origin' into small-object-8
joelriou Dec 24, 2024
eeb1167
Merge remote-tracking branch 'origin' into small-object-8
joelriou Dec 25, 2024
0a5f49b
wip
joelriou Dec 26, 2024
faf9569
refactor(CategoryTheory/SmallObject): better definitions
joelriou Dec 26, 2024
6a3aed8
removed unused file
joelriou Dec 26, 2024
64dcaa1
fix
joelriou Dec 26, 2024
b429049
better docstring
joelriou Dec 26, 2024
6e71693
Update Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
joelriou Dec 26, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Mathlib.lean
Original file line number Diff line number Diff line change
Expand Up @@ -2178,8 +2178,8 @@ import Mathlib.CategoryTheory.SmallObject.Construction
import Mathlib.CategoryTheory.SmallObject.Iteration.Basic
import Mathlib.CategoryTheory.SmallObject.Iteration.ExtendToSucc
import Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
import Mathlib.CategoryTheory.SmallObject.Iteration.Iteration
import Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
import Mathlib.CategoryTheory.SmallObject.Iteration.UniqueHom
import Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
import Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
import Mathlib.CategoryTheory.Square
Expand Down
Loading
Loading