Full and faithful functors #
We define typeclasses Full and Faithful, decorating functors. These typeclasses
carry no data. However, we also introduce a structure Functor.FullyFaithful which
contains the data of the inverse map (F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y) of the
map induced on morphisms by a functor F.
Main definitions and results #
- Use
F.map_injectiveto retrieve the fact thatF.mapis injective when[Faithful F]. - Similarly,
F.map_surjectivestates thatF.mapis surjective when[Full F]. - Use
F.preimageto 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.
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.Functor.Full
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective.
See https://stacks.math.columbia.edu/tag/001C.
- map_surjective : ∀ {X Y : C}, Function.Surjective F.map
Instances
theorem
CategoryTheory.Functor.Full.map_surjective
{C : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
{F : CategoryTheory.Functor C D} [self : F.Full] {X Y : C}, Function.Surjective F.map
class
CategoryTheory.Functor.Faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
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.
- map_injective : ∀ {X Y : C}, Function.Injective F.map
F.mapis injective for eachX Y : C.
Instances
theorem
CategoryTheory.Functor.Faithful.map_injective
{C : Type u₁}
:
∀ {inst : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst_1 : CategoryTheory.Category.{v₂, u₂} D}
{F : CategoryTheory.Functor C D} [self : F.Faithful] {X Y : C}, Function.Injective F.map
F.map is injective for each X Y : C.
theorem
CategoryTheory.Functor.map_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
(F : CategoryTheory.Functor C D)
[F.Faithful]
:
Function.Injective F.map
theorem
CategoryTheory.Functor.map_injective_iff
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Faithful]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
:
theorem
CategoryTheory.Functor.mapIso_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
(F : CategoryTheory.Functor C D)
[F.Faithful]
:
Function.Injective F.mapIso
theorem
CategoryTheory.Functor.map_surjective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
(F : CategoryTheory.Functor C D)
[F.Full]
:
Function.Surjective F.map
noncomputable def
CategoryTheory.Functor.preimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{X : C}
{Y : C}
(F : CategoryTheory.Functor C D)
[F.Full]
(f : F.obj X ⟶ F.obj Y)
:
X ⟶ Y
The choice of a preimage of a morphism under a full functor.
Equations
- F.preimage f = ⋯.choose
@[simp]
theorem
CategoryTheory.Functor.map_preimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Full]
{X : C}
{Y : C}
(f : F.obj X ⟶ F.obj Y)
:
F.map (F.preimage f) = f
@[simp]
theorem
CategoryTheory.Functor.preimage_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{X : C}
[F.Full]
[F.Faithful]
:
F.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X
@[simp]
theorem
CategoryTheory.Functor.preimage_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{X : C}
{Y : C}
{Z : C}
[F.Full]
[F.Faithful]
(f : F.obj X ⟶ F.obj Y)
(g : F.obj Y ⟶ F.obj Z)
:
F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)
@[simp]
theorem
CategoryTheory.Functor.preimage_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{X : C}
{Y : C}
[F.Full]
[F.Faithful]
(f : X ⟶ Y)
:
F.preimage (F.map f) = f
@[simp]
theorem
CategoryTheory.Functor.preimageIso_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
[F.Full]
[F.Faithful]
(f : F.obj X ≅ F.obj Y)
:
(F.preimageIso f).inv = F.preimage f.inv
@[simp]
theorem
CategoryTheory.Functor.preimageIso_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
[F.Full]
[F.Faithful]
(f : F.obj X ≅ F.obj Y)
:
(F.preimageIso f).hom = F.preimage f.hom
noncomputable def
CategoryTheory.Functor.preimageIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
[F.Full]
[F.Faithful]
(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
- F.preimageIso f = { hom := F.preimage f.hom, inv := F.preimage f.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
@[simp]
theorem
CategoryTheory.Functor.preimageIso_mapIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
{X : C}
{Y : C}
[F.Full]
[F.Faithful]
(f : X ≅ Y)
:
F.preimageIso (F.mapIso f) = f
structure
CategoryTheory.Functor.FullyFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Type (max (max u₁ v₁) v₂)
Structure containing the data of inverse map (F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y) of F.map
in order to express that F is a fully faithful functor.
The inverse map
(F.obj X ⟶ F.obj Y) ⟶ (X ⟶ Y)ofF.map.
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.map_preimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(self : F.FullyFaithful)
{X : C}
{Y : C}
(f : F.obj X ⟶ F.obj Y)
:
F.map (self.preimage f) = f
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.preimage_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(self : F.FullyFaithful)
{X : C}
{Y : C}
(f : X ⟶ Y)
:
self.preimage (F.map f) = f
noncomputable def
CategoryTheory.Functor.FullyFaithful.ofFullyFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Full]
[F.Faithful]
:
F.FullyFaithful
A FullyFaithful structure can be obtained from the assumption the F is both
full and faithful.
Equations
- CategoryTheory.Functor.FullyFaithful.ofFullyFaithful F = { preimage := fun {X Y : C} => F.preimage, map_preimage := ⋯, preimage_map := ⋯ }
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.id_preimage
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
:
∀ {X Y : C} (f : (CategoryTheory.Functor.id C).obj X ⟶ (CategoryTheory.Functor.id C).obj Y),
(CategoryTheory.Functor.FullyFaithful.id C).preimage f = f
def
CategoryTheory.Functor.FullyFaithful.id
(C : Type u₁)
[CategoryTheory.Category.{v₁, u₁} C]
:
(CategoryTheory.Functor.id C).FullyFaithful
The identity functor is fully faithful.
Equations
- One or more equations did not get rendered due to their size.
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.homEquiv_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
:
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.homEquiv_symm_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
(f : F.obj X ⟶ F.obj Y)
:
hF.homEquiv.symm f = hF.preimage f
def
CategoryTheory.Functor.FullyFaithful.homEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
:
The equivalence (X ⟶ Y) ≃ (F.obj X ⟶ F.obj Y) given by h : F.FullyFaithful.
Equations
- hF.homEquiv = { toFun := F.map, invFun := hF.preimage, left_inv := ⋯, right_inv := ⋯ }
theorem
CategoryTheory.Functor.FullyFaithful.map_injective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
{f : X ⟶ Y}
{g : X ⟶ Y}
(h : F.map f = F.map g)
:
f = g
theorem
CategoryTheory.Functor.FullyFaithful.map_surjective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
:
Function.Surjective F.map
theorem
CategoryTheory.Functor.FullyFaithful.map_bijective
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
(X : C)
(Y : C)
:
Function.Bijective F.map
theorem
CategoryTheory.Functor.FullyFaithful.full
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
:
F.Full
theorem
CategoryTheory.Functor.FullyFaithful.faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
:
F.Faithful
instance
CategoryTheory.Functor.FullyFaithful.instSubsingleton
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
:
Subsingleton F.FullyFaithful
Equations
- ⋯ = ⋯
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.preimageIso_inv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
(e : F.obj X ≅ F.obj Y)
:
(hF.preimageIso e).inv = hF.preimage e.inv
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.preimageIso_hom
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
(e : F.obj X ≅ F.obj Y)
:
(hF.preimageIso e).hom = hF.preimage e.hom
def
CategoryTheory.Functor.FullyFaithful.preimageIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
(e : F.obj X ≅ F.obj Y)
:
X ≅ Y
The unique isomorphism X ≅ Y which induces an isomorphism F.obj X ≅ F.obj Y
when hF : F.FullyFaithful.
Equations
- hF.preimageIso e = { hom := hF.preimage e.hom, inv := hF.preimage e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
theorem
CategoryTheory.Functor.FullyFaithful.isIso_of_isIso_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
(f : X ⟶ Y)
[CategoryTheory.IsIso (F.map f)]
:
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.isoEquiv_symm_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
(e : F.obj X ≅ F.obj Y)
:
hF.isoEquiv.symm e = hF.preimageIso e
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.isoEquiv_apply
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
(i : X ≅ Y)
:
hF.isoEquiv i = F.mapIso i
def
CategoryTheory.Functor.FullyFaithful.isoEquiv
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{X : C}
{Y : C}
:
The equivalence (X ≅ Y) ≃ (F.obj X ≅ F.obj Y) given by h : F.FullyFaithful.
Equations
- hF.isoEquiv = { toFun := F.mapIso, invFun := hF.preimageIso, left_inv := ⋯, right_inv := ⋯ }
@[simp]
theorem
CategoryTheory.Functor.FullyFaithful.comp_preimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{G : CategoryTheory.Functor D E}
(hG : G.FullyFaithful)
:
def
CategoryTheory.Functor.FullyFaithful.comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{F : CategoryTheory.Functor C D}
(hF : F.FullyFaithful)
{G : CategoryTheory.Functor D E}
(hG : G.FullyFaithful)
:
(F.comp G).FullyFaithful
Fully faithful functors are stable by composition.
def
CategoryTheory.Functor.FullyFaithful.ofCompFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u_1}
[CategoryTheory.Category.{u_2, u_1} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
[G.Faithful]
(hFG : (F.comp G).FullyFaithful)
:
F.FullyFaithful
If F ⋙ G is fully faithful and G is faithful, then F is fully faithful.
theorem
CategoryTheory.isIso_of_fully_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Full]
[F.Faithful]
{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.
instance
CategoryTheory.Functor.Full.id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
(CategoryTheory.Functor.id C).Full
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.Faithful.id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
:
(CategoryTheory.Functor.id C).Faithful
Equations
- ⋯ = ⋯
instance
CategoryTheory.Functor.Faithful.comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.Faithful]
[G.Faithful]
:
(F.comp G).Faithful
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Functor.Faithful.of_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[(F.comp G).Faithful]
:
F.Faithful
@[instance 100]
instance
CategoryTheory.Functor.instFaithfulOfIsThin
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[Quiver.IsThin C]
:
F.Faithful
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Functor.Full.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
[F.Full]
(α : F ≅ F')
:
F'.Full
If F is full, and naturally isomorphic to some F', then F' is also full.
theorem
CategoryTheory.Functor.Faithful.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
[F.Faithful]
(α : F ≅ F')
:
F'.Faithful
theorem
CategoryTheory.Functor.Faithful.of_comp_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor C E}
[H.Faithful]
(h : F.comp G ≅ H)
:
F.Faithful
theorem
CategoryTheory.Iso.faithful_of_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor C E}
[H.Faithful]
(h : F.comp G ≅ H)
:
F.Faithful
theorem
CategoryTheory.Functor.Faithful.of_comp_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor C E}
[ℋ : H.Faithful]
(h : F.comp G = H)
:
F.Faithful
theorem
Eq.faithful_of_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor C E}
[ℋ : H.Faithful]
(h : F.comp G = H)
:
F.Faithful
def
CategoryTheory.Functor.Faithful.div
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C E)
(G : CategoryTheory.Functor D E)
[G.Faithful]
(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}, HEq (G.map (map f)) (F.map f))
:
“Divide” a functor by a faithful functor.
Equations
- CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map = { obj := obj, map := map, map_id := ⋯, map_comp := ⋯ }
theorem
CategoryTheory.Functor.Faithful.div_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C E)
[F.Faithful]
(G : CategoryTheory.Functor D E)
[G.Faithful]
(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}, HEq (G.map (map f)) (F.map f))
:
(CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).comp G = F
theorem
CategoryTheory.Functor.Faithful.div_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C E)
[F.Faithful]
(G : CategoryTheory.Functor D E)
[G.Faithful]
(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}, HEq (G.map (map f)) (F.map f))
:
(CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).Faithful
instance
CategoryTheory.Functor.Full.comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[F.Full]
[G.Full]
:
(F.comp G).Full
Equations
- ⋯ = ⋯
theorem
CategoryTheory.Functor.Full.of_comp_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[(F.comp G).Full]
[G.Faithful]
:
F.Full
If F ⋙ G is full and G is faithful, then F is full.
theorem
CategoryTheory.Functor.Full.of_comp_faithful_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor C E}
[H.Full]
[G.Faithful]
(h : F.comp G ≅ H)
:
F.Full
If F ⋙ G is full and G is faithful, then F is full.
noncomputable def
CategoryTheory.Functor.fullyFaithfulCancelRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(H : CategoryTheory.Functor D E)
[H.Full]
[H.Faithful]
(comp_iso : F.comp H ≅ G.comp 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
- CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso = CategoryTheory.NatIso.ofComponents (fun (X : C) => H.preimageIso (comp_iso.app X)) ⋯
@[simp]
theorem
CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor D E}
[H.Full]
[H.Faithful]
(comp_iso : F.comp H ≅ G.comp H)
(X : C)
:
(CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)
@[simp]
theorem
CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor D E}
[H.Full]
[H.Faithful]
(comp_iso : F.comp H ≅ G.comp H)
(X : C)
:
(CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)
@[deprecated CategoryTheory.Functor.Full]
def
CategoryTheory.Full
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Alias of CategoryTheory.Functor.Full.
A functor F : C ⥤ D is full if for each X Y : C, F.map is surjective.
@[deprecated CategoryTheory.Functor.Faithful]
def
CategoryTheory.Faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
:
Alias of CategoryTheory.Functor.Faithful.
A functor F : C ⥤ D is faithful if for each X Y : C, F.map is injective.
@[deprecated CategoryTheory.Functor.preimage_id]
theorem
CategoryTheory.preimage_id
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{X : C}
[F.Full]
[F.Faithful]
:
F.preimage (CategoryTheory.CategoryStruct.id (F.obj X)) = CategoryTheory.CategoryStruct.id X
Alias of CategoryTheory.Functor.preimage_id.
@[deprecated CategoryTheory.Functor.preimage_comp]
theorem
CategoryTheory.preimage_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{X : C}
{Y : C}
{Z : C}
[F.Full]
[F.Faithful]
(f : F.obj X ⟶ F.obj Y)
(g : F.obj Y ⟶ F.obj Z)
:
F.preimage (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (F.preimage f) (F.preimage g)
Alias of CategoryTheory.Functor.preimage_comp.
@[deprecated CategoryTheory.Functor.preimage_map]
theorem
CategoryTheory.preimage_map
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{X : C}
{Y : C}
[F.Full]
[F.Faithful]
(f : X ⟶ Y)
:
F.preimage (F.map f) = f
Alias of CategoryTheory.Functor.preimage_map.
@[deprecated CategoryTheory.Functor.Faithful.of_comp]
theorem
CategoryTheory.Faithful.of_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[(F.comp G).Faithful]
:
F.Faithful
Alias of CategoryTheory.Functor.Faithful.of_comp.
@[deprecated CategoryTheory.Functor.Full.of_iso]
theorem
CategoryTheory.Full.ofIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
[F.Full]
(α : F ≅ F')
:
F'.Full
Alias of CategoryTheory.Functor.Full.of_iso.
If F is full, and naturally isomorphic to some F', then F' is also full.
@[deprecated CategoryTheory.Functor.Faithful.of_iso]
theorem
CategoryTheory.Faithful.of_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{F : CategoryTheory.Functor C D}
{F' : CategoryTheory.Functor C D}
[F.Faithful]
(α : F ≅ F')
:
F'.Faithful
Alias of CategoryTheory.Functor.Faithful.of_iso.
@[deprecated CategoryTheory.Functor.Faithful.of_comp_iso]
theorem
CategoryTheory.Faithful.of_comp_iso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor C E}
[H.Faithful]
(h : F.comp G ≅ H)
:
F.Faithful
@[deprecated CategoryTheory.Functor.Faithful.of_comp_eq]
theorem
CategoryTheory.Faithful.of_comp_eq
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor C E}
[ℋ : H.Faithful]
(h : F.comp G = H)
:
F.Faithful
@[deprecated CategoryTheory.Functor.Faithful.div]
def
CategoryTheory.Faithful.div
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C E)
(G : CategoryTheory.Functor D E)
[G.Faithful]
(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}, HEq (G.map (map f)) (F.map f))
:
Alias of CategoryTheory.Functor.Faithful.div.
“Divide” a functor by a faithful functor.
@[deprecated CategoryTheory.Functor.Faithful.div_comp]
theorem
CategoryTheory.Faithful.div_comp
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C E)
[F.Faithful]
(G : CategoryTheory.Functor D E)
[G.Faithful]
(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}, HEq (G.map (map f)) (F.map f))
:
(CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).comp G = F
Alias of CategoryTheory.Functor.Faithful.div_comp.
@[deprecated CategoryTheory.Functor.Faithful.div_faithful]
theorem
CategoryTheory.Faithful.div_faithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C E)
[F.Faithful]
(G : CategoryTheory.Functor D E)
[G.Faithful]
(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}, HEq (G.map (map f)) (F.map f))
:
(CategoryTheory.Functor.Faithful.div F G obj h_obj map h_map).Faithful
@[deprecated CategoryTheory.Functor.Full.of_comp_faithful]
theorem
CategoryTheory.Full.ofCompFaithful
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
(F : CategoryTheory.Functor C D)
(G : CategoryTheory.Functor D E)
[(F.comp G).Full]
[G.Faithful]
:
F.Full
Alias of CategoryTheory.Functor.Full.of_comp_faithful.
If F ⋙ G is full and G is faithful, then F is full.
@[deprecated CategoryTheory.Functor.Full.of_comp_faithful_iso]
theorem
CategoryTheory.Full.ofCompFaithfulIso
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor D E}
{H : CategoryTheory.Functor C E}
[H.Full]
[G.Faithful]
(h : F.comp G ≅ H)
:
F.Full
Alias of CategoryTheory.Functor.Full.of_comp_faithful_iso.
If F ⋙ G is full and G is faithful, then F is full.
@[deprecated CategoryTheory.Functor.fullyFaithfulCancelRight]
def
CategoryTheory.fullyFaithfulCancelRight
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
(H : CategoryTheory.Functor D E)
[H.Full]
[H.Faithful]
(comp_iso : F.comp H ≅ G.comp H)
:
F ≅ G
Alias of CategoryTheory.Functor.fullyFaithfulCancelRight.
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.
@[deprecated CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app]
theorem
CategoryTheory.fullyFaithfulCancelRight_hom_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor D E}
[H.Full]
[H.Faithful]
(comp_iso : F.comp H ≅ G.comp H)
(X : C)
:
(CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).hom.app X = H.preimage (comp_iso.hom.app X)
Alias of CategoryTheory.Functor.fullyFaithfulCancelRight_hom_app.
@[deprecated CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app]
theorem
CategoryTheory.fullyFaithfulCancelRight_inv_app
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
{E : Type u₃}
[CategoryTheory.Category.{v₃, u₃} E]
{F : CategoryTheory.Functor C D}
{G : CategoryTheory.Functor C D}
{H : CategoryTheory.Functor D E}
[H.Full]
[H.Faithful]
(comp_iso : F.comp H ≅ G.comp H)
(X : C)
:
(CategoryTheory.Functor.fullyFaithfulCancelRight H comp_iso).inv.app X = H.preimage (comp_iso.inv.app X)
Alias of CategoryTheory.Functor.fullyFaithfulCancelRight_inv_app.
@[deprecated CategoryTheory.Functor.map_preimage]
theorem
CategoryTheory.Functor.image_preimage
{C : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C]
{D : Type u₂}
[CategoryTheory.Category.{v₂, u₂} D]
(F : CategoryTheory.Functor C D)
[F.Full]
{X : C}
{Y : C}
(f : F.obj X ⟶ F.obj Y)
:
F.map (F.preimage f) = f
Alias of CategoryTheory.Functor.map_preimage.