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

• Use F.map_injective to retrieve the fact that F.map is injective when [Faithful F].
• Similarly, F.map_surjective states that F.map is surjective when [Full F].
• Use F.preimage to obtain preimages of morphisms when [Full F].
• We prove some basic "cancellation" lemmas for full and/or faithful functors, as well as a construction for "dividing" a functor by a faithful functor, see Faithful.div.

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.

class CategoryTheory.Functor.Full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

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

• map_surjective {X Y : C} : Function.Surjective F.map

class CategoryTheory.Functor.Faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Prop

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

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

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

theorem CategoryTheory.Functor.map_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} (F : Functor C D) [F.Faithful] : Function.Injective F.map

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

theorem CategoryTheory.Functor.mapIso_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} (F : Functor C D) [F.Faithful] : Function.Injective F.mapIso

theorem CategoryTheory.Functor.map_surjective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} (F : Functor C D) [F.Full] : Function.Surjective F.map

noncomputable def CategoryTheory.Functor.preimage {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {X Y : C} (F : 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

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.preimage_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} {X : C} [F.Full] [F.Faithful] : F.preimage (CategoryStruct.id (F.obj X)) = CategoryStruct.id X

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Functor.preimageIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X 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 := ⋯ }

@[simp]

theorem CategoryTheory.Functor.preimageIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} [F.Full] [F.Faithful] (f : F.obj X ≅ F.obj Y) : (F.preimageIso f).hom = F.preimage f.hom

@[simp]

theorem CategoryTheory.Functor.preimageIso_mapIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {X Y : C} [F.Full] [F.Faithful] (f : X ≅ Y) : F.preimageIso (F.mapIso f) = f

structure CategoryTheory.Functor.FullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) : Type (max (max u₁ v₁) v₂)

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 : 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

noncomputable def CategoryTheory.Functor.FullyFaithful.ofFullyFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] [F.Faithful] : F.FullyFaithful

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

Equations

• CategoryTheory.Functor.FullyFaithful.ofFullyFaithful F = { preimage := fun {X Y : C} => F.preimage, map_preimage := ⋯, preimage_map := ⋯ }

def CategoryTheory.Functor.FullyFaithful.id (C : Type u₁) [Category.{v₁, u₁} C] : (Functor.id C).FullyFaithful

The identity functor is fully faithful.

Equations

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

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.id_preimage (C : Type u₁) [Category.{v₁, u₁} C] {X✝ Y✝ : C} (f : (Functor.id C).obj X✝ ⟶ (Functor.id C).obj Y✝) : (id C).preimage f = f

def CategoryTheory.Functor.FullyFaithful.homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X 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 := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y : C} (a✝ : X ⟶ Y) : hF.homEquiv a✝ = F.map a✝

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.homEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y : C} (f : F.obj X ⟶ F.obj Y) : hF.homEquiv.symm f = hF.preimage f

theorem CategoryTheory.Functor.FullyFaithful.map_injective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y : C} {f g : X ⟶ Y} (h : F.map f = F.map g) : f = g

theorem CategoryTheory.Functor.FullyFaithful.map_surjective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y : C} : Function.Surjective F.map

theorem CategoryTheory.Functor.FullyFaithful.map_bijective {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) (X Y : C) : Function.Bijective F.map

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.preimage_id {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X : C} : hF.preimage (CategoryStruct.id (F.obj X)) = CategoryStruct.id X

@[simp]

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

theorem CategoryTheory.Functor.FullyFaithful.preimage_comp_assoc {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y Z : C} (f : F.obj X ⟶ F.obj Y) (g : F.obj Y ⟶ F.obj Z) {Z✝ : C} (h : Z ⟶ Z✝) : CategoryStruct.comp (hF.preimage (CategoryStruct.comp f g)) h = CategoryStruct.comp (hF.preimage f) (CategoryStruct.comp (hF.preimage g) h)

theorem CategoryTheory.Functor.FullyFaithful.full {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) : F.Full

theorem CategoryTheory.Functor.FullyFaithful.faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) : F.Faithful

instance CategoryTheory.Functor.FullyFaithful.instSubsingleton {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} : Subsingleton F.FullyFaithful

def CategoryTheory.Functor.FullyFaithful.preimageIso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X 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 := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.preimageIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X 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₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y) : (hF.preimageIso e).hom = hF.preimage e.hom

theorem CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y : C} (f : X ⟶ Y) [IsIso (F.map f)] : IsIso f

