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
.- witness : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (CategoryTheory.Full.preimage f) = f
The property that
Full.preimage f
of maps tof
viaF.map
.
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
- map_injective : ∀ {X Y : C}, Function.Injective F.map
F.map
is injective for eachX Y : C
.
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
The specified preimage of a morphism under a full functor.
Instances For
Deduce that F
is full from the existence of preimages, using choice.
Instances For
Deduce that F
is full from surjectivity of F.map
, using choice.
Instances For
If F : C ⥤ D
is fully faithful, every isomorphism F.obj X ≅ F.obj Y
has a preimage.
Instances For
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
and F X ⟶ F Y
.
Instances For
If F
is fully faithful, we have an equivalence of iso-sets X ≅ Y
and F X ≅ F Y
.
Instances For
We can construct a natural transformation between functors by constructing a natural transformation between those functors composed with a fully faithful functor.
Instances For
We can construct a natural isomorphism between functors by constructing a natural isomorphism between those functors composed with a fully faithful functor.
Instances For
Horizontal composition with a fully faithful functor induces a bijection on natural transformations.
Instances For
Horizontal composition with a fully faithful functor induces a bijection on natural isomorphisms.
Instances For
If F
is full, and naturally isomorphic to some F'
, then F'
is also full.
Instances For
Alias of CategoryTheory.Faithful.of_comp_iso
.
Alias of CategoryTheory.Faithful.of_comp_eq
.
“Divide” a functor by a faithful functor.
Instances For
If F ⋙ G
is full and G
is faithful, then F
is full.
Instances For
If F ⋙ G
is full and G
is faithful, then F
is full.
Instances For
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
.