ColimitsOfShape

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

Statistics

Metric	Count
Definitions ClosedUnderColimitsOfShape, ColimitOfShape, colimit, ofIso, ofLE, reindex, toColimitPresentation, toCostructuredArrow, IsClosedUnderColimitsOfShape, colimitsOfShape, strictColimitsOfShape	11
Theorems colimit, closedUnderColimitsOfShape_of_colimit, colimit_toColimitPresentation, colimitsOfShape, ofIso_toColimitPresentation, ofLE_toColimitPresentation, prop, prop_diag_obj, reindex_toColimitPresentation, toCostructuredArrow_map, toCostructuredArrow_obj, colimitsOfShape_le, inverseImage, mk', of_equivalence, colimitsOfShape_congr, colimitsOfShape_eq_unop_limitsOfShape, colimitsOfShape_isoClosure, colimitsOfShape_le_of_final, colimitsOfShape_monotone, colimitsOfShape_op, instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape, instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape_1, instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite, instIsClosedUnderColimitsOfShapeUnopOppositeOfIsClosedUnderLimitsOfShape, instIsClosedUnderIsomorphismsColimitsOfShape, instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape, instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape_1, instIsClosedUnderLimitsOfShapeUnopOfIsClosedUnderColimitsOfShapeOpposite, instIsClosedUnderLimitsOfShapeUnopOppositeOfIsClosedUnderColimitsOfShape, instIsStableUnderRetractsOfIsClosedUnderColimitsOfShapeWalkingParallelPair, instSmallStrictColimitsOfShapeOfSmallOfLocallySmall, isClosedUnderColimitsOfShape_iff, isClosedUnderColimitsOfShape_iff_of_equivalence, isClosedUnderColimitsOfShape_iff_op, isClosedUnderColimitsOfShape_iff_unop, isClosedUnderColimitsOfShape_inverseImage_iff, isClosedUnderColimitsOfShape_op_iff_op, isClosedUnderColimitsOfShape_op_iff_unop, isClosedUnderLimitsOfShape_iff_op, isClosedUnderLimitsOfShape_iff_unop, isClosedUnderLimitsOfShape_op_iff_op, isClosedUnderLimitsOfShape_op_iff_unop, isoClosure_strictColimitsOfShape, limitsOfShape_eq_unop_colimitsOfShape, limitsOfShape_op, prop_colimit, prop_of_isColimit, strictColimitsOfShape_le_colimitsOfShape, strictColimitsOfShape_monotone	50
Total	61

CategoryTheory.Limits

Definitions

Name	Category	Theorems
ClosedUnderColimitsOfShape 📖	MathDef	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
closedUnderColimitsOfShape_of_colimit 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.ObjectProperty.strictColimitsOfShape	CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape	—	CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.mk'

CategoryTheory.Limits.ClosedUnderColimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimit 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Limits.colimit	—	CategoryTheory.ObjectProperty.prop_colimit

CategoryTheory.ObjectProperty

Definitions

