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} [CategoryTheory.Category.{v, u} C] {X : C} {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 : CategoryTheory.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.

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

Instances For

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

    @[simp]

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

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

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

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

    Equations
    Instances For

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

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

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

        Equations
        Instances For

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

          Equations
          Instances For

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

            Instances For
              @[simp]

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

              The trivial factorisation of a monomorphism satisfies the universal property.

              Equations
              Instances For

                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 := }
                Instances For

                  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
                  Instances For
                    structure CategoryTheory.Limits.ImageFactorisation {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :
                    Type (max u v)

                    Data exhibiting that a morphism f has an image.

                    Instances For

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

                      Equations
                      • F.ofArrowIso sq = { F := F.F.ofArrowIso sq, isImage := F.isImage.ofArrowIso sq }
                      Instances For
                        class CategoryTheory.Limits.HasImage {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (f : X Y) :

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

                        Instances

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

                          @[instance 100]
                          Equations
                          • =

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

                          Equations
                          Instances For

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

                            Equations
                            Instances For

                              The categorical image of a morphism.

                              Equations
                              Instances For

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

                                Equations
                                Instances For

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

                                  Equations
                                  Instances For

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

                                    Equations
                                    • =

                                    HasImages asserts that every morphism has an image.

                                    Instances

                                      HasImages asserts that every morphism has an image.

                                      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.
                                      Instances For

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

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

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

                                          Equations
                                          • =

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

                                          Equations
                                          • =

                                          Postcomposing by an isomorphism induces an isomorphism on the image.

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

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

                                            Instances For
                                              @[simp]

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

                                              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.
                                              Instances For

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

                                                Instances
                                                  theorem CategoryTheory.Limits.ImageMap.ext {C : Type u} :
                                                  ∀ {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C} {inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f g} {x y : CategoryTheory.Limits.ImageMap sq}, x.map = y.mapx = y

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

                                                  Equations
                                                  Instances For

                                                    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.
                                                      Instances For

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

                                                        Instances For

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

                                                          Satisfying the inhabited linter

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

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

                                                          Equations
                                                          Instances For

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

                                                            Instances

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

                                                              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.

                                                                Equations
                                                                • =
                                                                @[instance 100]

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

                                                                Equations
                                                                • =

                                                                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.
                                                                Instances For

                                                                  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.
                                                                  Instances For