mathlib3 documentation

topology.sheaves.skyscraper

Skyscraper (pre)sheaves #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

Main statements #

TODO: generalize universe level when calculating stalks, after generalizing universe level of stalk.

noncomputable def skyscraper_presheaf {X : Top} (p₀ : X) [Π (U : topological_space.opens X), decidable (p₀ U)] {C : Type v} [category_theory.category C] [category_theory.limits.has_terminal C] (A : C) :

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

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

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
Instances for skyscraper_presheaf_functor
noncomputable def skyscraper_sheaf {X : Top} (p₀ : X) [Π (U : topological_space.opens X), decidable (p₀ U)] {C : Type v} [category_theory.category C] (A : C) [category_theory.limits.has_terminal C] :

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

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
Instances for skyscraper_sheaf_functor

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.

Equations

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.

Equations