Name	Category	Theorems
ColimitOfShape 📖	CompData	—
IsClosedUnderColimitsOfShape 📖	CompData	32 math math: isClosedUnderColimitsOfShape_iff_op, instIsClosedUnderColimitsOfShapeColimitsClosure, instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape, IsClosedUnderColimitsOfShape.of_equivalence, instIsClosedUnderColimitsOfShapeUnopOppositeOfIsClosedUnderLimitsOfShape, isClosedUnderLimitsOfShape_op_iff_unop, instIsClosedUnderColimitsOfShapeColimitsCardinalClosureCategoryFamily, CategoryTheory.Limits.closedUnderColimitsOfShape_of_colimit, CategoryTheory.NatTrans.instIsClosedUnderColimitsOfShapeUnderFunctorCoequifiberedHomDiscretePUnitOfHasProductsOfShapeHom, instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite, isClosedUnderColimitsOfShape_iff, isClosedUnderColimitsOfShape_op_iff_unop, isClosedUnderColimitsOfShape_of_preservesColimitsOfShape_ι, CategoryTheory.Limits.instIsClosedUnderColimitsOfShapeEssImageOfHasColimitsOfShapeOfPreservesColimitsOfShapeOfFullOfFaithful, IsClosedUnderColimitsOfShape.inverseImage, instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape_1, isClosedUnderColimitsOfShape_iff_of_equivalence, isClosedUnderColimitsOfShape_op_iff_op, isClosedUnderLimitsOfShape_op_iff_op, isClosedUnderColimitsOfShape_colimitsCardinalClosure, isClosedUnderColimitsOfShape_iff_unop, CategoryTheory.CostructuredArrow.isClosedUnderColimitsOfShape, CategoryTheory.isClosedUnderColimitsOfShape_isCardinalPresentable, isClosedUnderColimitsOfShape_inverseImage_iff, CategoryTheory.MorphismProperty.isClosedUnderColimitsOfShape_isLocal, IsClosedUnderColimitsOfShape.mk', instIsClosedUnderColimitsOfShapeFunctorPreservesFiniteLimitsOfHasExactColimitsOfShape, CategoryTheory.MorphismProperty.instIsClosedUnderColimitsOfShapeIsColocal, isClosedUnderLimitsOfShape_iff_unop, isClosedUnderLimitsOfShape_iff_op, instIsClosedUnderColimitsOfShapeFunctorPreservesLimitsOfShapeOfPreservesLimitsOfShapeColim, CategoryTheory.instIsClosedUnderColimitsOfShapeFunctorOppositeTypeIsIndObjectOfIsFiltered
colimitsOfShape 📖	CompOp	15 math math: colimitsOfShape_op, instIsClosedUnderIsomorphismsColimitsOfShape, IsClosedUnderColimitsOfShape.colimitsOfShape_le, limitsOfShape_op, colimitsOfShape_le_of_final, colimitsOfShape_isoClosure, isoClosure_strictColimitsOfShape, isClosedUnderColimitsOfShape_iff, limitsOfShape_eq_unop_colimitsOfShape, colimitsOfShape_monotone, ColimitOfShape.colimitsOfShape, IsCardinalFilteredGenerator.exists_colimitsOfShape, colimitsOfShape_eq_unop_limitsOfShape, strictColimitsOfShape_le_colimitsOfShape, colimitsOfShape_congr
strictColimitsOfShape 📖	CompData	4 math math: strictColimitsOfShape_monotone, isoClosure_strictColimitsOfShape, instSmallStrictColimitsOfShapeOfSmallOfLocallySmall, strictColimitsOfShape_le_colimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitsOfShape_congr 📖	mathematical	—	colimitsOfShape	—	le_antisymm colimitsOfShape_le_of_final CategoryTheory.Functor.final_of_isRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Equivalence.isEquivalence_functor
colimitsOfShape_eq_unop_limitsOfShape 📖	mathematical	—	colimitsOfShape unop CategoryTheory.Category.toCategoryStruct limitsOfShape Opposite CategoryTheory.Category.opposite op	—	ColimitOfShape.prop_diag_obj LimitOfShape.prop_diag_obj
colimitsOfShape_isoClosure 📖	mathematical	—	colimitsOfShape isoClosure	—	le_antisymm ColimitOfShape.prop_diag_obj colimitsOfShape_monotone le_isoClosure
colimitsOfShape_le_of_final 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le colimitsOfShape	—	—
colimitsOfShape_monotone 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	colimitsOfShape	—	—
colimitsOfShape_op 📖	mathematical	—	colimitsOfShape Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct limitsOfShape	—	limitsOfShape_eq_unop_colimitsOfShape op_unop colimitsOfShape_congr
instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape 📖	mathematical	—	IsClosedUnderColimitsOfShape Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	isClosedUnderLimitsOfShape_iff_op
instIsClosedUnderColimitsOfShapeOppositeOpOfIsClosedUnderLimitsOfShape_1 📖	mathematical	—	IsClosedUnderColimitsOfShape Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	isClosedUnderLimitsOfShape_op_iff_op
instIsClosedUnderColimitsOfShapeUnopOfIsClosedUnderLimitsOfShapeOpposite 📖	mathematical	—	IsClosedUnderColimitsOfShape unop CategoryTheory.Category.toCategoryStruct	—	isClosedUnderLimitsOfShape_op_iff_unop
instIsClosedUnderColimitsOfShapeUnopOppositeOfIsClosedUnderLimitsOfShape 📖	mathematical	—	IsClosedUnderColimitsOfShape unop CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite	—	isClosedUnderLimitsOfShape_iff_unop
instIsClosedUnderIsomorphismsColimitsOfShape 📖	mathematical	—	IsClosedUnderIsomorphisms colimitsOfShape	—	—
instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape 📖	mathematical	—	IsClosedUnderLimitsOfShape Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_iff_op
instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape_1 📖	mathematical	—	IsClosedUnderLimitsOfShape Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_op_iff_op
instIsClosedUnderLimitsOfShapeUnopOfIsClosedUnderColimitsOfShapeOpposite 📖	mathematical	—	IsClosedUnderLimitsOfShape unop CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_op_iff_unop
instIsClosedUnderLimitsOfShapeUnopOppositeOfIsClosedUnderColimitsOfShape 📖	mathematical	—	IsClosedUnderLimitsOfShape unop CategoryTheory.Category.toCategoryStruct Opposite CategoryTheory.Category.opposite	—	isClosedUnderColimitsOfShape_iff_unop
instIsStableUnderRetractsOfIsClosedUnderColimitsOfShapeWalkingParallelPair 📖	mathematical	—	IsStableUnderRetracts	—	CategoryTheory.Category.assoc CategoryTheory.Retract.retract CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.Cofork.condition CategoryTheory.Retract.retract_assoc prop_of_isColimit
instSmallStrictColimitsOfShapeOfSmallOfLocallySmall 📖	mathematical	—	Small strictColimitsOfShape	—	small_of_surjective small_subtype CategoryTheory.instSmallFunctorOfLocallySmall instSmallFullSubcategoryOfSmall CategoryTheory.locallySmall_fullSubcategory FullSubcategory.property
isClosedUnderColimitsOfShape_iff 📖	mathematical	—	IsClosedUnderColimitsOfShape CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le colimitsOfShape	—	—
isClosedUnderColimitsOfShape_iff_of_equivalence 📖	mathematical	—	IsClosedUnderColimitsOfShape	—	colimitsOfShape_congr
isClosedUnderColimitsOfShape_iff_op 📖	mathematical	—	IsClosedUnderColimitsOfShape IsClosedUnderLimitsOfShape Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_iff isClosedUnderLimitsOfShape_iff colimitsOfShape_eq_unop_limitsOfShape op_monotone_iff op_unop
isClosedUnderColimitsOfShape_iff_unop 📖	mathematical	—	IsClosedUnderColimitsOfShape Opposite CategoryTheory.Category.opposite IsClosedUnderLimitsOfShape unop CategoryTheory.Category.toCategoryStruct	—	isClosedUnderLimitsOfShape_op_iff_op
isClosedUnderColimitsOfShape_inverseImage_iff 📖	mathematical	—	IsClosedUnderColimitsOfShape inverseImage CategoryTheory.Equivalence.functor	—	prop_iff_of_iso IsClosedUnderColimitsOfShape.inverseImage CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Equivalence.isEquivalence_inverse CategoryTheory.Equivalence.isEquivalence_functor
isClosedUnderColimitsOfShape_op_iff_op 📖	mathematical	—	IsClosedUnderColimitsOfShape Opposite CategoryTheory.Category.opposite IsClosedUnderLimitsOfShape op CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_iff isClosedUnderLimitsOfShape_iff limitsOfShape_op op_monotone_iff
isClosedUnderColimitsOfShape_op_iff_unop 📖	mathematical	—	IsClosedUnderColimitsOfShape Opposite CategoryTheory.Category.opposite IsClosedUnderLimitsOfShape unop CategoryTheory.Category.toCategoryStruct	—	isClosedUnderLimitsOfShape_iff_op
isClosedUnderLimitsOfShape_iff_op 📖	mathematical	—	IsClosedUnderLimitsOfShape IsClosedUnderColimitsOfShape Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_iff isClosedUnderLimitsOfShape_iff limitsOfShape_eq_unop_colimitsOfShape op_monotone_iff op_unop
isClosedUnderLimitsOfShape_iff_unop 📖	mathematical	—	IsClosedUnderLimitsOfShape Opposite CategoryTheory.Category.opposite IsClosedUnderColimitsOfShape unop CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_op_iff_op
isClosedUnderLimitsOfShape_op_iff_op 📖	mathematical	—	IsClosedUnderLimitsOfShape Opposite CategoryTheory.Category.opposite IsClosedUnderColimitsOfShape op CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_iff isClosedUnderLimitsOfShape_iff colimitsOfShape_op op_monotone_iff
isClosedUnderLimitsOfShape_op_iff_unop 📖	mathematical	—	IsClosedUnderLimitsOfShape Opposite CategoryTheory.Category.opposite IsClosedUnderColimitsOfShape unop CategoryTheory.Category.toCategoryStruct	—	isClosedUnderColimitsOfShape_iff_op
isoClosure_strictColimitsOfShape 📖	mathematical	—	isoClosure strictColimitsOfShape colimitsOfShape	—	le_antisymm isoClosure_le_iff instIsClosedUnderIsomorphismsColimitsOfShape strictColimitsOfShape_le_colimitsOfShape CategoryTheory.Limits.ColimitPresentation.hasColimit ColimitOfShape.prop_diag_obj
limitsOfShape_eq_unop_colimitsOfShape 📖	mathematical	—	limitsOfShape unop CategoryTheory.Category.toCategoryStruct colimitsOfShape Opposite CategoryTheory.Category.opposite op	—	LimitOfShape.prop_diag_obj ColimitOfShape.prop_diag_obj
limitsOfShape_op 📖	mathematical	—	limitsOfShape Opposite CategoryTheory.Category.opposite op CategoryTheory.Category.toCategoryStruct colimitsOfShape	—	colimitsOfShape_eq_unop_limitsOfShape op_unop limitsOfShape_congr
prop_colimit 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Limits.colimit	—	prop_of_isColimit
prop_of_isColimit 📖	mathematical	CategoryTheory.Functor.obj	CategoryTheory.Limits.Cocone.pt	—	IsClosedUnderColimitsOfShape.colimitsOfShape_le
strictColimitsOfShape_le_colimitsOfShape 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le strictColimitsOfShape colimitsOfShape	—	—
strictColimitsOfShape_monotone 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	strictColimitsOfShape	—	—

