# Documentation

Mathlib.CategoryTheory.Functor.FullyFaithful

# Full and faithful functors #

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 fullOfExists and fullOfSurjective.

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.Full {C : Type u₁} [] {D : Type u₂} [] (F : ) :
Type (max (max u₁ v₁) v₂)
• preimage : {X Y : C} → (F.obj X F.obj Y) → (X Y)

The data of a preimage for every f : F.obj X ⟶ F.obj Y.

• witness : ∀ {X Y : C} (f : F.obj X F.obj Y), F.map () = f

The property that Full.preimage f of maps to f via F.map.

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
class CategoryTheory.Faithful {C : Type u₁} [] {D : Type u₂} [] (F : ) :
• map_injective : ∀ {X Y : C}, Function.Injective F.map

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

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

Instances
theorem CategoryTheory.Functor.map_injective {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (F : ) :
theorem CategoryTheory.Functor.mapIso_injective {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (F : ) :
def CategoryTheory.Functor.preimage {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (F : ) (f : F.obj X F.obj Y) :
X Y

The specified preimage of a morphism under a full functor.

Instances For
@[simp]
theorem CategoryTheory.Functor.image_preimage {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : F.obj X F.obj Y) :
F.map (F.preimage f) = f
theorem CategoryTheory.Functor.map_surjective {C : Type u₁} [] {D : Type u₂} [] {X : C} {Y : C} (F : ) :
noncomputable def CategoryTheory.Functor.fullOfExists {C : Type u₁} [] {D : Type u₂} [] (F : ) (h : ∀ (X Y : C) (f : F.obj X F.obj Y), p, F.map p = f) :

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

Instances For
noncomputable def CategoryTheory.Functor.fullOfSurjective {C : Type u₁} [] {D : Type u₂} [] (F : ) (h : ∀ (X Y : C), Function.Surjective F.map) :

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

Instances For
@[simp]
theorem CategoryTheory.preimage_id {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} :
F.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) =
@[simp]
theorem CategoryTheory.preimage_comp {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} {Y : C} {Z : C} (f : F.obj X F.obj Y) (g : F.obj Y F.obj Z) :
F.preimage () = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)
@[simp]
theorem CategoryTheory.preimage_map {C : Type u₁} [] {D : Type u₂} [] {F : } {X : C} {Y : C} (f : X Y) :
F.preimage (F.map f) = f
@[simp]
theorem CategoryTheory.Functor.preimageIso_inv {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : F.obj X F.obj Y) :
().inv = F.preimage f.inv
@[simp]
theorem CategoryTheory.Functor.preimageIso_hom {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : F.obj X F.obj Y) :
().hom = F.preimage f.hom
def CategoryTheory.Functor.preimageIso {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {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.

Instances For
@[simp]
theorem CategoryTheory.Functor.preimageIso_mapIso {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : X Y) :
theorem CategoryTheory.isIso_of_fully_faithful {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : X Y) [CategoryTheory.IsIso (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.

@[simp]
theorem CategoryTheory.equivOfFullyFaithful_symm_apply {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : F.obj X F.obj Y) :
().symm f = F.preimage f
@[simp]
theorem CategoryTheory.equivOfFullyFaithful_apply {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : X Y) :
= F.map f
def CategoryTheory.equivOfFullyFaithful {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {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.

Instances For
@[simp]
theorem CategoryTheory.isoEquivOfFullyFaithful_apply {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : X Y) :
= F.mapIso f
@[simp]
theorem CategoryTheory.isoEquivOfFullyFaithful_symm_apply {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {Y : C} (f : F.obj X F.obj Y) :
def CategoryTheory.isoEquivOfFullyFaithful {C : Type u₁} [] {D : Type u₂} [] (F : ) {X : C} {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.

Instances For
@[simp]
theorem CategoryTheory.natTransOfCompFullyFaithful_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (α : ) (X : C) :
().app X = ().symm (α.app X)
def CategoryTheory.natTransOfCompFullyFaithful {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {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.

Instances For
@[simp]
theorem CategoryTheory.natIsoOfCompFullyFaithful_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (i : ) (X : C) :
().hom.app X = H.preimage (i.hom.app X)
@[simp]
theorem CategoryTheory.natIsoOfCompFullyFaithful_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (i : ) (X : C) :
().inv.app X = H.preimage (i.inv.app X)
def CategoryTheory.natIsoOfCompFullyFaithful {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (i : ) :
F G

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

Instances For
theorem CategoryTheory.natIsoOfCompFullyFaithful_hom {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (i : ) :
theorem CategoryTheory.natIsoOfCompFullyFaithful_inv {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (i : ) :
@[simp]
theorem CategoryTheory.NatTrans.equivOfCompFullyFaithful_apply {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (α : F G) :
@[simp]
theorem CategoryTheory.NatTrans.equivOfCompFullyFaithful_symm_apply {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (α : ) :
def CategoryTheory.NatTrans.equivOfCompFullyFaithful {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) :
(F G) ()

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

Instances For
@[simp]
theorem CategoryTheory.NatIso.equivOfCompFullyFaithful_apply {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (e : F G) :
@[simp]
theorem CategoryTheory.NatIso.equivOfCompFullyFaithful_symm_apply {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) (i : ) :
def CategoryTheory.NatIso.equivOfCompFullyFaithful {C : Type u₁} [] {D : Type u₂} [] {E : Type u_1} [] {F : } {G : } (H : ) :
(F G) ()

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

Instances For
instance CategoryTheory.Full.id {C : Type u₁} [] :
instance CategoryTheory.Faithful.id {C : Type u₁} [] :
instance CategoryTheory.Faithful.comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
theorem CategoryTheory.Faithful.of_comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
def CategoryTheory.Full.ofIso {C : Type u₁} [] {D : Type u₂} [] {F : } {F' : } (α : F F') :

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

Instances For
theorem CategoryTheory.Faithful.of_iso {C : Type u₁} [] {D : Type u₂} [] {F : } {F' : } (α : F F') :
theorem CategoryTheory.Faithful.of_comp_iso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (h : ) :
theorem CategoryTheory.Iso.faithful_of_comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (h : ) :

Alias of CategoryTheory.Faithful.of_comp_iso.

theorem CategoryTheory.Faithful.of_comp_eq {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [ℋ : ] (h : ) :
theorem Eq.faithful_of_comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } [ℋ : ] (h : ) :

Alias of CategoryTheory.Faithful.of_comp_eq.

def CategoryTheory.Faithful.div {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (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 X Y f)) (F.map f)) :

“Divide” a functor by a faithful functor.

Instances For
theorem CategoryTheory.Faithful.div_comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (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 X Y f)) (F.map f)) :
theorem CategoryTheory.Faithful.div_faithful {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (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 X Y f)) (F.map f)) :
instance CategoryTheory.Full.comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
def CategoryTheory.Full.ofCompFaithful {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :

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

Instances For
def CategoryTheory.Full.ofCompFaithfulIso {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (h : ) :

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

Instances For
def CategoryTheory.fullyFaithfulCancelRight {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } (H : ) (comp_iso : ) :
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.

Instances For
@[simp]
theorem CategoryTheory.fullyFaithfulCancelRight_hom_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (comp_iso : ) (X : C) :
().hom.app X = H.preimage (comp_iso.hom.app X)
@[simp]
theorem CategoryTheory.fullyFaithfulCancelRight_inv_app {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] {F : } {G : } {H : } (comp_iso : ) (X : C) :
().inv.app X = H.preimage (comp_iso.inv.app X)