mathlib documentation

category_theory.fully_faithful

@[class]
structure category_theory.faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] :
C D → Prop

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.

Instances
def category_theory.functor.preimage {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) [category_theory.full F] {X Y : C} :
(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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) [category_theory.full F] {X Y : C} (f : F.obj X F.obj Y) :
F.map (F.preimage f) = f

@[simp]
theorem category_theory.preimage_id {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} [category_theory.full F] [category_theory.faithful F] {X : C} :
F.preimage (𝟙 (F.obj X)) = 𝟙 X

@[simp]
theorem category_theory.preimage_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} [category_theory.full F] [category_theory.faithful F] {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} [category_theory.full F] [category_theory.faithful F] {X Y : C} (f : X Y) :
F.preimage (F.map f) = f

def category_theory.preimage_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {F : C D} [category_theory.full F] [category_theory.faithful F] {X Y : C} :
(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]

@[simp]

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

Equations
def category_theory.equiv_of_fully_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (F : C D) [category_theory.full F] [category_theory.faithful F] {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
@[instance]

Equations
theorem category_theory.faithful.of_comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D) (G : D E) [category_theory.faithful (F G)] :

theorem category_theory.faithful.of_comp_iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C D} {G : D E} {H : C E} [ℋ : category_theory.faithful H] :

theorem category_theory.faithful.of_comp_eq {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F : C D} {G : D E} {H : C E} [ℋ : category_theory.faithful H] :

def category_theory.faithful.div {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C E) (G : D E) [category_theory.faithful G] (obj : C → D) (h_obj : ∀ (X : C), G.obj (obj X) = F.obj X) (map : Π {X Y : C}, (X Y)(obj X obj Y)) :
(∀ {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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C E) [category_theory.faithful F] (G : D E) [category_theory.faithful G] (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.div F G obj h_obj map h_map G = F

theorem category_theory.faithful.div_faithful {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C E) [category_theory.faithful F] (G : D E) [category_theory.faithful G] (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) :

@[instance]
def category_theory.full.comp {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] (F : C D) (G : D E) [category_theory.full F] [category_theory.full G] :

Equations
def category_theory.fully_faithful_cancel_right {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C D} (H : D E) [category_theory.full H] [category_theory.faithful H] :
(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₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C D} {H : D E} [category_theory.full H] [category_theory.faithful H] (comp_iso : F H G H) (X : C) :

@[simp]
theorem category_theory.fully_faithful_cancel_right_inv_app {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] {E : Type u₃} [category_theory.category E] {F G : C D} {H : D E} [category_theory.full H] [category_theory.faithful H] (comp_iso : F H G H) (X : C) :