Full and faithful functors #
We define typeclasses full and faithful, decorating functors.
Use F.map_injective to retrieve the fact that F.map is injective when [faithful F],
and F.preimage to obtain preimages of morphisms when [full F].
We prove some basic "cancellation" lemmas for full and/or faithful functors.
See category_theory.equivalence 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₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Type (max u₁ v₁ v₂)
- preimage : Π {X Y : C}, (F.obj X ⟶ F.obj Y) → (X ⟶ Y)
- witness' : (∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (category_theory.full.preimage f) = f) . "obviously"
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.
See https://stacks.math.columbia.edu/tag/001C.
Instances
- category_theory.equivalence.full_of_equivalence
- category_theory.full.id
- category_theory.full.comp
- category_theory.induced_category.full
- category_theory.full_subcategory.full
- category_theory.full_subcategory.map.full
- category_theory.full_subcategory.lift.full
- category_theory.functor.ess_image_inclusion.full
- category_theory.full.to_ess_image
- category_theory.functor.op.category_theory.full
- category_theory.ulift_functor_full
- category_theory.bundled_hom.forget₂_full
- CommRing.category_theory.forget₂.category_theory.full
@[simp]
theorem
category_theory.full.witness
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F : C ⥤ D}
[self : category_theory.full F]
{X Y : C}
(f : F.obj X ⟶ F.obj Y) :
F.map (category_theory.full.preimage f) = f
@[class]
structure
category_theory.faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D) :
Prop
- map_injective' : (∀ {X Y : C}, function.injective F.map) . "obviously"
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
- category_theory.equivalence.faithful_of_equivalence
- category_theory.faithful.id
- category_theory.faithful.comp
- category_theory.induced_category.faithful
- category_theory.full_subcategory.faithful
- category_theory.full_subcategory.map.faithful
- category_theory.full_subcategory.lift.faithful
- category_theory.faithful_whiskering_right_obj
- category_theory.functor.ess_image_inclusion.faithful
- category_theory.faithful.to_ess_image
- category_theory.functor.op.category_theory.faithful
- category_theory.functor.right_op_faithful
- category_theory.functor.left_op_faithful
- category_theory.ulift_functor_faithful
- category_theory.concrete_category.forget_faithful
- category_theory.forget_faithful
theorem
category_theory.faithful.map_injective
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[self : category_theory.faithful F]
{X Y : C} :
theorem
category_theory.functor.map_injective
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.faithful F]
{X Y : C} :
theorem
category_theory.functor.map_iso_injective
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.faithful F]
{X Y : C} :
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 : 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) :
@[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} :
@[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) :
@[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) :
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 : 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
- category_theory.preimage_iso f = {hom := F.preimage f.hom, inv := F.preimage f.inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.preimage_iso_hom
{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 : F.obj X ≅ F.obj Y) :
(category_theory.preimage_iso f).hom = F.preimage f.hom
@[simp]
theorem
category_theory.preimage_iso_inv
{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 : F.obj X ≅ F.obj Y) :
(category_theory.preimage_iso f).inv = F.preimage f.inv
@[simp]
theorem
category_theory.preimage_iso_map_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 : X ≅ Y) :
category_theory.preimage_iso (F.map_iso f) = f
theorem
category_theory.is_iso_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}
(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₁}
[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} :
If F is fully faithful, we have an equivalence of hom-sets X ⟶ Y and F X ⟶ F Y.
@[simp]
theorem
category_theory.equiv_of_fully_faithful_symm_apply
{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 : F.obj X ⟶ F.obj Y) :
⇑((category_theory.equiv_of_fully_faithful F).symm) f = F.preimage f
@[simp]
theorem
category_theory.equiv_of_fully_faithful_apply
{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) :
⇑(category_theory.equiv_of_fully_faithful F) f = F.map f
def
category_theory.iso_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} :
If F is fully faithful, we have an equivalence of iso-sets X ≅ Y and F X ≅ F Y.
@[simp]
theorem
category_theory.iso_equiv_of_fully_faithful_symm_apply
{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 : F.obj X ≅ F.obj Y) :
@[simp]
theorem
category_theory.iso_equiv_of_fully_faithful_apply
{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) :
@[simp]
theorem
category_theory.nat_trans_of_comp_fully_faithful_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u_1}
[category_theory.category E]
{F G : C ⥤ D}
(H : D ⥤ E)
[category_theory.full H]
[category_theory.faithful H]
(α : F ⋙ H ⟶ G ⋙ H)
(X : C) :
(category_theory.nat_trans_of_comp_fully_faithful H α).app X = ⇑((category_theory.equiv_of_fully_faithful H).symm) (α.app X)
def
category_theory.nat_trans_of_comp_fully_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u_1}
[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
We can construct a natural transformation between functors by constructing a natural transformation between those functors composed with a fully faithful functor.
Equations
- category_theory.nat_trans_of_comp_fully_faithful H α = {app := λ (X : C), ⇑((category_theory.equiv_of_fully_faithful H).symm) (α.app X), naturality' := _}
def
category_theory.nat_iso_of_comp_fully_faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u_1}
[category_theory.category E]
{F G : C ⥤ D}
(H : D ⥤ E)
[category_theory.full H]
[category_theory.faithful H]
(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
- category_theory.nat_iso_of_comp_fully_faithful H i = category_theory.nat_iso.of_components (λ (X : C), ⇑((category_theory.iso_equiv_of_fully_faithful H).symm) (i.app X)) _
@[simp]
theorem
category_theory.nat_iso_of_comp_fully_faithful_hom_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u_1}
[category_theory.category E]
{F G : C ⥤ D}
(H : D ⥤ E)
[category_theory.full H]
[category_theory.faithful H]
(i : F ⋙ H ≅ G ⋙ H)
(X : C) :
@[simp]
theorem
category_theory.nat_iso_of_comp_fully_faithful_inv_app
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u_1}
[category_theory.category E]
{F G : C ⥤ D}
(H : D ⥤ E)
[category_theory.full H]
[category_theory.faithful H]
(i : F ⋙ H ≅ G ⋙ H)
(X : C) :
theorem
category_theory.nat_iso_of_comp_fully_faithful_hom
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u_1}
[category_theory.category E]
{F G : C ⥤ D}
(H : D ⥤ E)
[category_theory.full H]
[category_theory.faithful H]
(i : F ⋙ H ≅ G ⋙ H) :
theorem
category_theory.nat_iso_of_comp_fully_faithful_inv
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{E : Type u_1}
[category_theory.category E]
{F G : C ⥤ D}
(H : D ⥤ E)
[category_theory.full H]
[category_theory.faithful H]
(i : F ⋙ H ≅ G ⋙ H) :
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.faithful.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]
[category_theory.faithful G] :
category_theory.faithful (F ⋙ G)
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)] :
def
category_theory.full.of_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F F' : C ⥤ D}
[category_theory.full F]
(α : F ≅ F') :
If F is full, and naturally isomorphic to some F', then F' is also full.
theorem
category_theory.faithful.of_iso
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D]
{F F' : C ⥤ D}
[category_theory.faithful F]
(α : F ≅ F') :
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]
(h : F ⋙ G ≅ H) :
theorem
category_theory.iso.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}
{H : C ⥤ E}
[ℋ : category_theory.faithful H]
(h : F ⋙ G ≅ H) :
Alias of faithful.of_comp_iso.
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]
(h : F ⋙ G = H) :
theorem
eq.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}
{H : C ⥤ E}
[ℋ : category_theory.faithful H]
(h : F ⋙ G = H) :
Alias of faithful.of_comp_eq.
@[protected]
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))
(h_map : ∀ {X Y : C} {f : X ⟶ Y}, G.map (map f) == F.map f) :
C ⥤ D
“Divide” a functor by a faithful functor.
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) :
category_theory.faithful (category_theory.faithful.div F G obj h_obj map h_map)
@[protected, 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] :
category_theory.full (F ⋙ G)
def
category_theory.full.of_comp_faithful
{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 ⋙ G)]
[category_theory.faithful G] :
If F ⋙ G is full and G is faithful, then F is full.
def
category_theory.full.of_comp_faithful_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.full H]
[category_theory.faithful G]
(h : F ⋙ G ≅ H) :
If F ⋙ G is full and G is faithful, then F is full.
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]
(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
- category_theory.fully_faithful_cancel_right H comp_iso = category_theory.nat_iso.of_components (λ (X : C), category_theory.preimage_iso (comp_iso.app X)) _
@[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) :