Documentation

Mathlib.CategoryTheory.Limits.Shapes.Images

Categorical images #

We define the categorical image of f as a factorisation f = em through a monomorphism m, so that m factors through the m' in any other such factorisation.

Main definitions #

Main statements #

Future work #

structure CategoryTheory.Limits.MonoFactorisation {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) :
Type (max u v)

A factorisation of a morphism f = em, with m monic.

  • I : C

    A factorisation of a morphism f = em, with m monic.

  • m : self.I Y

    A factorisation of a morphism f = em, with m monic.

  • m_mono : Mono self.m

    A factorisation of a morphism f = em, with m monic.

  • e : X self.I

    A factorisation of a morphism f = em, with m monic.

  • fac : CategoryStruct.comp self.e self.m = f

    A factorisation of a morphism f = em, with m monic.

@[simp]

The obvious factorisation of a monomorphism through itself.

Equations
theorem CategoryTheory.Limits.MonoFactorisation.ext {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F F' : MonoFactorisation f} (hI : F.I = F'.I) (hm : F.m = CategoryStruct.comp (eqToHom hI) F'.m) :
F = F'

The morphism m in a factorisation f = em through a monomorphism is uniquely determined.

Any mono factorisation of f gives a mono factorisation of f ≫ g when g is a mono.

Equations
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.compMono_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} (F : MonoFactorisation f) {Y' : C} (g : Y Y') [Mono g] :
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.compMono_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} (F : MonoFactorisation f) {Y' : C} (g : Y Y') [Mono g] :
(F.compMono g).I = F.I
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.compMono_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} (F : MonoFactorisation f) {Y' : C} (g : Y Y') [Mono g] :
(F.compMono g).e = F.e

A mono factorisation of f ≫ g, where g is an isomorphism, gives a mono factorisation of f.

Equations
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofCompIso_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {Y' : C} {g : Y Y'} [IsIso g] (F : MonoFactorisation (CategoryStruct.comp f g)) :
@[simp]
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofCompIso_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {Y' : C} {g : Y Y'} [IsIso g] (F : MonoFactorisation (CategoryStruct.comp f g)) :

Any mono factorisation of f gives a mono factorisation of g ≫ f.

Equations
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.isoComp_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} (F : MonoFactorisation f) {X' : C} (g : X' X) :
(F.isoComp g).I = F.I
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.isoComp_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} (F : MonoFactorisation f) {X' : C} (g : X' X) :
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.isoComp_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} (F : MonoFactorisation f) {X' : C} (g : X' X) :
(F.isoComp g).m = F.m

A mono factorisation of g ≫ f, where g is an isomorphism, gives a mono factorisation of f.

