Commit 2023-03-11 14:23 7edeec3f

View on Github →

feat: Port CategoryTheory.Limits.ConeCategory (#2767)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Limits/ConeCategory.lean

added def CategoryTheory.Limits.Cocone.equivStructuredArrow

added def CategoryTheory.Limits.Cocone.fromStructuredArrow

added def CategoryTheory.Limits.Cocone.isColimitEquivIsInitial

added def CategoryTheory.Limits.Cocone.toStructuredArrow

added def CategoryTheory.Limits.Cone.equivCostructuredArrow

added def CategoryTheory.Limits.Cone.fromCostructuredArrow

added def CategoryTheory.Limits.Cone.isLimitEquivIsTerminal

added def CategoryTheory.Limits.Cone.toCostructuredArrow

added theorem CategoryTheory.Limits.IsColimit.descCoconeMorphism_eq_isInitial_to

added def CategoryTheory.Limits.IsColimit.ofPreservesCoconeInitial

added def CategoryTheory.Limits.IsColimit.ofReflectsCoconeInitial

added theorem CategoryTheory.Limits.IsInitial.to_eq_descCoconeMorphism

added theorem CategoryTheory.Limits.IsLimit.liftConeMorphism_eq_isTerminal_from

added def CategoryTheory.Limits.IsLimit.ofPreservesConeTerminal

added def CategoryTheory.Limits.IsLimit.ofReflectsConeTerminal

added theorem CategoryTheory.Limits.IsTerminal.from_eq_liftConeMorphism

added theorem CategoryTheory.Limits.hasColimit_iff_hasInitial_cocone

added theorem CategoryTheory.Limits.hasColimitsOfShape_iff_isRightAdjoint_const

added theorem CategoryTheory.Limits.hasLimit_iff_hasTerminal_cone

added theorem CategoryTheory.Limits.hasLimitsOfShape_iff_isLeftAdjoint_const