Full and faithful functors #
We define typeclasses Full
and Faithful
, decorating functors.
Main definitions and results #
- Use
F.map_injective
to retrieve the fact thatF.map
is injective when[Faithful F]
. - Similarly,
F.map_surjective
states thatF.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 usingF.preimage
. To obtain an instance ofFull F
non-constructively, you can usefullOfExists
andfullOfSurjective
.
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.
The data of a preimage for every
f : F.obj X ⟶ F.obj Y⟶ F.obj Y
.The property that
Full.preimage f
of maps tof
viaF.map
.
A functor F : C ⥤ D⥤ 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⟶ F.obj Y
.
See https://stacks.math.columbia.edu/tag/001C.
Instances
F.map
is injective for eachX Y : C
.map_injective : autoParam (∀ {X Y : C}, Function.Injective (Prefunctor.map F.toPrefunctor)) _auto✝
A functor F : C ⥤ D⥤ D
is faithful if for each X Y : C
, F.map
is injective.
See https://stacks.math.columbia.edu/tag/001C.
Instances
The specified preimage of a morphism under a full functor.
Equations
Deduce that F
is full from the existence of preimages, using choice.
Equations
- One or more equations did not get rendered due to their size.
Deduce that F
is full from surjectivity of F.map
, using choice.
Equations
If F : C ⥤ D⥤ D
is fully faithful, every isomorphism F.obj X ≅ F.obj Y≅ F.obj Y
has a preimage.
Equations
If the image of a morphism under a fully faithful functor in an isomorphism, then the original morphisms is also an isomorphism.
If F
is fully faithful, we have an equivalence of hom-sets X ⟶ Y⟶ Y
and F X ⟶ F Y⟶ F Y
.
Equations
- One or more equations did not get rendered due to their size.
If F
is fully faithful, we have an equivalence of iso-sets X ≅ Y≅ Y
and F X ≅ F Y≅ F Y
.
Equations
- One or more equations did not get rendered due to their size.
We can construct a natural transformation between functors by constructing a natural transformation between those functors composed with a fully faithful functor.
Equations
- CategoryTheory.natTransOfCompFullyFaithful H α = CategoryTheory.NatTrans.mk fun X => ↑(Equiv.symm (CategoryTheory.equivOfFullyFaithful H)) (α.app X)
We can construct a natural isomorphism between functors by constructing a natural isomorphism between those functors composed with a fully faithful functor.
Equations
- One or more equations did not get rendered due to their size.
Horizontal composition with a fully faithful functor induces a bijection on natural transformations.
Equations
- One or more equations did not get rendered due to their size.
Horizontal composition with a fully faithful functor induces a bijection on natural isomorphisms.
Equations
- One or more equations did not get rendered due to their size.
Equations
- CategoryTheory.Full.id = CategoryTheory.Full.mk fun {X Y} f => f
If F
is full, and naturally isomorphic to some F'
, then F'
is also full.
Equations
- CategoryTheory.Full.ofIso α = CategoryTheory.Full.mk fun {X Y} f => CategoryTheory.Functor.preimage F ((α.app X).hom ≫ f ≫ (α.app Y).inv)
Alias of CategoryTheory.Faithful.of_comp_iso
.
Alias of CategoryTheory.Faithful.of_comp_eq
.
“Divide” a functor by a faithful functor.
Equations
- CategoryTheory.Faithful.div F G obj h_obj map h_map = CategoryTheory.Functor.mk { obj := obj, map := map }
Equations
- CategoryTheory.Full.comp F G = CategoryTheory.Full.mk fun {X Y} f => CategoryTheory.Functor.preimage F (CategoryTheory.Functor.preimage G f)
If F ⋙ G⋙ G
is full and G
is faithful, then F
is full.
Equations
- CategoryTheory.Full.ofCompFaithful F G = CategoryTheory.Full.mk fun {X Y} f => CategoryTheory.Functor.preimage (F ⋙ G) (G.map f)
If F ⋙ G⋙ G
is full and G
is faithful, then F
is full.
Given a natural isomorphism between F ⋙ H⋙ H
and G ⋙ H⋙ H
for a fully faithful functor H
, we
can 'cancel' it to give a natural iso between F
and G
.
Equations
- One or more equations did not get rendered due to their size.