Equations
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_e {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {X' : C} (g : X' X) [IsIso g] (F : MonoFactorisation (CategoryStruct.comp g f)) :
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {X' : C} (g : X' X) [IsIso g] (F : MonoFactorisation (CategoryStruct.comp g f)) :
(ofIsoComp g F).m = F.m
@[simp]
theorem CategoryTheory.Limits.MonoFactorisation.ofIsoComp_I {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {X' : C} (g : X' X) [IsIso g] (F : MonoFactorisation (CategoryStruct.comp g f)) :
(ofIsoComp g F).I = F.I

If f and g are isomorphic arrows, then a mono factorisation of f gives a mono factorisation of g

Equations
@[simp]
structure CategoryTheory.Limits.IsImage {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} (F : MonoFactorisation f) :
Type (max u v)

Data exhibiting that a given factorisation through a mono is initial.

@[simp]
theorem CategoryTheory.Limits.IsImage.lift_fac_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F : MonoFactorisation f} (self : IsImage F) (F' : MonoFactorisation f) {Z : C} (h : Y Z) :
@[simp]
theorem CategoryTheory.Limits.IsImage.fac_lift {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F : MonoFactorisation f} (hF : IsImage F) (F' : MonoFactorisation f) :
@[simp]
theorem CategoryTheory.Limits.IsImage.fac_lift_assoc {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F : MonoFactorisation f} (hF : IsImage F) (F' : MonoFactorisation f) {Z : C} (h : F'.I Z) :

The trivial factorisation of a monomorphism satisfies the universal property.

Equations
@[simp]
theorem CategoryTheory.Limits.IsImage.self_lift {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [Mono f] (F' : MonoFactorisation f) :
(self f).lift F' = F'.e
def CategoryTheory.Limits.IsImage.isoExt {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') :
F.I F'.I

Two factorisations through monomorphisms satisfying the universal property must factor through isomorphic objects.

Equations
  • hF.isoExt hF' = { hom := hF.lift F', inv := hF'.lift F, hom_inv_id := , inv_hom_id := }
@[simp]
theorem CategoryTheory.Limits.IsImage.isoExt_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') :
(hF.isoExt hF').inv = hF'.lift F
@[simp]
theorem CategoryTheory.Limits.IsImage.isoExt_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') :
(hF.isoExt hF').hom = hF.lift F'
theorem CategoryTheory.Limits.IsImage.isoExt_hom_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') :
theorem CategoryTheory.Limits.IsImage.isoExt_inv_m {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') :
theorem CategoryTheory.Limits.IsImage.e_isoExt_hom {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') :
theorem CategoryTheory.Limits.IsImage.e_isoExt_inv {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} {F F' : MonoFactorisation f} (hF : IsImage F) (hF' : IsImage F') :

If f and g are isomorphic arrows, then a mono factorisation of f that is an image gives a mono factorisation of g that is an image

Equations
@[simp]
theorem CategoryTheory.Limits.IsImage.ofArrowIso_lift {C : Type u} [Category.{v, u} C] {f g : Arrow C} {F : MonoFactorisation f.hom} (hF : IsImage F) (sq : f g) [IsIso sq] (F' : MonoFactorisation g.hom) :
(hF.ofArrowIso sq).lift F' = hF.lift (F'.ofArrowIso (inv sq))
structure CategoryTheory.Limits.ImageFactorisation {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) :
Type (max u v)

Data exhibiting that a morphism f has an image.

  • Data exhibiting that a morphism f has an image.

  • isImage : IsImage self.F

    Data exhibiting that a morphism f has an image.

If f and g are isomorphic arrows, then an image factorisation of f gives an image factorisation of g

Equations
class CategoryTheory.Limits.HasImage {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) :

HasImage f means that there exists an image factorisation of f.

Instances
    @[instance 100]
    instance CategoryTheory.Limits.mono_hasImage {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [Mono f] :

    Some factorisation of f through a monomorphism (selected with choice).

    Equations

    The witness of the universal property for the chosen factorisation of f through a monomorphism.

    Equations
    def CategoryTheory.Limits.image {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [HasImage f] :
    C

    The categorical image of a morphism.

    Equations
    def CategoryTheory.Limits.image.ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [HasImage f] :

    The inclusion of the image of a morphism into the target.

    Equations
    @[simp]
    instance CategoryTheory.Limits.instMonoι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [HasImage f] :
    def CategoryTheory.Limits.factorThruImage {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [HasImage f] :

    The map from the source to the image of a morphism.

    Equations
    @[simp]

    Rewrite in terms of the factorThruImage interface.

    @[simp]
    def CategoryTheory.Limits.image.lift {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} [HasImage f] (F' : MonoFactorisation f) :
    image f F'.I

    Any other factorisation of the morphism f through a monomorphism receives a map from the image.

    Equations
    @[simp]
    theorem CategoryTheory.Limits.image.lift_fac {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} [HasImage f] (F' : MonoFactorisation f) :
    @[simp]
    @[simp]
    instance CategoryTheory.Limits.image.lift_mono {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} [HasImage f] (F' : MonoFactorisation f) :
    Mono (lift F')
    theorem CategoryTheory.Limits.HasImage.uniq {C : Type u} [Category.{v, u} C] {X Y : C} {f : X Y} [HasImage f] (F' : MonoFactorisation f) (l : image f F'.I) (w : CategoryStruct.comp l F'.m = image.ι f) :
    instance CategoryTheory.Limits.instHasImageCompOfIsIso {C : Type u} [Category.{v, u} C] {X Y Z : C} (f : X Y) [IsIso f] (g : Y Z) [HasImage g] :

    If has_image g, then has_image (f ≫ g) when f is an isomorphism.

    HasImages asserts that every morphism has an image.

    Instances
      theorem CategoryTheory.Limits.epi_image_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) [HasImage f] [E : Epi f] :
      def CategoryTheory.Limits.image.eqToHom {C : Type u} [Category.{v, u} C] {X Y : C} {f f' : X Y} [HasImage f] [HasImage f'] (h : f = f') :

      An equation between morphisms gives a comparison map between the images (which momentarily we prove is an iso).

      Equations
      • One or more equations did not get rendered due to their size.
      instance CategoryTheory.Limits.instIsIsoEqToHom {C : Type u} [Category.{v, u} C] {X Y : C} {f f' : X Y} [HasImage f] [HasImage f'] (h : f = f') :
      def CategoryTheory.Limits.image.eqToIso {C : Type u} [Category.{v, u} C] {X Y : C} {f f' : X Y} [HasImage f] [HasImage f'] (h : f = f') :

      An equation between morphisms gives an isomorphism between the images.

      Equations
      theorem CategoryTheory.Limits.image.eq_fac {C : Type u} [Category.{v, u} C] {X Y : C} {f f' : X Y} [HasImage f] [HasImage f'] [HasEqualizers C] (h : f = f') :

      As long as the category has equalizers, the image inclusion maps commute with image.eqToIso.

      def CategoryTheory.Limits.image.preComp {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) {Z : C} (g : Y Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] :

      The comparison map image (f ≫ g) ⟶ image g.

      Equations
      • One or more equations did not get rendered due to their size.
      @[simp]
      theorem CategoryTheory.Limits.image.preComp_ι {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) {Z : C} (g : Y Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] :
      @[simp]
      theorem CategoryTheory.Limits.image.preComp_ι_assoc {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) {Z : C} (g : Y Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] {Z✝ : C} (h : Z Z✝) :
      instance CategoryTheory.Limits.image.preComp_mono {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) {Z : C} (g : Y Z) [HasImage g] [HasImage (CategoryStruct.comp f g)] :

      image.preComp f g is a monomorphism.

      The two step comparison map image (f ≫ (g ≫ h)) ⟶ image (g ≫ h) ⟶ image h agrees with the one step comparison map image (f ≫ (g ≫ h)) ≅ image ((f ≫ g) ≫ h) ⟶ image h.

      instance CategoryTheory.Limits.image.preComp_epi_of_epi {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) {Z : C} (g : Y Z) [HasEqualizers C] [HasImage g] [HasImage (CategoryStruct.comp f g)] [Epi f] :
      Epi (preComp f g)

      image.preComp f g is an epimorphism when f is an epimorphism (we need C to have equalizers to prove this).

      instance CategoryTheory.Limits.hasImage_iso_comp {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) {Z : C} (g : Y Z) [IsIso f] [HasImage g] :
      instance CategoryTheory.Limits.image.isIso_precomp_iso {C : Type u} [Category.{v, u} C] {X Y Z : C} (g : Y Z) [HasEqualizers C] (f : X Y) [IsIso f] [HasImage g] :

      image.preComp f g is an isomorphism when f is an isomorphism (we need C to have equalizers to prove this).

      instance CategoryTheory.Limits.hasImage_comp_iso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) {Z : C} (g : Y Z) [HasImage f] [IsIso g] :
      def CategoryTheory.Limits.image.compIso {C : Type u} [Category.{v, u} C] {X Y : C} (f : X Y) {Z : C} (g : Y Z) [HasEqualizers C] [HasImage f] [IsIso g] :

      Postcomposing by an isomorphism induces an isomorphism on the image.

      Equations
      • One or more equations did not get rendered due to their size.
      structure CategoryTheory.Limits.ImageMap {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f g) :

      An image map is a morphism image f → image g fitting into a commutative square and satisfying the obvious commutativity conditions.

      def CategoryTheory.Limits.ImageMap.transport {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f g) (F : MonoFactorisation f.hom) {F' : MonoFactorisation g.hom} (hF' : IsImage F') {map : F.I F'.I} (map_ι : CategoryStruct.comp map F'.m = CategoryStruct.comp F.m sq.right) :

      To give an image map for a commutative square with f at the top and g at the bottom, it suffices to give a map between any mono factorisation of f and any image factorisation of g.

      Equations
      • One or more equations did not get rendered due to their size.

      HasImageMap sq means that there is an ImageMap for the square sq.

      Instances
        theorem CategoryTheory.Limits.HasImageMap.transport {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f g) (F : MonoFactorisation f.hom) {F' : MonoFactorisation g.hom} (hF' : IsImage F') (map : F.I F'.I) (map_ι : CategoryStruct.comp map F'.m = CategoryStruct.comp F.m sq.right) :
        @[instance 100]
        instance CategoryTheory.Limits.HasImageMap.comp {C : Type u} [Category.{v, u} C] {f g h : Arrow C} [HasImage f.hom] [HasImage g.hom] [HasImage h.hom] (sq1 : f g) (sq2 : g h) [HasImageMap sq1] [HasImageMap sq2] :
        theorem CategoryTheory.Limits.ImageMap.ext {C : Type u} {inst✝ : Category.{v, u} C} {f g : Arrow C} {inst✝¹ : HasImage f.hom} {inst✝² : HasImage g.hom} {sq : f g} {x y : ImageMap sq} (map : x.map = y.map) :
        x = y
        theorem CategoryTheory.Limits.ImageMap.ext_iff {C : Type u} {inst✝ : Category.{v, u} C} {f g : Arrow C} {inst✝¹ : HasImage f.hom} {inst✝² : HasImage g.hom} {sq : f g} {x y : ImageMap sq} :
        x = y x.map = y.map
        theorem CategoryTheory.Limits.ImageMap.map_uniq_aux {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f g} (map : image f.hom image g.hom) (map_ι : CategoryStruct.comp map (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right := by aesop_cat) (map' : image f.hom image g.hom) (map_ι' : CategoryStruct.comp map' (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right) :
        map = map'
        theorem CategoryTheory.Limits.ImageMap.map_uniq {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f g} (F G : ImageMap sq) :
        F.map = G.map
        @[simp]
        theorem CategoryTheory.Limits.ImageMap.mk.injEq' {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] {sq : f g} (map : image f.hom image g.hom) (map_ι : CategoryStruct.comp map (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right := by aesop_cat) (map' : image f.hom image g.hom) (map_ι' : CategoryStruct.comp map' (image.ι g.hom) = CategoryStruct.comp (image.ι f.hom) sq.right) :
        (map = map') = True
        @[reducible, inline]

        The map on images induced by a commutative square.

        Equations
        theorem CategoryTheory.Limits.image.map_homMk'_ι {C : Type u} [Category.{v, u} C] {X Y P Q : C} {k : X Y} [HasImage k] {l : P Q} [HasImage l] {m : X P} {n : Y Q} (w : CategoryStruct.comp m l = CategoryStruct.comp k n) [HasImageMap (Arrow.homMk' m n w)] :
        def CategoryTheory.Limits.imageMapComp {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f g) [HasImageMap sq] {h : Arrow C} [HasImage h.hom] (sq' : g h) [HasImageMap sq'] :

        Image maps for composable commutative squares induce an image map in the composite square.

        Equations
        @[simp]
        theorem CategoryTheory.Limits.image.map_comp {C : Type u} [Category.{v, u} C] {f g : Arrow C} [HasImage f.hom] [HasImage g.hom] (sq : f g) [HasImageMap sq] {h : Arrow C} [HasImage h.hom] (sq' : g h) [HasImageMap sq'] [HasImageMap (CategoryStruct.comp sq sq')] :

        The identity image f ⟶ image f fits into the commutative square represented by the identity morphism 𝟙 f in the arrow category.

        Equations

        If a category has_image_maps, then all commutative squares induce morphisms on images.

        Instances

          The functor from the arrow category of C to C itself that maps a morphism to its image and a commutative square to the induced morphism on images.

          Equations
          • One or more equations did not get rendered due to their size.
          @[simp]
          theorem CategoryTheory.Limits.im_map {C : Type u} [Category.{v, u} C] [HasImages C] [HasImageMaps C] {X✝ Y✝ : Arrow C} (st : X✝ Y✝) :

          A strong epi-mono factorisation is a decomposition f = em with e a strong epimorphism and m a monomorphism.

          Satisfying the inhabited linter

          Equations

          A mono factorisation coming from a strong epi-mono factorisation always has the universal property of the image.

          Equations

          A category has strong epi-mono factorisations if every morphism admits a strong epi-mono factorisation.

          • mk' :: (
          • )
          Instances

            A category has strong epi images if it has all images and factorThruImage f is a strong epimorphism for all f.

            Instances

              If there is a single strong epi-mono factorisation of f, then every image factorisation is a strong epi-mono factorisation.

              @[instance 100]

              If we constructed our images from strong epi-mono factorisations, then these images are strong epi images.

              @[instance 100]

              A category with strong epi images has image maps.

              @[instance 100]

              If a category has images, equalizers and pullbacks, then images are automatically strong epi images.

              def CategoryTheory.Limits.image.isoStrongEpiMono {C : Type u} [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] {X Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : CategoryStruct.comp e m = f) [StrongEpi e] [Mono m] :
              I' image f

              If C has strong epi mono factorisations, then the image is unique up to isomorphism, in that if f factors as a strong epi followed by a mono, this factorisation is essentially the image factorisation.

              Equations
              • One or more equations did not get rendered due to their size.
              @[simp]
              theorem CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι {C : Type u} [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] {X Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : CategoryStruct.comp e m = f) [StrongEpi e] [Mono m] :
              @[simp]
              theorem CategoryTheory.Limits.image.isoStrongEpiMono_inv_comp_mono {C : Type u} [Category.{v, u} C] [HasStrongEpiMonoFactorisations C] {X Y : C} {f : X Y} {I' : C} (e : X I') (m : I' Y) (comm : CategoryStruct.comp e m = f) [StrongEpi e] [Mono m] :

              A category with strong epi mono factorisations admits functorial epi/mono factorizations.

              Equations
              • One or more equations did not get rendered due to their size.