CategoryTheory.ObjectProperty.ColimitOfShape

Definitions

Name	Category	Theorems
colimit 📖	CompOp	1 math math: colimit_toColimitPresentation
ofIso 📖	CompOp	1 math math: ofIso_toColimitPresentation
ofLE 📖	CompOp	1 math math: ofLE_toColimitPresentation
reindex 📖	CompOp	1 math math: reindex_toColimitPresentation
toColimitPresentation 📖	CompOp	7 math math: toCostructuredArrow_obj, colimit_toColimitPresentation, prop_diag_obj, ofLE_toColimitPresentation, toCostructuredArrow_map, ofIso_toColimitPresentation, reindex_toColimitPresentation
toCostructuredArrow 📖	CompOp	3 math math: toCostructuredArrow_obj, CategoryTheory.IsCardinalAccessibleCategory.final_toCostructuredArrow, toCostructuredArrow_map

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimit_toColimitPresentation 📖	mathematical	CategoryTheory.Functor.obj	toColimitPresentation CategoryTheory.Limits.colimit colimit CategoryTheory.Limits.ColimitPresentation.colimit	—	—
colimitsOfShape 📖	mathematical	—	CategoryTheory.ObjectProperty.colimitsOfShape	—	—
ofIso_toColimitPresentation 📖	mathematical	—	toColimitPresentation ofIso CategoryTheory.Limits.ColimitPresentation.ofIso	—	—
ofLE_toColimitPresentation 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le	toColimitPresentation ofLE	—	—
prop 📖	—	—	—	—	CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.colimitsOfShape_le
prop_diag_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.Limits.ColimitPresentation.diag toColimitPresentation	—	—
reindex_toColimitPresentation 📖	mathematical	—	toColimitPresentation reindex CategoryTheory.Limits.ColimitPresentation.reindex	—	—
toCostructuredArrow_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.CostructuredArrow CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.CostructuredArrow.homMk CategoryTheory.Functor.obj CategoryTheory.Limits.ColimitPresentation.diag toColimitPresentation prop_diag_obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.ColimitPresentation.ι CategoryTheory.ObjectProperty.homMk CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit	—	prop_diag_obj
toCostructuredArrow_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.CostructuredArrow CategoryTheory.ObjectProperty.FullSubcategory CategoryTheory.ObjectProperty.FullSubcategory.category CategoryTheory.ObjectProperty.ι CategoryTheory.instCategoryCostructuredArrow toCostructuredArrow CategoryTheory.Limits.ColimitPresentation.diag toColimitPresentation prop_diag_obj CategoryTheory.NatTrans.app CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.ColimitPresentation.ι	—	—

CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitsOfShape_le 📖	mathematical	—	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.ObjectProperty.colimitsOfShape	—	—
inverseImage 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape CategoryTheory.ObjectProperty.inverseImage	—	CategoryTheory.ObjectProperty.ColimitOfShape.prop
mk' 📖	mathematical	CategoryTheory.ObjectProperty CategoryTheory.Category.toCategoryStruct Pi.hasLe Prop.le CategoryTheory.ObjectProperty.strictColimitsOfShape	CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape	—	CategoryTheory.ObjectProperty.isoClosure_eq_self CategoryTheory.ObjectProperty.isoClosure_strictColimitsOfShape CategoryTheory.ObjectProperty.monotone_isoClosure
of_equivalence 📖	mathematical	—	CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape	—	CategoryTheory.ObjectProperty.isClosedUnderColimitsOfShape_iff_of_equivalence

---

← Back to Index