@[class]
structure
category_theory.full
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
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.
Instances
- category_theory.equivalence.full_of_equivalence
- category_theory.reflective.to_full
- category_theory.full.id
- category_theory.full.comp
- category_theory.ulift_functor_full
- category_theory.functor.category_theory.full
- category_theory.induced_category.full
- category_theory.full_subcategory.full
- category_theory.bundled_hom.forget₂_full
- CommRing.category_theory.full
- category_theory.yoneda.yoneda_full
- category_theory.coyoneda.coyoneda_full
- category_theory.limits.cones.functoriality_full
- category_theory.limits.cocones.functoriality_full
- category_theory.forget₂.category_theory.full
- Mon.to_Cat_full
- category_theory.Groupoid.forget_to_Cat_full
- category_theory.reflective.comparison_full
- Top.sheaf.forget.full
@[class]
structure
category_theory.faithful
{C : Type u₁}
[category_theory.category C]
{D : Type u₂}
[category_theory.category D] :
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.
Instances
- category_theory.equivalence.faithful_of_equivalence
- category_theory.reflective.to_faithful
- category_theory.faithful.id
- category_theory.faithful.comp
- category_theory.ulift_functor_faithful
- category_theory.functor.category_theory.faithful
- category_theory.functor.right_op_faithful
- category_theory.functor.left_op_faithful
- category_theory.induced_category.faithful
- category_theory.full_subcategory.faithful
- category_theory.concrete_category.forget_faithful
- category_theory.forget_faithful
- category_theory.yoneda.yoneda_faithful
- category_theory.coyoneda.coyoneda_faithful
- category_theory.limits.cones.functoriality_faithful
- category_theory.limits.cocones.functoriality_faithful
- category_theory.monoidal_category.category_theory.faithful
- category_theory.graded_object.category_theory.faithful
- category_theory.differential_object.forget_faithful
- Mon.to_Cat_faithful
- category_theory.Groupoid.forget_to_Cat_faithful
- category_theory.reflective.comparison_faithful
- Top.sheaf.forget.faithful
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} :
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} :
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} :
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
def
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.
Equations
- category_theory.is_iso_of_fully_faithful F f = {inv := F.preimage (category_theory.is_iso.inv (F.map f)), hom_inv_id' := _, inv_hom_id' := _}
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_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
@[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
@[instance]
@[instance]
Equations
@[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)
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_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') → category_theory.faithful 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] :
(F ⋙ G ≅ H) → category_theory.faithful F
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] :
F ⋙ G = H → category_theory.faithful F
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)) :
“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)
@[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.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] :
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) :