Documentation

Mathlib.CategoryTheory.EssentialImage

Essential image of a functor #

The essential image essImage of a functor consists of the objects in the target category which are isomorphic to an object in the image of the object function. This, for instance, allows us to talk about objects belonging to a subcategory expressed as a functor rather than a subtype, preserving the principle of equivalence. For example this lets us define exponential ideals.

The essential image can also be seen as a subcategory of the target category, and witnesses that a functor decomposes into an essentially surjective functor and a fully faithful functor. (TODO: show that this decomposition forms an orthogonal factorisation system).

The essential image of a functor F consists of those objects in the target category which are isomorphic to an object in the image of the function F.obj. In other words, this is the closure under isomorphism of the function F.obj. This is the "non-evil" way of describing the image of a functor.

Equations
Instances For

    Get the witnessing object that Y is in the subcategory given by F.

    Equations
    Instances For

      Extract the isomorphism between F.obj h.witness and Y itself.

      Equations
      Instances For
        theorem CategoryTheory.Functor.essImage.ofIso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {Y : D} {Y' : D} (h : Y Y') (hY : Y F.essImage) :
        Y' F.essImage

        Being in the essential image is a "hygienic" property: it is preserved under isomorphism.

        theorem CategoryTheory.Functor.essImage.ofNatIso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {F' : CategoryTheory.Functor C D} (h : F F') {Y : D} (hY : Y F.essImage) :
        Y F'.essImage

        If Y is in the essential image of F then it is in the essential image of F' as long as F ≅ F'.

        Isomorphic functors have equal essential images.

        An object in the image is in the essential image.

        The essential image of a functor, interpreted as a full subcategory of the target category.

        Equations
        Instances For
          Equations
          • CategoryTheory.Functor.instCategoryEssImageSubcategory = inferInstance
          @[simp]
          theorem CategoryTheory.Functor.essImageInclusion_map {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
          ∀ {X Y : CategoryTheory.InducedCategory D CategoryTheory.FullSubcategory.obj} (f : X Y), F.essImageInclusion.map f = f
          @[simp]

          The essential image as a subcategory has a fully faithful inclusion into the target category.

          Equations
          Instances For
            theorem CategoryTheory.Functor.essImage_ext {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : F.EssImageSubcategory} {Y : F.EssImageSubcategory} (f : X Y) (g : X Y) (h : F.essImageInclusion.map f = F.essImageInclusion.map g) :
            f = g
            @[simp]
            theorem CategoryTheory.Functor.toEssImage_map {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) :
            ∀ {X Y : C} (f : X Y), F.toEssImage.map f = F.map f
            @[simp]
            theorem CategoryTheory.Functor.toEssImage_obj_obj {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) (X : C) :
            (F.toEssImage.obj X).obj = F.obj X

            Given a functor F : C ⥤ D, we have an (essentially surjective) functor from C to the essential image of F.

            Equations
            Instances For

              The functor F factorises through its essential image, where the first functor is essentially surjective and the second is fully faithful.

              Equations
              Instances For

                A functor F : C ⥤ D is essentially surjective if every object of D is in the essential image of F. In other words, for every Y : D, there is some X : C with F.obj X ≅ Y.

                See https://stacks.math.columbia.edu/tag/001C.

                • mem_essImage : ∀ (Y : D), Y F.essImage

                  All the objects of the target category are in the essential image.

                Instances
                  theorem CategoryTheory.Functor.EssSurj.mem_essImage {C : Type u₁} {D : Type u₂} :
                  ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.EssSurj] (Y : D), Y F.essImage

                  All the objects of the target category are in the essential image.

                  Given an essentially surjective functor, we can find a preimage for every object Y in the codomain. Applying the functor to this preimage will yield an object isomorphic to Y, see obj_obj_preimage_iso.

                  Equations
                  Instances For
                    def CategoryTheory.Functor.objObjPreimageIso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.EssSurj] (Y : D) :
                    F.obj (F.objPreimage Y) Y

                    Applying an essentially surjective functor to a preimage of Y yields an object that is isomorphic to Y.

                    Equations
                    Instances For

                      The induced functor of a faithful functor is faithful.

                      Equations
                      • =

                      The induced functor of a full functor is full.

                      Equations
                      • =
                      Equations
                      • =
                      @[deprecated CategoryTheory.Functor.EssSurj]

                      Alias of CategoryTheory.Functor.EssSurj.


                      A functor F : C ⥤ D is essentially surjective if every object of D is in the essential image of F. In other words, for every Y : D, there is some X : C with F.obj X ≅ Y.

                      See https://stacks.math.columbia.edu/tag/001C.

                      Equations
                      Instances For
                        @[deprecated CategoryTheory.Functor.essSurj_of_iso]

                        Alias of CategoryTheory.Functor.essSurj_of_iso.