# mathlib3documentation

category_theory.functor.fully_faithful

# Full and faithful functors #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define typeclasses full and faithful, decorating functors.

## 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.
• full F carries data, so definitional properties of the preimage can be used when using F.preimage. To obtain an instance of full F non-constructively, you can use full_of_exists and full_of_surjective.

See category_theory.equivalence.of_fully_faithful_ess_surj for the fact that a functor is an equivalence if and only if it is fully faithful and essentially surjective.

@[class]
structure category_theory.full {C : Type u₁} {D : Type u₂} (F : C D) :
Type (max u₁ v₁ v₂)

A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective. In fact, we use a constructive definition, so the full F typeclass contains data, specifying a particular preimage of each f : F.obj X ⟶ F.obj Y.

Instances of this typeclass
Instances of other typeclasses for category_theory.full
• category_theory.full.has_sizeof_inst
@[simp]
theorem category_theory.full.witness {C : Type u₁} {D : Type u₂} {F : C D} [self : category_theory.full F] {X Y : C} (f : F.obj X F.obj Y) :
@[class]
structure category_theory.faithful {C : Type u₁} {D : Type u₂} (F : C D) :
Prop
• map_injective' : ( {X Y : C}, . "obviously"

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

Instances of this typeclass
theorem category_theory.faithful.map_injective {C : Type u₁} {D : Type u₂} (F : C D) [self : category_theory.faithful F] {X Y : C} :
theorem category_theory.functor.map_injective {C : Type u₁} {D : Type u₂} {X Y : C} (F : C D)  :
theorem category_theory.functor.map_iso_injective {C : Type u₁} {D : Type u₂} {X Y : C} (F : C D)  :
def category_theory.functor.preimage {C : Type u₁} {D : Type u₂} {X Y : C} (F : C D) (f : F.obj X F.obj Y) :
X Y

The specified preimage of a morphism under a full functor.

Equations
@[simp]
theorem category_theory.functor.image_preimage {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : F.obj X F.obj Y) :
F.map (F.preimage f) = f
theorem category_theory.functor.map_surjective {C : Type u₁} {D : Type u₂} {X Y : C} (F : C D)  :
noncomputable def category_theory.functor.full_of_exists {C : Type u₁} {D : Type u₂} (F : C D) (h : (X Y : C) (f : F.obj X F.obj Y), (p : X Y), F.map p = f) :

Deduce that F is full from the existence of preimages, using choice.

Equations
noncomputable def category_theory.functor.full_of_surjective {C : Type u₁} {D : Type u₂} (F : C D) (h : (X Y : C), ) :

Deduce that F is full from surjectivity of F.map, using choice.

