ColimitsClosure

📁 Source: Mathlib/CategoryTheory/ObjectProperty/ColimitsClosure.lean

Statistics

Metric	Count
Definitions colimitClosure, colimitsClosure	2
Theorems colimitsClosure_bot, colimitsClosure_eq_self, colimitsClosure_eq_unop_limitsClosure, colimitsClosure_isoClosure, colimitsClosure_le, colimitsClosure_monotone, colimitsClosure_top, instEssentiallySmallColimitsClosureOfSmallOfLocallySmall, instIsClosedUnderColimitsOfShapeColimitClosure, instIsClosedUnderColimitsOfShapeColimitsClosure, instIsClosedUnderIsomorphismsColimitsClosure, le_colimitsClosure	12
Total	14

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
colimitClosure 📖	CompOp	1 math math: instIsClosedUnderColimitsOfShapeColimitClosure
colimitsClosure 📖	CompData	11 math math: instIsClosedUnderColimitsOfShapeColimitsClosure, instIsClosedUnderIsomorphismsColimitsClosure, colimitsClosure_bot, colimitsClosure_eq_self, colimitsClosure_isoClosure, instEssentiallySmallColimitsClosureOfSmallOfLocallySmall, le_colimitsClosure, colimitsClosure_eq_unop_limitsClosure, colimitsClosure_le, colimitsClosure_monotone, colimitsClosure_top

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitsClosure_bot 📖	mathematical	—	colimitsClosure Bot.bot CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instBotForall BooleanAlgebra.toBot Prop.instBooleanAlgebra	—	colimitsClosure_eq_self instIsClosedUnderIsomorphismsBot instIsClosedUnderColimitsOfShapeBotOfNonempty
colimitsClosure_eq_self 📖	mathematical	IsClosedUnderColimitsOfShape	colimitsClosure	—	le_antisymm colimitsClosure_le le_refl le_colimitsClosure
colimitsClosure_eq_unop_limitsClosure 📖	mathematical	—	colimitsClosure unop CategoryTheory.Category.toCategoryStruct limitsClosure Opposite CategoryTheory.Category.opposite op	—	le_antisymm colimitsClosure_le instIsClosedUnderIsomorphismsUnopOfOpposite instIsClosedUnderIsomorphismsLimitsClosure instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite instIsClosedUnderLimitsOfShapeLimitsClosure op_monotone_iff op_unop le_limitsClosure limitsClosure_le instIsClosedUnderIsomorphismsOppositeOp instIsClosedUnderIsomorphismsColimitsClosure instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape instIsClosedUnderColimitsOfShapeColimitsClosure le_colimitsClosure
colimitsClosure_isoClosure 📖	mathematical	—	colimitsClosure isoClosure	—	le_antisymm colimitsClosure_le instIsClosedUnderIsomorphismsColimitsClosure instIsClosedUnderColimitsOfShapeColimitsClosure isoClosure_le_iff le_colimitsClosure colimitsClosure_monotone le_isoClosure
colimitsClosure_le 📖	mathematical	IsClosedUnderColimitsOfShape CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le colimitsClosure	—	prop_of_iso prop_of_isColimit
colimitsClosure_monotone 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le colimitsClosure	—	colimitsClosure_le instIsClosedUnderIsomorphismsColimitsClosure instIsClosedUnderColimitsOfShapeColimitsClosure LE.le.trans le_colimitsClosure
colimitsClosure_top 📖	mathematical	—	colimitsClosure Top.top CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.instTopForall BooleanAlgebra.toTop Prop.instBooleanAlgebra	—	colimitsClosure_eq_self instIsClosedUnderIsomorphismsTop instIsClosedUnderColimitsOfShapeTop
instEssentiallySmallColimitsClosureOfSmallOfLocallySmall 📖	mathematical	Small CategoryTheory.LocallySmall	EssentiallySmall colimitsClosure	—	colimitsClosure_eq_unop_limitsClosure Opposite.small instEssentiallySmallUnopOfOpposite instEssentiallySmallLimitsClosureOfSmallOfLocallySmall instEssentiallySmallOppositeOp CategoryTheory.instLocallySmallOpposite
instIsClosedUnderColimitsOfShapeColimitClosure 📖	mathematical	—	IsClosedUnderColimitsOfShape colimitClosure	—	instIsClosedUnderColimitsOfShapeColimitsClosure
instIsClosedUnderColimitsOfShapeColimitsClosure 📖	mathematical	—	IsClosedUnderColimitsOfShape colimitsClosure	—	ColimitOfShape.prop_diag_obj
instIsClosedUnderIsomorphismsColimitsClosure 📖	mathematical	—	IsClosedUnderIsomorphisms colimitsClosure	—	—
le_colimitsClosure 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le colimitsClosure	—	—

---

← Back to Index