Commit 2023-03-11 13:48 89751ebf

View on Github →

feat: port CategoryTheory.Limits.Types (#2712)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Images.lean

modified theorem CategoryTheory.Limits.ImageMap.map_uniq

modified theorem CategoryTheory.Limits.ImageMap.map_uniq_aux

modified theorem CategoryTheory.Limits.ImageMap.mk.injEq'

modified def CategoryTheory.Limits.IsImage.isoExt

modified theorem CategoryTheory.Limits.MonoFactorisation.ext

Created Mathlib/CategoryTheory/Limits/Types.lean

added theorem CategoryTheory.Limits.Types.Colimit.w_apply'

added theorem CategoryTheory.Limits.Types.Colimit.w_apply

added theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply'

added theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply

added theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply'

added theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply

added theorem CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff

added theorem CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux

added theorem CategoryTheory.Limits.Types.FilteredColimit.eqvGen_quot_rel_of_rel

added theorem CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff

added theorem CategoryTheory.Limits.Types.FilteredColimit.rel_of_quot_rel

added theorem CategoryTheory.Limits.Types.Image.lift_fac

added def CategoryTheory.Limits.Types.Image.ι

added def CategoryTheory.Limits.Types.Image

added theorem CategoryTheory.Limits.Types.Limit.lift_π_apply'

added theorem CategoryTheory.Limits.Types.Limit.lift_π_apply

added theorem CategoryTheory.Limits.Types.Limit.map_π_apply'

added theorem CategoryTheory.Limits.Types.Limit.map_π_apply

added theorem CategoryTheory.Limits.Types.Limit.w_apply'

added theorem CategoryTheory.Limits.Types.Limit.w_apply

added theorem CategoryTheory.Limits.Types.Limit.π_mk

added def CategoryTheory.Limits.Types.Quot.Rel

added def CategoryTheory.Limits.Types.Quot

added def CategoryTheory.Limits.Types.colimitCocone

added def CategoryTheory.Limits.Types.colimitCoconeIsColimit

added theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply

added theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply

added theorem CategoryTheory.Limits.Types.colimit_eq

added theorem CategoryTheory.Limits.Types.colimit_sound'

added theorem CategoryTheory.Limits.Types.colimit_sound

added def CategoryTheory.Limits.Types.isLimitEquivSections

added theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply

added theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply

added theorem CategoryTheory.Limits.Types.jointly_surjective'

added theorem CategoryTheory.Limits.Types.jointly_surjective

added def CategoryTheory.Limits.Types.limitCone

added def CategoryTheory.Limits.Types.limitConeIsLimit

added theorem CategoryTheory.Limits.Types.limitEquivSections_apply

added theorem CategoryTheory.Limits.Types.limitEquivSections_symm_apply

added theorem CategoryTheory.Limits.Types.limit_ext'

added theorem CategoryTheory.Limits.Types.limit_ext

added theorem CategoryTheory.Limits.Types.limit_ext_iff'

added theorem CategoryTheory.Limits.Types.limit_ext_iff

added def CategoryTheory.Limits.Types.monoFactorisation

Modified Mathlib/CategoryTheory/Types.lean

added theorem CategoryTheory.Functor.sections_property