Equations
@[simp]
theorem category_theory.preimage_id {C : Type u₁} {D : Type u₂} {F : C D} {X : C} :
F.preimage (𝟙 (F.obj X)) = 𝟙 X
@[simp]
theorem category_theory.preimage_comp {C : Type u₁} {D : Type u₂} {F : C D} {X Y Z : C} (f : F.obj X F.obj Y) (g : F.obj Y F.obj Z) :
F.preimage (f g) = F.preimage f F.preimage g
@[simp]
theorem category_theory.preimage_map {C : Type u₁} {D : Type u₂} {F : C D} {X Y : C} (f : X Y) :
F.preimage (F.map f) = f
@[simp]
theorem category_theory.functor.preimage_iso_hom {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : F.obj X F.obj Y) :
def category_theory.functor.preimage_iso {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (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
@[simp]
theorem category_theory.functor.preimage_iso_inv {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : F.obj X F.obj Y) :
@[simp]
theorem category_theory.functor.preimage_iso_map_iso {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : X Y) :
theorem category_theory.is_iso_of_fully_faithful {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : X Y) [category_theory.is_iso (F.map f)] :

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

def category_theory.equiv_of_fully_faithful {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} :
(X Y) (F.obj X F.obj Y)

If F is fully faithful, we have an equivalence of hom-sets X ⟶ Y and F X ⟶ F Y.

Equations
@[simp]
theorem category_theory.equiv_of_fully_faithful_symm_apply {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : F.obj X F.obj Y) :
@[simp]
theorem category_theory.equiv_of_fully_faithful_apply {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : X Y) :
def category_theory.iso_equiv_of_fully_faithful {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} :
(X Y) (F.obj X F.obj Y)

If F is fully faithful, we have an equivalence of iso-sets X ≅ Y and F X ≅ F Y.

Equations
@[simp]
theorem category_theory.iso_equiv_of_fully_faithful_symm_apply {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : F.obj X F.obj Y) :
@[simp]
theorem category_theory.iso_equiv_of_fully_faithful_apply {C : Type u₁} {D : Type u₂} (F : C D) {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.nat_trans_of_comp_fully_faithful_app {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (α : F H G H) (X : C) :
def category_theory.nat_trans_of_comp_fully_faithful {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (α : F H G H) :
F G

We can construct a natural transformation between functors by constructing a natural transformation between those functors composed with a fully faithful functor.

Equations
def category_theory.nat_iso_of_comp_fully_faithful {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (i : F H G H) :
F G

We can construct a natural isomorphism between functors by constructing a natural isomorphism between those functors composed with a fully faithful functor.

Equations
@[simp]
theorem category_theory.nat_iso_of_comp_fully_faithful_hom_app {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (i : F H G H) (X : C) :
= H.preimage (i.hom.app X)
@[simp]
theorem category_theory.nat_iso_of_comp_fully_faithful_inv_app {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (i : F H G H) (X : C) :
= H.preimage (i.inv.app X)
theorem category_theory.nat_iso_of_comp_fully_faithful_hom {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (i : F H G H) :
theorem category_theory.nat_iso_of_comp_fully_faithful_inv {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (i : F H G H) :
def category_theory.nat_trans.equiv_of_comp_fully_faithful {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E)  :
(F G) (F H G H)

Horizontal composition with a fully faithful functor induces a bijection on natural transformations.

Equations
@[simp]
theorem category_theory.nat_trans.equiv_of_comp_fully_faithful_apply {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (α : F G) :
@[simp]
theorem category_theory.nat_trans.equiv_of_comp_fully_faithful_symm_apply {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (α : F H G H) :
def category_theory.nat_iso.equiv_of_comp_fully_faithful {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E)  :
(F G) (F H G H)

Horizontal composition with a fully faithful functor induces a bijection on natural isomorphisms.

Equations
@[simp]
theorem category_theory.nat_iso.equiv_of_comp_fully_faithful_symm_apply {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (i : F H G H) :
@[simp]
theorem category_theory.nat_iso.equiv_of_comp_fully_faithful_apply {C : Type u₁} {D : Type u₂} {E : Type u_1} {F G : C D} (H : D E) (e : F G) :
@[protected, instance]
def category_theory.full.id {C : Type u₁}  :
Equations
@[protected, instance]
def category_theory.faithful.id {C : Type u₁}  :
@[protected, instance]
def category_theory.faithful.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E)  :
theorem category_theory.faithful.of_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E) [category_theory.faithful (F G)] :
def category_theory.full.of_iso {C : Type u₁} {D : Type u₂} {F F' : C D} (α : F F') :

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

Equations
theorem category_theory.faithful.of_iso {C : Type u₁} {D : Type u₂} {F F' : C D} (α : F F') :
theorem category_theory.faithful.of_comp_iso {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C D} {G : D E} {H : C E} [ℋ : category_theory.faithful H] (h : F G H) :
theorem category_theory.iso.faithful_of_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C D} {G : D E} {H : C E} [ℋ : category_theory.faithful H] (h : F G H) :

Alias of category_theory.faithful.of_comp_iso.

theorem category_theory.faithful.of_comp_eq {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C D} {G : D E} {H : C E} [ℋ : category_theory.faithful H] (h : F G = H) :
theorem eq.faithful_of_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C D} {G : D E} {H : C E} [ℋ : category_theory.faithful H] (h : F G = H) :

Alias of category_theory.faithful.of_comp_eq.

@[protected]
def category_theory.faithful.div {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C E) (G : D E) (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}, G.map (map f) == F.map f) :
C D

“Divide” a functor by a faithful functor.

Equations
theorem category_theory.faithful.div_comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C E) (G : D E) (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}, G.map (map f) == F.map f) :
obj h_obj map h_map G = F
theorem category_theory.faithful.div_faithful {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C E) (G : D E) (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}, G.map (map f) == F.map f) :
category_theory.faithful obj h_obj map h_map)
@[protected, instance]
def category_theory.full.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E)  :
Equations
def category_theory.full.of_comp_faithful {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : C D) (G : D E) [category_theory.full (F G)]  :

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

Equations
def category_theory.full.of_comp_faithful_iso {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : C D} {G : D E} {H : C E} (h : F G H) :

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

Equations
def category_theory.fully_faithful_cancel_right {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D} (H : D E) (comp_iso : F H G 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
@[simp]
theorem category_theory.fully_faithful_cancel_right_hom_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D} {H : D E} (comp_iso : F H G H) (X : C) :
comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)
@[simp]
theorem category_theory.fully_faithful_cancel_right_inv_app {C : Type u₁} {D : Type u₂} {E : Type u₃} {F G : C D} {H : D E} (comp_iso : F H G H) (X : C) :
comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)