Relatively representable morphisms #
In this file we define and develop basic results about relatively representable morphisms.
Classically, a morphism f : F ⟶ G
of presheaves is said to be representable if for any morphism
g : yoneda.obj X ⟶ G
, there exists a pullback square of the following form
yoneda.obj Y --yoneda.map snd--> yoneda.obj X
| |
fst g
| |
v v
F ------------ f --------------> G
In this file, we define a notion of relative representability which works with respect to any
functor, and not just yoneda
. The fact that a morphism f : F ⟶ G
between presheaves is
representable in the classical case will then be given by yoneda.relativelyRepresentable f
.
Main definitions #
Throughout this file, F : C ⥤ D
is a functor between categories C
and D
.
Functor.relativelyRepresentable
: A morphismf : X ⟶ Y
inD
is said to be relatively representable with respect toF
, if for anyg : F.obj a ⟶ Y
, there exists a pullback square of the following form
F.obj b --F.map snd--> F.obj a
| |
fst g
| |
v v
X ------- f --------> Y
MorphismProperty.relative
: Given a morphism propertyP
inC
, a morphismf : X ⟶ Y
inD
satisfiesP.relative F
if it is relatively representable and for anyg : F.obj a ⟶ Y
, the propertyP
holds for any represented pullback off
byg
.
API #
Given hf : relativelyRepresentable f
, with f : X ⟶ Y
and g : F.obj a ⟶ Y
, we provide:
hf.pullback g
which is the object inC
such thatF.obj (hf.pullback g)
is a pullback off
andg
.hf.snd g
is the morphismhf.pullback g ⟶ F.obj a
hf.fst g
is the morphismF.obj (hf.pullback g) ⟶ X
- If
F
is full, andf
is of typeF.obj c ⟶ G
, we also havehf.fst' g : hf.pullback g ⟶ X
which is the preimage underF
ofhf.fst g
. hom_ext
,hom_ext'
,lift
,lift'
are variants of the universal property ofF.obj (hf.pullback g)
, where as much as possible has been formulated internally toC
. For these theorems we also need thatF
is full and/or faithful.symmetry
andsymmetryIso
are variants of the fact that pullbacks are symmetric for representable morphisms, formulated internally toC
. We assume thatF
is fully faithful here.
Main results #
relativelyRepresentable.isMultiplicative
: The class of relatively representable morphisms is multiplicative.relativelyRepresentable.isStableUnderBaseChange
: Being relatively representable is stable under base change.relativelyRepresentable.of_isIso
: Isomorphisms are relatively representable.
A morphism f : X ⟶ Y
in D
is said to be relatively representable if for any
g : F.obj a ⟶ Y
, there exists a pullback square of the following form
F.obj b --F.map snd--> F.obj a
| |
fst g
| |
v v
X ------- f --------> Y
Equations
- F.relativelyRepresentable f = ∀ ⦃a : C⦄ (g : F.obj a ⟶ Y), ∃ (b : C) (snd : b ⟶ a) (fst : F.obj b ⟶ X), CategoryTheory.IsPullback fst (F.map snd) f g
Instances For
Let f : X ⟶ Y
be a relatively representable morphism in D
. Then, for any
g : F.obj a ⟶ Y
, hf.pullback g
denotes the (choice of) a corresponding object in C
such that
there is a pullback square of the following form
hf.pullback g --F.map snd--> F.obj a
| |
fst g
| |
v v
X ---------- f ----------> Y
Equations
- hf.pullback g = ⋯.choose
Instances For
Given a representable morphism f : X ⟶ Y
, then for any g : F.obj a ⟶ Y
, hf.snd g
denotes the morphism in C
giving rise to the following diagram
hf.pullback g --F.map (hf.snd g)--> F.obj a
| |
fst g
| |
v v
X -------------- f -------------> Y
Equations
- hf.snd g = ⋯.choose
Instances For
Given a relatively representable morphism f : X ⟶ Y
, then for any g : F.obj a ⟶ Y
,
hf.fst g
denotes the first projection in the following diagram, given by the defining property
of f
being relatively representable
hf.pullback g --F.map (hf.snd g)--> F.obj a
| |
hf.fst g g
| |
v v
X -------------- f -------------> Y
Equations
- hf.fst g = ⋯.choose
Instances For
When F
is full, given a representable morphism f' : F.obj b ⟶ Y
, then hf'.fst' g
denotes
the preimage of hf'.fst g
under F
.
Equations
- hf'.fst' g = F.preimage (hf'.fst g)
Instances For
Variant of the pullback square when F
is full, and given f' : F.obj b ⟶ Y
.
Two morphisms a b : c ⟶ hf.pullback g
are equal if
In the case of a representable morphism f' : F.obj Y ⟶ G
, whose codomain lies
in the image of F
, we get that two morphism a b : Z ⟶ hf.pullback g
are equal if
The lift (in C
) obtained from the universal property of F.obj (hf.pullback g)
, in the
case when the cone point is in the image of F.obj
.
Equations
- hf.lift i h hi = F.preimage (CategoryTheory.Limits.PullbackCone.IsLimit.lift ⋯.isLimit i (F.map h) hi)
Instances For
Variant of lift
in the case when the domain of f
lies in the image of F.obj
. Thus,
in this case, one can obtain the lift directly by giving two morphisms in C
.
Equations
- hf'.lift' i h hi = hf'.lift (F.map i) h hi
Instances For
Given two representable morphisms f' : F.obj b ⟶ Y
and g : F.obj a ⟶ Y
, we
obtain an isomorphism hf'.pullback g ⟶ hg.pullback f'
.
Equations
- hf'.symmetry hg = hg.lift' (hf'.snd g) (hf'.fst' g) ⋯
Instances For
The isomorphism given by Presheaf.representable.symmetry
.
Equations
- hf'.symmetryIso hg = { hom := hf'.symmetry hg, inv := hg.symmetry hf', hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
When C
has pullbacks, then F.map f
is representable with respect to F
for any
f : a ⟶ b
in C
.
Given a morphism property P
in a category C
, a functor F : C ⥤ D
and a morphism
f : X ⟶ Y
in D
. Then f
satisfies the morphism property P.relative
with respect to F
iff:
- The morphism is representable with respect to
F
- For any morphism
g : F.obj a ⟶ Y
, the propertyP
holds for any represented pullback off
byg
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Given a morphism property P
in a category C
, a morphism f : F ⟶ G
of presheaves in the
category Cᵒᵖ ⥤ Type v
satisfies the morphism property P.presheaf
iff:
- The morphism is representable.
- For any morphism
g : F.obj a ⟶ G
, the propertyP
holds for any represented pullback off
byg
. This is implemented as a special case of the more general notion ofP.relative
, to the case when the functorF
isyoneda
.
Equations
- P.presheaf = CategoryTheory.MorphismProperty.relative CategoryTheory.yoneda P
Instances For
A morphism satisfying P.relative
is representable.
Given a morphism property P
which respects isomorphisms, then to show that a morphism
f : X ⟶ Y
satisfies P.relative
it suffices to show that:
- The morphism is representable.
- For any morphism
g : F.obj a ⟶ G
, the propertyP
holds for some represented pullback off
byg
.
If P : MorphismProperty C
is stable under base change, F
is fully faithful and preserves
pullbacks, and C
has all pullbacks, then for any f : a ⟶ b
in C
, F.map f
satisfies
P.relative
if f
satisfies P
.
If P' : MorphismProperty C
is satisfied whenever P
is, then also P'.relative
is
satisfied whenever P.relative
is.
Morphisms satisfying (monomorphism C).presheaf
are in particular monomorphisms.