Relatively representable morphisms #
In this file we define and develop basic results about relatively representable morphisms.
Classically, a morphism f : X ⟶ Y
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
.
- We define
relativelyRepresentable
as aMorphismProperty
. 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
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.stableUnderBaseChange
: 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
Equations
- ⋯ = ⋯
When C
has pullbacks, then F.map f
is representable with respect to F
for any
f : a ⟶ b
in C
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