Documentation

Mathlib.CategoryTheory.Functor.FullyFaithful

Full and faithful functors #

We define typeclasses Full and Faithful, decorating functors. These typeclasses carry no data. However, we also introduce a structure Functor.FullyFaithful which contains the data of the inverse map (F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y) of the map induced on morphisms by a functor F.

Main definitions and results #

See CategoryTheory.Equivalence.of_fullyFaithful_ess_surj for the fact that a functor is an equivalence if and only if it is fully faithful and essentially surjective.

A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective.

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

Instances

    A functor F : C ⥤ D is faithful if for each X Y : C, F.map is injective.

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

    • map_injective : ∀ {X Y : C}, Function.Injective F.map

      F.map is injective for each X Y : C.

    Instances
      theorem CategoryTheory.Functor.Faithful.map_injective {C : Type u₁} :
      ∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D} {F : CategoryTheory.Functor C D} [self : F.Faithful] {X Y : C}, Function.Injective F.map

      F.map is injective for each X Y : C.

      theorem CategoryTheory.Functor.map_injective_iff {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Faithful] {X : C} {Y : C} (f : X Y) (g : X Y) :
      F.map f = F.map g f = g
      noncomputable def CategoryTheory.Functor.preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {X : C} {Y : C} (F : CategoryTheory.Functor C D) [F.Full] (f : F.obj X F.obj Y) :
      X Y

      The choice of a preimage of a morphism under a full functor.

      Equations
      • F.preimage f = .choose
      Instances For
        @[simp]
        theorem CategoryTheory.Functor.map_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Full] {X : C} {Y : C} (f : F.obj X F.obj Y) :
        F.map (F.preimage f) = f
        @[simp]
        theorem CategoryTheory.Functor.preimage_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C} {Y : C} {Z : C} [F.Full] [F.Faithful] (f : F.obj X F.obj Y) (g : F.obj Y F.obj Z) :
        F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)
        @[simp]
        theorem CategoryTheory.Functor.preimage_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C} {Y : C} [F.Full] [F.Faithful] (f : X Y) :
        F.preimage (F.map f) = f
        @[simp]
        theorem CategoryTheory.Functor.preimageIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} [F.Full] [F.Faithful] (f : F.obj X F.obj Y) :
        (F.preimageIso f).inv = F.preimage f.inv
        @[simp]
        theorem CategoryTheory.Functor.preimageIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} [F.Full] [F.Faithful] (f : F.obj X F.obj Y) :
        (F.preimageIso f).hom = F.preimage f.hom
        noncomputable def CategoryTheory.Functor.preimageIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} [F.Full] [F.Faithful] (f : F.obj X F.obj Y) :
        X Y

        If F : C ⥤ D is fully faithful, every isomorphism F.obj X ≅ F.obj Y has a preimage.

        Equations
        • F.preimageIso f = { hom := F.preimage f.hom, inv := F.preimage f.inv, hom_inv_id := , inv_hom_id := }
        Instances For
          @[simp]
          theorem CategoryTheory.Functor.preimageIso_mapIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) {X : C} {Y : C} [F.Full] [F.Faithful] (f : X Y) :
          F.preimageIso (F.mapIso f) = f

          Structure containing the data of inverse map (F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y) of F.map in order to express that F is a fully faithful functor.

          • preimage : {X Y : C} → (F.obj X F.obj Y)(X Y)

            The inverse map (F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y) of F.map.

          • map_preimage : ∀ {X Y : C} (f : F.obj X F.obj Y), F.map (self.preimage f) = f
          • preimage_map : ∀ {X Y : C} (f : X Y), self.preimage (F.map f) = f
          Instances For
            @[simp]
            theorem CategoryTheory.Functor.FullyFaithful.map_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (self : F.FullyFaithful) {X : C} {Y : C} (f : F.obj X F.obj Y) :
            F.map (self.preimage f) = f
            @[simp]
            theorem CategoryTheory.Functor.FullyFaithful.preimage_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (self : F.FullyFaithful) {X : C} {Y : C} (f : X Y) :
            self.preimage (F.map f) = f

            A FullyFaithful structure can be obtained from the assumption the F is both full and faithful.

            Equations
            Instances For

              The identity functor is fully faithful.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.Functor.FullyFaithful.homEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} :
                ∀ (a : X Y), hF.homEquiv a = F.map a
                @[simp]
                theorem CategoryTheory.Functor.FullyFaithful.homEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} (f : F.obj X F.obj Y) :
                hF.homEquiv.symm f = hF.preimage f
                def CategoryTheory.Functor.FullyFaithful.homEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} :
                (X Y) (F.obj X F.obj Y)

                The equivalence (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y) given by h : F.FullyFaithful.

                Equations
                • hF.homEquiv = { toFun := F.map, invFun := hF.preimage, left_inv := , right_inv := }
                Instances For
                  theorem CategoryTheory.Functor.FullyFaithful.map_injective {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} {f : X Y} {g : X Y} (h : F.map f = F.map g) :
                  f = g
                  @[simp]
                  theorem CategoryTheory.Functor.FullyFaithful.preimageIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} (e : F.obj X F.obj Y) :
                  (hF.preimageIso e).inv = hF.preimage e.inv
                  @[simp]
                  theorem CategoryTheory.Functor.FullyFaithful.preimageIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} (e : F.obj X F.obj Y) :
                  (hF.preimageIso e).hom = hF.preimage e.hom
                  def CategoryTheory.Functor.FullyFaithful.preimageIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} (e : F.obj X F.obj Y) :
                  X Y

                  The unique isomorphism X ≅ Y which induces an isomorphism F.obj X ≅ F.obj Y when hF : F.FullyFaithful.

                  Equations
                  • hF.preimageIso e = { hom := hF.preimage e.hom, inv := hF.preimage e.inv, hom_inv_id := , inv_hom_id := }
                  Instances For
                    @[simp]
                    theorem CategoryTheory.Functor.FullyFaithful.isoEquiv_symm_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} (e : F.obj X F.obj Y) :
                    hF.isoEquiv.symm e = hF.preimageIso e
                    @[simp]
                    theorem CategoryTheory.Functor.FullyFaithful.isoEquiv_apply {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} (i : X Y) :
                    hF.isoEquiv i = F.mapIso i
                    def CategoryTheory.Functor.FullyFaithful.isoEquiv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {X : C} {Y : C} :
                    (X Y) (F.obj X F.obj Y)

                    The equivalence (X ≅ Y) ≃ (F.obj X ≅ F.obj Y) given by h : F.FullyFaithful.

                    Equations
                    • hF.isoEquiv = { toFun := F.mapIso, invFun := hF.preimageIso, left_inv := , right_inv := }
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Functor.FullyFaithful.comp_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {G : CategoryTheory.Functor D E} (hG : G.FullyFaithful) :
                      ∀ {X Y : C} (f : (F.comp G).obj X (F.comp G).obj Y), (hF.comp hG).preimage f = hF.preimage (hG.preimage f)
                      def CategoryTheory.Functor.FullyFaithful.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u_1} [CategoryTheory.Category.{u_2, u_1} E] {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) {G : CategoryTheory.Functor D E} (hG : G.FullyFaithful) :
                      (F.comp G).FullyFaithful

                      Fully faithful functors are stable by composition.

                      Equations
                      • hF.comp hG = { preimage := fun {X Y : C} (f : (F.comp G).obj X (F.comp G).obj Y) => hF.preimage (hG.preimage f), map_preimage := , preimage_map := }
                      Instances For

                        If F ⋙ G is fully faithful and G is faithful, then F is fully faithful.

                        Equations
                        • hFG.ofCompFaithful = { preimage := fun {X Y : C} (f : F.obj X F.obj Y) => hFG.preimage (G.map f), map_preimage := , preimage_map := }
                        Instances For

                          If the image of a morphism under a fully faithful functor in an isomorphism, then the original morphisms is also an isomorphism.

                          Equations
                          • =

                          If F is full, and naturally isomorphic to some F', then F' is also full.

                          def CategoryTheory.Functor.Faithful.div {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) (G : CategoryTheory.Functor D E) [G.Faithful] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y)(obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map f)) (F.map f)) :

                          “Divide” a functor by a faithful functor.

                          Equations
                          Instances For
                            theorem CategoryTheory.Functor.Faithful.div_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) [F.Faithful] (G : CategoryTheory.Functor D E) [G.Faithful] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y)(obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map f)) (F.map f)) :
                            (CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).comp G = F
                            theorem CategoryTheory.Functor.Faithful.div_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) [F.Faithful] (G : CategoryTheory.Functor D E) [G.Faithful] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y)(obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map f)) (F.map f)) :
                            (CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).Faithful

                            If F ⋙ G is full and G is faithful, then F is full.

                            If F ⋙ G is full and G is faithful, then F is full.

                            noncomputable def CategoryTheory.Functor.fullyFaithfulCancelRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} (H : CategoryTheory.Functor D E) [H.Full] [H.Faithful] (comp_iso : F.comp H G.comp H) :
                            F G

                            Given a natural isomorphism between F ⋙ H and G ⋙ H for a fully faithful functor H, we can 'cancel' it to give a natural iso between F and G.

                            Equations
                            Instances For
                              @[simp]
                              theorem CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [H.Full] [H.Faithful] (comp_iso : F.comp H G.comp H) (X : C) :
                              (CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)
                              @[simp]
                              theorem CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [H.Full] [H.Faithful] (comp_iso : F.comp H G.comp H) (X : C) :
                              (CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)
                              @[deprecated CategoryTheory.Functor.Full]

                              Alias of CategoryTheory.Functor.Full.


                              A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective.

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

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

                                Alias of CategoryTheory.Functor.Faithful.


                                A functor F : C ⥤ D is faithful if for each X Y : C, F.map is injective.

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

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

                                  Alias of CategoryTheory.Functor.preimage_id.

                                  @[deprecated CategoryTheory.Functor.preimage_comp]
                                  theorem CategoryTheory.preimage_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C} {Y : C} {Z : C} [F.Full] [F.Faithful] (f : F.obj X F.obj Y) (g : F.obj Y F.obj Z) :
                                  F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)

                                  Alias of CategoryTheory.Functor.preimage_comp.

                                  @[deprecated CategoryTheory.Functor.preimage_map]
                                  theorem CategoryTheory.preimage_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {F : CategoryTheory.Functor C D} {X : C} {Y : C} [F.Full] [F.Faithful] (f : X Y) :
                                  F.preimage (F.map f) = f

                                  Alias of CategoryTheory.Functor.preimage_map.

                                  @[deprecated CategoryTheory.Functor.Faithful.of_comp]

                                  Alias of CategoryTheory.Functor.Faithful.of_comp.

                                  @[deprecated CategoryTheory.Functor.Full.of_iso]

                                  Alias of CategoryTheory.Functor.Full.of_iso.


                                  If F is full, and naturally isomorphic to some F', then F' is also full.

                                  @[deprecated CategoryTheory.Functor.Faithful.of_iso]

                                  Alias of CategoryTheory.Functor.Faithful.of_iso.

                                  @[deprecated CategoryTheory.Functor.Faithful.of_comp_iso]

                                  Alias of CategoryTheory.Functor.Faithful.of_comp_iso.

                                  @[deprecated CategoryTheory.Functor.Faithful.of_comp_eq]

                                  Alias of CategoryTheory.Functor.Faithful.of_comp_eq.

                                  @[deprecated CategoryTheory.Functor.Faithful.div]
                                  def CategoryTheory.Faithful.div {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) (G : CategoryTheory.Functor D E) [G.Faithful] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y)(obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map f)) (F.map f)) :

                                  Alias of CategoryTheory.Functor.Faithful.div.


                                  “Divide” a functor by a faithful functor.

                                  Equations
                                  Instances For
                                    @[deprecated CategoryTheory.Functor.Faithful.div_comp]
                                    theorem CategoryTheory.Faithful.div_comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) [F.Faithful] (G : CategoryTheory.Functor D E) [G.Faithful] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y)(obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map f)) (F.map f)) :
                                    (CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).comp G = F

                                    Alias of CategoryTheory.Functor.Faithful.div_comp.

                                    @[deprecated CategoryTheory.Functor.Faithful.div_faithful]
                                    theorem CategoryTheory.Faithful.div_faithful {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C E) [F.Faithful] (G : CategoryTheory.Functor D E) [G.Faithful] (obj : CD) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : {X Y : C} → (X Y)(obj X obj Y)) (h_map : ∀ {X Y : C} {f : X Y}, HEq (G.map (map f)) (F.map f)) :
                                    (CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).Faithful

                                    Alias of CategoryTheory.Functor.Faithful.div_faithful.

                                    @[deprecated CategoryTheory.Functor.Full.of_comp_faithful]

                                    Alias of CategoryTheory.Functor.Full.of_comp_faithful.


                                    If F ⋙ G is full and G is faithful, then F is full.

                                    @[deprecated CategoryTheory.Functor.Full.of_comp_faithful_iso]

                                    Alias of CategoryTheory.Functor.Full.of_comp_faithful_iso.


                                    If F ⋙ G is full and G is faithful, then F is full.

                                    @[deprecated CategoryTheory.Functor.fullyFaithfulCancelRight]

                                    Alias of CategoryTheory.Functor.fullyFaithfulCancelRight.


                                    Given a natural isomorphism between F ⋙ H and G ⋙ H for a fully faithful functor H, we can 'cancel' it to give a natural iso between F and G.

                                    Equations
                                    Instances For
                                      @[deprecated CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app]
                                      theorem CategoryTheory.fullyFaithfulCancelRight_hom_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [H.Full] [H.Faithful] (comp_iso : F.comp H G.comp H) (X : C) :
                                      (CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)

                                      Alias of CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app.

                                      @[deprecated CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app]
                                      theorem CategoryTheory.fullyFaithfulCancelRight_inv_app {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor D E} [H.Full] [H.Faithful] (comp_iso : F.comp H G.comp H) (X : C) :
                                      (CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)

                                      Alias of CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app.

                                      @[deprecated CategoryTheory.Functor.map_preimage]
                                      theorem CategoryTheory.Functor.image_preimage {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (F : CategoryTheory.Functor C D) [F.Full] {X : C} {Y : C} (f : F.obj X F.obj Y) :
                                      F.map (F.preimage f) = f

                                      Alias of CategoryTheory.Functor.map_preimage.