def CategoryTheory.Functor.FullyFaithful.isoEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X 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 := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.isoEquiv_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y : C} (i : X ≅ Y) : hF.isoEquiv i = F.mapIso i

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.isoEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F : Functor C D} (hF : F.FullyFaithful) {X Y : C} (e : F.obj X ≅ F.obj Y) : hF.isoEquiv.symm e = hF.preimageIso e

def CategoryTheory.Functor.FullyFaithful.comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] {F : Functor C D} (hF : F.FullyFaithful) {G : 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 := ⋯ }

@[simp]

theorem CategoryTheory.Functor.FullyFaithful.comp_preimage {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] {F : Functor C D} (hF : F.FullyFaithful) {G : 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.ofCompFaithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u_1} [Category.{u_2, u_1} E] {F : Functor C D} {G : Functor D E} [G.Faithful] (hFG : (F.comp G).FullyFaithful) : F.FullyFaithful

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 := ⋯ }

theorem CategoryTheory.isIso_of_fully_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [F.Full] [F.Faithful] {X Y : C} (f : X ⟶ Y) [IsIso (F.map f)] : IsIso f

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

instance CategoryTheory.Functor.Full.id {C : Type u₁} [Category.{v₁, u₁} C] : (Functor.id C).Full

instance CategoryTheory.Functor.Faithful.id {C : Type u₁} [Category.{v₁, u₁} C] : (Functor.id C).Faithful

instance CategoryTheory.Functor.Faithful.comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [F.Faithful] [G.Faithful] : (F.comp G).Faithful

theorem CategoryTheory.Functor.Faithful.of_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [(F.comp G).Faithful] : F.Faithful

@[instance 100]

instance CategoryTheory.Functor.instFaithfulOfIsThin {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) [Quiver.IsThin C] : F.Faithful

theorem CategoryTheory.Functor.Full.of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} [F.Full] (α : F ≅ F') : F'.Full

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

theorem CategoryTheory.Functor.Faithful.of_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {F F' : Functor C D} [F.Faithful] (α : F ≅ F') : F'.Faithful

theorem CategoryTheory.Functor.Faithful.of_comp_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} {H : Functor C E} [H.Faithful] (h : F.comp G ≅ H) : F.Faithful

theorem CategoryTheory.Iso.faithful_of_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} {H : Functor C E} [H.Faithful] (h : F.comp G ≅ H) : F.Faithful

Alias of CategoryTheory.Functor.Faithful.of_comp_iso.

theorem CategoryTheory.Functor.Faithful.of_comp_eq {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} {H : Functor C E} [ℋ : H.Faithful] (h : F.comp G = H) : F.Faithful

theorem Eq.faithful_of_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 D} {G : CategoryTheory.Functor D E} {H : CategoryTheory.Functor C E} [ℋ : H.Faithful] (h : F.comp G = H) : F.Faithful

Alias of CategoryTheory.Functor.Faithful.of_comp_eq.

def CategoryTheory.Functor.Faithful.div {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) (G : Functor D E) [G.Faithful] (obj : C → D) (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)) : Functor C D

“Divide” a functor by a faithful functor.

Equations

• CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map = { obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }

theorem CategoryTheory.Functor.Faithful.div_comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) [F.Faithful] (G : Functor D E) [G.Faithful] (obj : C → D) (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)) : (Faithful.div F G obj h_obj map h_map).comp G = F

theorem CategoryTheory.Functor.Faithful.div_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C E) [F.Faithful] (G : Functor D E) [G.Faithful] (obj : C → D) (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)) : (Faithful.div F G obj h_obj map h_map).Faithful

instance CategoryTheory.Functor.Full.comp {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [F.Full] [G.Full] : (F.comp G).Full

theorem CategoryTheory.Functor.Full.of_comp_faithful {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] (F : Functor C D) (G : Functor D E) [(F.comp G).Full] [G.Faithful] : F.Full

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

theorem CategoryTheory.Functor.Full.of_comp_faithful_iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F : Functor C D} {G : Functor D E} {H : Functor C E} [H.Full] [G.Faithful] (h : F.comp G ≅ H) : F.Full

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

noncomputable def CategoryTheory.Functor.fullyFaithfulCancelRight {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] {E : Type u₃} [Category.{v₃, u₃} E] {F G : Functor C D} (H : 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

• CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso = CategoryTheory.NatIso.ofComponents (fun (X : C) => H.preimageIso (comp_iso.app X)) ⋯

@[simp]

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

@[simp]

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