Commit 2024-11-13 21:29 7b4b3db9

View on Github →

feat: the category of Ind-objects (#18881)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/FullSubcategory.lean

added theorem CategoryTheory.Limits.closedUnderColimitsOfShape_of_colimit

added theorem CategoryTheory.Limits.closedUnderLimitsOfShape_of_limit

Created Mathlib/CategoryTheory/Limits/Indization/Category.lean

added def CategoryTheory.Ind

Modified Mathlib/CategoryTheory/Limits/Indization/IndObject.lean