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)
  • I : C

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

  • m : s.I Y

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

  • m_mono : CategoryTheory.Mono s.m

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

  • e : X s.I

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

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

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

Instances For

    The obvious factorisation of a monomorphism through itself.

    Instances For

      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.

      Instances For

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

        Instances For

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

          Instances For

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

            Instances For

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

              Instances For

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

                Instances For

                  The trivial factorisation of a monomorphism satisfies the universal property.

                  Instances For

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

                    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

                      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

                          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

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

                              Instances For

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

                                Instances For

                                  The categorical image of a morphism.

                                  Instances For

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

                                    Instances For

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

                                      Instances For

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

                                        Instances For

                                          HasImages asserts that every morphism has an image.

                                          Instances

                                            The image of a monomorphism is isomorphic to the source.

                                            Instances For

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

                                              Instances For

                                                An equation between morphisms gives an isomorphism between the images.

                                                Instances For

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

                                                  Postcomposing by an isomorphism induces an isomorphism on the image.

                                                  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

                                                      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.

                                                      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.

                                                          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.

                                                              Instances For

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

                                                                Instances For

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

                                                                  Instances For

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

                                                                    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.

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

                                                                        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.

                                                                        Instances For