Skyscraper (pre)sheaves #
A skyscraper (pre)sheaf ๐ : (Pre)Sheaf C X
is the (pre)sheaf with value A
at point pโ
that is
supported only at open sets contain pโ
, i.e. ๐(U) = A
if pโ โ U
and ๐(U) = *
if pโ โ U
where *
is a terminal object of C
. In terms of stalks, ๐
is supported at all specializations
of pโ
, i.e. if pโ โคณ x
then ๐โ โ
A
and if ยฌ pโ โคณ x
then ๐โ โ
*
.
Main definitions #
skyscraperPresheaf
:skyscraperPresheaf pโ A
is the skyscraper presheaf at pointpโ
with valueA
.skyscraperSheaf
: the skyscraper presheaf satisfies the sheaf condition.
Main statements #
skyscraperPresheafStalkOfSpecializes
: ify โ closure {pโ}
then the stalk ofskyscraperPresheaf pโ A
aty
isA
.skyscraperPresheafStalkOfNotSpecializes
: ify โ closure {pโ}
then the stalk ofskyscraperPresheaf pโ A
aty
is*
the terminal object.
TODO: generalize universe level when calculating stalks, after generalizing universe level of stalk.
A skyscraper presheaf is a presheaf supported at a single point: if pโ โ X
is a specified
point, then the skyscraper presheaf ๐
with value A
is defined by U โฆ A
if pโ โ U
and
U โฆ *
if pโ โ A
where *
is some terminal object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Taking skyscraper presheaf at a point is functorial: c โฆ skyscraper pโ c
defines a functor by
sending every f : a โถ b
to the natural transformation ฮฑ
defined as: ฮฑ(U) = f : a โถ b
if
pโ โ U
and the unique morphism to a terminal object in C
if pโ โ U
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Taking skyscraper presheaf at a point is functorial: c โฆ skyscraper pโ c
defines a functor by
sending every f : a โถ b
to the natural transformation ฮฑ
defined as: ฮฑ(U) = f : a โถ b
if
pโ โ U
and the unique morphism to a terminal object in C
if pโ โ U
.
Equations
- skyscraperPresheafFunctor pโ = { obj := skyscraperPresheaf pโ, map := fun {X_1 Y : C} => SkyscraperPresheafFunctor.map' pโ, map_id := โฏ, map_comp := โฏ }
Instances For
The cocone at A
for the stalk functor of skyscraperPresheaf pโ A
when y โ closure {pโ}
Equations
Instances For
The cocone at A
for the stalk functor of skyscraperPresheaf pโ A
when y โ closure {pโ}
is a
colimit
Equations
- One or more equations did not get rendered due to their size.
Instances For
If y โ closure {pโ}
, then the stalk of skyscraperPresheaf pโ A
at y
is A
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cocone at *
for the stalk functor of skyscraperPresheaf pโ A
when y โ closure {pโ}
Equations
- One or more equations did not get rendered due to their size.
Instances For
The cocone at *
for the stalk functor of skyscraperPresheaf pโ A
when y โ closure {pโ}
is a
colimit
Equations
- One or more equations did not get rendered due to their size.
Instances For
If y โ closure {pโ}
, then the stalk of skyscraperPresheaf pโ A
at y
is isomorphic to a
terminal object.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If y โ closure {pโ}
, then the stalk of skyscraperPresheaf pโ A
at y
is a terminal object
Equations
Instances For
The skyscraper presheaf supported at pโ
with value A
is the sheaf that assigns A
to all opens
U
that contain pโ
and assigns *
otherwise.
Equations
- skyscraperSheaf pโ A = { val := skyscraperPresheaf pโ A, cond := โฏ }
Instances For
Taking skyscraper sheaf at a point is functorial: c โฆ skyscraper pโ c
defines a functor by
sending every f : a โถ b
to the natural transformation ฮฑ
defined as: ฮฑ(U) = f : a โถ b
if
pโ โ U
and the unique morphism to a terminal object in C
if pโ โ U
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If f : ๐.stalk pโ โถ c
, then a natural transformation ๐ โถ skyscraperPresheaf pโ c
can be
defined by: ๐.germ pโ โซ f : ๐(U) โถ c
if pโ โ U
and the unique morphism to a terminal object
if pโ โ U
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
If f : ๐ โถ skyscraperPresheaf pโ c
is a natural transformation, then there is a morphism
๐.stalk pโ โถ c
defined as the morphism from colimit to cocone at c
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The unit in Presheaf.stalkFunctor โฃ skyscraperPresheafFunctor
Equations
- One or more equations did not get rendered due to their size.
Instances For
The counit in Presheaf.stalkFunctor โฃ skyscraperPresheafFunctor
Equations
Instances For
skyscraperPresheafFunctor
is the right adjoint of Presheaf.stalkFunctor
Equations
- One or more equations did not get rendered due to their size.
Instances For
Taking stalks of a sheaf is the left adjoint functor to skyscraperSheafFunctor
Equations
- One or more equations did not get rendered due to their size.