Commit 2023-02-28 21:14 7b5ca5d3

View on Github →

feat: port/CategoryTheory.Limits.HasLimits (#2368)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Cones.lean

Created Mathlib/CategoryTheory/Limits/HasLimits.lean

added structure CategoryTheory.Limits.ColimitCocone

added def CategoryTheory.Limits.HasColimit.isoOfEquivalence

added theorem CategoryTheory.Limits.HasColimit.isoOfEquivalence_hom_π

added theorem CategoryTheory.Limits.HasColimit.isoOfEquivalence_inv_π

added def CategoryTheory.Limits.HasColimit.isoOfNatIso

added theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_hom_desc

added theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_inv_desc

added theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_hom

added theorem CategoryTheory.Limits.HasColimit.isoOfNatIso_ι_inv

added theorem CategoryTheory.Limits.HasColimit.mk

added theorem CategoryTheory.Limits.HasColimit.ofCoconesIso

added theorem CategoryTheory.Limits.HasColimits.hasColimitsOfShape

added def CategoryTheory.Limits.HasLimit.isoOfEquivalence

added theorem CategoryTheory.Limits.HasLimit.isoOfEquivalence_hom_π

added theorem CategoryTheory.Limits.HasLimit.isoOfEquivalence_inv_π

added def CategoryTheory.Limits.HasLimit.isoOfNatIso

added theorem CategoryTheory.Limits.HasLimit.isoOfNatIso_hom_π

added theorem CategoryTheory.Limits.HasLimit.isoOfNatIso_inv_π

added theorem CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_hom

added theorem CategoryTheory.Limits.HasLimit.lift_isoOfNatIso_inv

added theorem CategoryTheory.Limits.HasLimit.mk

added theorem CategoryTheory.Limits.HasLimit.ofConesIso

added theorem CategoryTheory.Limits.HasLimits.has_limits_of_shape

added def CategoryTheory.Limits.IsColimit.op

added def CategoryTheory.Limits.IsColimit.unop

added def CategoryTheory.Limits.IsLimit.op

added def CategoryTheory.Limits.IsLimit.unop

added structure CategoryTheory.Limits.LimitCone

added def CategoryTheory.Limits.colim

added def CategoryTheory.Limits.colimConstAdj

added def CategoryTheory.Limits.colimCoyoneda

added def CategoryTheory.Limits.colimMap

added def CategoryTheory.Limits.colimit.cocone

added def CategoryTheory.Limits.colimit.coconeMorphism

added theorem CategoryTheory.Limits.colimit.coconeMorphism_hom

added theorem CategoryTheory.Limits.colimit.cocone_x

added theorem CategoryTheory.Limits.colimit.cocone_ι

added theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_hom

added theorem CategoryTheory.Limits.colimit.comp_coconePointUniqueUpToIso_inv

added def CategoryTheory.Limits.colimit.desc

added theorem CategoryTheory.Limits.colimit.desc_cocone

added theorem CategoryTheory.Limits.colimit.desc_extend

added theorem CategoryTheory.Limits.colimit.existsUnique

added def CategoryTheory.Limits.colimit.homIso'

added def CategoryTheory.Limits.colimit.homIso

added theorem CategoryTheory.Limits.colimit.homIso_hom

added theorem CategoryTheory.Limits.colimit.hom_ext

added def CategoryTheory.Limits.colimit.isColimit

added theorem CategoryTheory.Limits.colimit.isColimit_desc

added def CategoryTheory.Limits.colimit.isoColimitCocone

added theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_hom

added theorem CategoryTheory.Limits.colimit.isoColimitCocone_ι_inv

added theorem CategoryTheory.Limits.colimit.map_desc

added theorem CategoryTheory.Limits.colimit.map_post

added def CategoryTheory.Limits.colimit.post

added theorem CategoryTheory.Limits.colimit.post_desc

added theorem CategoryTheory.Limits.colimit.post_post

added def CategoryTheory.Limits.colimit.pre

added theorem CategoryTheory.Limits.colimit.pre_desc

added theorem CategoryTheory.Limits.colimit.pre_eq

added theorem CategoryTheory.Limits.colimit.pre_id

added theorem CategoryTheory.Limits.colimit.pre_map'

added theorem CategoryTheory.Limits.colimit.pre_map

added theorem CategoryTheory.Limits.colimit.pre_post

added theorem CategoryTheory.Limits.colimit.pre_pre

added theorem CategoryTheory.Limits.colimit.w

added def CategoryTheory.Limits.colimit.ι

added theorem CategoryTheory.Limits.colimit.ι_coconeMorphism

added theorem CategoryTheory.Limits.colimit.ι_desc

added theorem CategoryTheory.Limits.colimit.ι_map

added theorem CategoryTheory.Limits.colimit.ι_post

added theorem CategoryTheory.Limits.colimit.ι_pre

added def CategoryTheory.Limits.colimit

added def CategoryTheory.Limits.constLimAdj

added def CategoryTheory.Limits.getColimitCocone

added def CategoryTheory.Limits.getLimitCone

added theorem CategoryTheory.Limits.hasColimitOfIso

added theorem CategoryTheory.Limits.hasColimit_of_equivalence_comp

added theorem CategoryTheory.Limits.hasColimitsOfShape_of_equivalence

added theorem CategoryTheory.Limits.hasColimitsOfSize_shrink

added theorem CategoryTheory.Limits.hasLimitOfEquivalenceComp

added theorem CategoryTheory.Limits.hasLimitOfIso

added theorem CategoryTheory.Limits.hasLimitsOfShapeOfEquivalence

added theorem CategoryTheory.Limits.hasLimitsOfSizeShrink

added def CategoryTheory.Limits.isColimitEquivIsLimitOp

added def CategoryTheory.Limits.isLimitEquivIsColimitOp

added def CategoryTheory.Limits.lim

added def CategoryTheory.Limits.limMap

added theorem CategoryTheory.Limits.limMap_π

added def CategoryTheory.Limits.limYoneda

added def CategoryTheory.Limits.limit.cone

added def CategoryTheory.Limits.limit.coneMorphism

added theorem CategoryTheory.Limits.limit.coneMorphism_hom

added theorem CategoryTheory.Limits.limit.coneMorphism_π

added theorem CategoryTheory.Limits.limit.conePointUniqueUpToIso_hom_comp

added theorem CategoryTheory.Limits.limit.conePointUniqueUpToIso_inv_comp

added theorem CategoryTheory.Limits.limit.cone_x

added theorem CategoryTheory.Limits.limit.cone_π

added theorem CategoryTheory.Limits.limit.existsUnique

added def CategoryTheory.Limits.limit.homIso'

added def CategoryTheory.Limits.limit.homIso

added theorem CategoryTheory.Limits.limit.homIso_hom

added theorem CategoryTheory.Limits.limit.hom_ext

added theorem CategoryTheory.Limits.limit.id_pre

added def CategoryTheory.Limits.limit.isLimit

added theorem CategoryTheory.Limits.limit.isLimit_lift

added def CategoryTheory.Limits.limit.isoLimitCone

added theorem CategoryTheory.Limits.limit.isoLimitCone_hom_π

added theorem CategoryTheory.Limits.limit.isoLimitCone_inv_π

added def CategoryTheory.Limits.limit.lift

added theorem CategoryTheory.Limits.limit.lift_cone

added theorem CategoryTheory.Limits.limit.lift_extend

added theorem CategoryTheory.Limits.limit.lift_map

added theorem CategoryTheory.Limits.limit.lift_post

added theorem CategoryTheory.Limits.limit.lift_pre

added theorem CategoryTheory.Limits.limit.lift_π

added theorem CategoryTheory.Limits.limit.map_post

added theorem CategoryTheory.Limits.limit.map_pre'

added theorem CategoryTheory.Limits.limit.map_pre

added def CategoryTheory.Limits.limit.post

added theorem CategoryTheory.Limits.limit.post_post

added theorem CategoryTheory.Limits.limit.post_π

added def CategoryTheory.Limits.limit.pre

added theorem CategoryTheory.Limits.limit.pre_eq

added theorem CategoryTheory.Limits.limit.pre_post

added theorem CategoryTheory.Limits.limit.pre_pre

added theorem CategoryTheory.Limits.limit.pre_π

added theorem CategoryTheory.Limits.limit.w

added def CategoryTheory.Limits.limit.π

added def CategoryTheory.Limits.limit

added theorem CategoryTheory.Limits.ι_colimMap