Over

📁 Source: Mathlib/CategoryTheory/Limits/Over.lean

Statistics

Metric	Count
Definitions isColimitToOver, isLimitToOver, createsColimitsOfSize, createsColimitsOfSizeMapCompForget, isColimitLiftCocone, isColimitToOver, liftCocone, createLimitsOfSizeMapCompForget, createsLimitsOfSize, isLimitLiftCone, isLimitToUnder, liftCone	12
Theorems epi_iff_epi_left, epi_left_of_epi, hasColimit_of_hasColimit_comp_forget, instHasColimits, instHasColimitsOfShape, instHasFiniteColimits, instHasFiniteCoproducts, liftCocone_pt, liftCocone_ι_app, preservesColimitsOfSize_map, hasLimit_of_hasLimit_comp_forget, instHasLimits, instHasLimitsOfShape, liftCone_pt, liftCone_π_app, mono_iff_mono_right, mono_right_of_mono, preservesLimitsOfSize_map	18
Total	30

CategoryTheory.Limits.colimit

Definitions

Name	Category	Theorems
isColimitToOver 📖	CompOp	—

CategoryTheory.Limits.limit

Definitions

Name	Category	Theorems
isLimitToOver 📖	CompOp	—

CategoryTheory.Over

Definitions

Name	Category	Theorems
createsColimitsOfSize 📖	CompOp	—
createsColimitsOfSizeMapCompForget 📖	CompOp	—
isColimitLiftCocone 📖	CompOp	—
isColimitToOver 📖	CompOp	—
liftCocone 📖	CompOp	2 math math: liftCocone_ι_app, liftCocone_pt

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
epi_iff_epi_left 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Over CategoryTheory.instCategoryOver CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left	—	CategoryTheory.CostructuredArrow.epi_iff_epi_left CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl
epi_left_of_epi 📖	mathematical	—	CategoryTheory.Epi CategoryTheory.Comma.left CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.id CategoryTheory.Functor.fromPUnit CategoryTheory.CommaMorphism.left	—	CategoryTheory.CostructuredArrow.epi_left_of_epi CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl
hasColimit_of_hasColimit_comp_forget 📖	mathematical	—	CategoryTheory.Limits.HasColimit CategoryTheory.Over CategoryTheory.instCategoryOver	—	CategoryTheory.CostructuredArrow.hasColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Functor.instPreservesColimitsOfShapeOfIsLeftAdjoint CategoryTheory.Functor.isLeftAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl
instHasColimits 📖	mathematical	—	CategoryTheory.Limits.HasColimits CategoryTheory.Over CategoryTheory.instCategoryOver	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShapeOfHasColimitsOfSize
instHasColimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Over CategoryTheory.instCategoryOver	—	hasColimit_of_hasColimit_comp_forget CategoryTheory.Limits.hasColimitOfHasColimitsOfShape
instHasFiniteColimits 📖	mathematical	—	CategoryTheory.Limits.HasFiniteColimits CategoryTheory.Over CategoryTheory.instCategoryOver	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits
instHasFiniteCoproducts 📖	mathematical	—	CategoryTheory.Limits.HasFiniteCoproducts CategoryTheory.Over CategoryTheory.instCategoryOver	—	instHasColimitsOfShape CategoryTheory.Limits.hasColimitsOfShape_discrete Finite.of_fintype
liftCocone_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.Over CategoryTheory.instCategoryOver lift CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.ι CategoryTheory.Functor.map liftCocone	—	—
liftCocone_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Over CategoryTheory.instCategoryOver lift CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι CategoryTheory.Functor.map liftCocone homMk	—	—
preservesColimitsOfSize_map 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.Over CategoryTheory.instCategoryOver map	—	CategoryTheory.Limits.preservesColimits_of_reflects_of_preserves CategoryTheory.preservesColimits_of_createsColimits_and_hasColimits CategoryTheory.reflectsColimitsOfCreatesColimits

CategoryTheory.Under

Definitions

Name	Category	Theorems
createLimitsOfSizeMapCompForget 📖	CompOp	—
createsLimitsOfSize 📖	CompOp	—
isLimitLiftCone 📖	CompOp	—
isLimitToUnder 📖	CompOp	—
liftCone 📖	CompOp	2 math math: liftCone_pt, liftCone_π_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasLimit_of_hasLimit_comp_forget 📖	mathematical	—	CategoryTheory.Limits.HasLimit CategoryTheory.Under CategoryTheory.instCategoryUnder	—	CategoryTheory.StructuredArrow.hasLimit CategoryTheory.Limits.PreservesLimitsOfShape.preservesLimit CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl
instHasLimits 📖	mathematical	—	CategoryTheory.Limits.HasLimits CategoryTheory.Under CategoryTheory.instCategoryUnder	—	instHasLimitsOfShape CategoryTheory.Limits.hasLimitsOfShapeOfHasLimits
instHasLimitsOfShape 📖	mathematical	—	CategoryTheory.Limits.HasLimitsOfShape CategoryTheory.Under CategoryTheory.instCategoryUnder	—	hasLimit_of_hasLimit_comp_forget CategoryTheory.Limits.hasLimitOfHasLimitsOfShape
liftCone_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.Under CategoryTheory.instCategoryUnder lift CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj CategoryTheory.Functor.const CategoryTheory.Functor.map CategoryTheory.Limits.Cone.π liftCone	—	—
liftCone_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cone.pt lift CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map CategoryTheory.Limits.Cone.π liftCone homMk	—	—
mono_iff_mono_right 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Under CategoryTheory.instCategoryUnder CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	CategoryTheory.StructuredArrow.mono_iff_mono_right CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl
mono_right_of_mono 📖	mathematical	—	CategoryTheory.Mono CategoryTheory.Comma.right CategoryTheory.Discrete CategoryTheory.discreteCategory CategoryTheory.Functor.fromPUnit CategoryTheory.Functor.id CategoryTheory.CommaMorphism.right	—	CategoryTheory.StructuredArrow.mono_right_of_mono CategoryTheory.Functor.instPreservesLimitsOfShapeOfIsRightAdjoint CategoryTheory.Functor.isRightAdjoint_of_isEquivalence CategoryTheory.Functor.isEquivalence_refl
preservesLimitsOfSize_map 📖	mathematical	—	CategoryTheory.Limits.PreservesLimitsOfSize CategoryTheory.Under CategoryTheory.instCategoryUnder map	—	CategoryTheory.Limits.preservesLimits_of_reflects_of_preserves CategoryTheory.preservesLimits_of_createsLimits_and_hasLimits CategoryTheory.reflectsLimitsOfCreatesLimits

---

← Back to Index