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 #
skyscraper_presheaf
:skyscraper_presheaf p₀ A
is the skyscraper presheaf at pointp₀
with valueA
.skyscraper_sheaf
: the skyscraper presheaf satisfies the sheaf condition.
Main statements #
skyscraper_presheaf_stalk_of_specializes
: ify ∈ closure {p₀}
then the stalk ofskyscraper_presheaf p₀ A
aty
isA
.skyscraper_presheaf_stalk_of_not_specializes
: ify ∉ closure {p₀}
then the stalk ofskyscraper_presheaf 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.
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
.
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
.
Instances For
The cocone at A
for the stalk functor of skyscraper_presheaf p₀ A
when y ∈ closure {p₀}
Instances For
The cocone at A
for the stalk functor of skyscraper_presheaf p₀ A
when y ∈ closure {p₀}
is a
colimit
Instances For
If y ∈ closure {p₀}
, then the stalk of skyscraper_presheaf p₀ A
at y
is A
.
Instances For
The cocone at *
for the stalk functor of skyscraper_presheaf p₀ A
when y ∉ closure {p₀}
Instances For
The cocone at *
for the stalk functor of skyscraper_presheaf p₀ A
when y ∉ closure {p₀}
is a
colimit
Instances For
If y ∉ closure {p₀}
, then the stalk of skyscraper_presheaf p₀ A
at y
is isomorphic to a
terminal object.
Instances For
If y ∉ closure {p₀}
, then the stalk of skyscraper_presheaf p₀ A
at y
is a terminal object
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.
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
.
Instances For
If f : 𝓕.stalk p₀ ⟶ c
, then a natural transformation 𝓕 ⟶ skyscraper_presheaf 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
.
Instances For
If f : 𝓕 ⟶ skyscraper_presheaf p₀ c
is a natural transformation, then there is a morphism
𝓕.stalk p₀ ⟶ c
defined as the morphism from colimit to cocone at c
.
Instances For
The unit in presheaf.stalk ⊣ skyscraper_presheaf_functor
Instances For
The counit in presheaf.stalk ⊣ skyscraper_presheaf_functor
Instances For
skyscraper_presheaf_functor
is the right adjoint of presheaf.stalk_functor
Instances For
Taking stalks of a sheaf is the left adjoint functor to skyscraper_sheaf_functor