Commit 2023-03-07 17:35 367e5e69

View on Github →

feat: port CategoryTheory.Limits.Shapes.Images (#2615)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Category/Basic.lean

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

added theorem CategoryTheory.Functor.hasStrongEpiMonoFactorisations_imp_of_isEquivalence

added theorem CategoryTheory.Limits.HasImage.mk

added theorem CategoryTheory.Limits.HasImage.of_arrow_iso

added theorem CategoryTheory.Limits.HasImage.uniq

added def CategoryTheory.Limits.HasImageMap.imageMap

added theorem CategoryTheory.Limits.HasImageMap.mk

added theorem CategoryTheory.Limits.HasImageMap.transport

added theorem CategoryTheory.Limits.HasStrongEpiMonoFactorisations.mk

added def CategoryTheory.Limits.Image.isImage

added def CategoryTheory.Limits.Image.monoFactorisation

added def CategoryTheory.Limits.ImageFactorisation.ofArrowIso

added structure CategoryTheory.Limits.ImageFactorisation

added theorem CategoryTheory.Limits.ImageMap.factor_map

added theorem CategoryTheory.Limits.ImageMap.map_uniq

added theorem CategoryTheory.Limits.ImageMap.map_uniq_aux

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

added def CategoryTheory.Limits.ImageMap.transport

added structure CategoryTheory.Limits.ImageMap

added theorem CategoryTheory.Limits.IsImage.e_isoExt_hom

added theorem CategoryTheory.Limits.IsImage.e_isoExt_inv

added theorem CategoryTheory.Limits.IsImage.fac_lift

added def CategoryTheory.Limits.IsImage.isoExt

added theorem CategoryTheory.Limits.IsImage.isoExt_hom_m

added theorem CategoryTheory.Limits.IsImage.isoExt_inv_m

added theorem CategoryTheory.Limits.IsImage.lift_ι

added def CategoryTheory.Limits.IsImage.ofArrowIso

added def CategoryTheory.Limits.IsImage.self

added structure CategoryTheory.Limits.IsImage

added def CategoryTheory.Limits.MonoFactorisation.compMono

added theorem CategoryTheory.Limits.MonoFactorisation.ext

added def CategoryTheory.Limits.MonoFactorisation.isoComp

added def CategoryTheory.Limits.MonoFactorisation.ofArrowIso

added def CategoryTheory.Limits.MonoFactorisation.ofCompIso

added def CategoryTheory.Limits.MonoFactorisation.ofIsoComp

added def CategoryTheory.Limits.MonoFactorisation.self

added structure CategoryTheory.Limits.MonoFactorisation

added def CategoryTheory.Limits.StrongEpiMonoFactorisation.toMonoIsImage

added structure CategoryTheory.Limits.StrongEpiMonoFactorisation

added theorem CategoryTheory.Limits.as_factorThruImage

added theorem CategoryTheory.Limits.epi_image_of_epi

added theorem CategoryTheory.Limits.epi_of_epi_image

added def CategoryTheory.Limits.factorThruImage

added def CategoryTheory.Limits.im

added theorem CategoryTheory.Limits.image.as_ι

added def CategoryTheory.Limits.image.compIso

added theorem CategoryTheory.Limits.image.compIso_hom_comp_image_ι

added theorem CategoryTheory.Limits.image.compIso_inv_comp_image_ι

added def CategoryTheory.Limits.image.eqToHom

added def CategoryTheory.Limits.image.eqToIso

added theorem CategoryTheory.Limits.image.eq_fac

added theorem CategoryTheory.Limits.image.ext

added theorem CategoryTheory.Limits.image.fac

added theorem CategoryTheory.Limits.image.fac_lift

added theorem CategoryTheory.Limits.image.factorThruImage_preComp

added theorem CategoryTheory.Limits.image.factor_map

added theorem CategoryTheory.Limits.image.isImage_lift

added def CategoryTheory.Limits.image.isoStrongEpiMono

added theorem CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι

added theorem CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono

added def CategoryTheory.Limits.image.lift

added theorem CategoryTheory.Limits.image.lift_fac

added theorem CategoryTheory.Limits.image.map_comp

added theorem CategoryTheory.Limits.image.map_homMk'_ι

added theorem CategoryTheory.Limits.image.map_id

added theorem CategoryTheory.Limits.image.map_ι

added def CategoryTheory.Limits.image.preComp

added theorem CategoryTheory.Limits.image.preComp_comp

added theorem CategoryTheory.Limits.image.preComp_ι

added def CategoryTheory.Limits.image.ι

added def CategoryTheory.Limits.image

added def CategoryTheory.Limits.imageMapComp

added def CategoryTheory.Limits.imageMapId

added def CategoryTheory.Limits.imageMonoIsoSource

added theorem CategoryTheory.Limits.imageMonoIsoSource_hom_self

added theorem CategoryTheory.Limits.imageMonoIsoSource_inv_ι

added theorem CategoryTheory.Limits.strongEpi_factorThruImage_of_strongEpiMonoFactorisation

added theorem CategoryTheory.Limits.strongEpi_of_strongEpiMonoFactorisation