# mathlib3documentation

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 #

• skyscraper_presheaf: skyscraper_presheaf p₀ A is the skyscraper presheaf at point p₀ with value A.
• skyscraper_sheaf: the skyscraper presheaf satisfies the sheaf condition.

## Main statements #

• skyscraper_presheaf_stalk_of_specializes: if y ∈ closure {p₀} then the stalk of skyscraper_presheaf p₀ A at y is A.
• skyscraper_presheaf_stalk_of_not_specializes: if y ∉ closure {p₀} then the stalk of skyscraper_presheaf p₀ A at y is * the terminal object.

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

@[simp]
theorem skyscraper_presheaf_obj {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) (U : ᵒᵖ) :
A).obj U = ite (p₀ A (⊤_ C)
@[simp]
theorem skyscraper_presheaf_map {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) (U V : ᵒᵖ) (i : U V) :
A).map i = dite (p₀ (λ (h : p₀ , (λ (h : p₀ , .from (ite (p₀ A (⊤_ C)))
noncomputable def skyscraper_presheaf {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) :
X

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
theorem skyscraper_presheaf_eq_pushforward {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) [hd : Π (U : , decidable (punit.star U)] :
= _* skyscraper_presheaf punit.star A
@[simp]
theorem skyscraper_presheaf_functor.map'_app {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {a b : C} (f : a b) (U : ᵒᵖ) :
U = dite (p₀ (λ (h : p₀ , (λ (h : p₀ , .from a).obj U))
noncomputable def skyscraper_presheaf_functor.map' {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {a b : C} (f : a b) :

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
theorem skyscraper_presheaf_functor.map'_id {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {a : C} :
= 𝟙 a)
theorem skyscraper_presheaf_functor.map'_comp {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {a b c : C} (f : a b) (g : b c) :
@[simp]
theorem skyscraper_presheaf_functor_obj {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) :
=
@[simp]
theorem skyscraper_presheaf_functor_map {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (_x _x_1 : C) (f : _x _x_1) :
noncomputable def skyscraper_presheaf_functor {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :
C X

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
@[simp]
theorem skyscraper_presheaf_cocone_of_specializes_ι_app {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : p₀ y) (U : ᵒᵖ) :
@[simp]
theorem skyscraper_presheaf_cocone_of_specializes_X {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : p₀ y) :
= A
noncomputable def skyscraper_presheaf_cocone_of_specializes {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : p₀ y) :

The cocone at A for the stalk functor of skyscraper_presheaf p₀ A when y ∈ closure {p₀}

Equations
noncomputable def skyscraper_presheaf_cocone_is_colimit_of_specializes {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : p₀ y) :

The cocone at A for the stalk functor of skyscraper_presheaf p₀ A when y ∈ closure {p₀} is a colimit

Equations
noncomputable def skyscraper_presheaf_stalk_of_specializes {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : p₀ y) :
A).stalk y A

If y ∈ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is A.

Equations
noncomputable def skyscraper_presheaf_cocone {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) (y : X) :

The cocone at * for the stalk functor of skyscraper_presheaf p₀ A when y ∉ closure {p₀}

Equations
@[simp]
theorem skyscraper_presheaf_cocone_ι_app {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) (y : X) (U : ᵒᵖ) :
y).ι.app U =
@[simp]
theorem skyscraper_presheaf_cocone_X {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) (y : X) :
y).X = ⊤_ C
noncomputable def skyscraper_presheaf_cocone_is_colimit_of_not_specializes {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : ¬p₀ y) :

The cocone at * for the stalk functor of skyscraper_presheaf p₀ A when y ∉ closure {p₀} is a colimit

Equations
noncomputable def skyscraper_presheaf_stalk_of_not_specializes {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : ¬p₀ y) :
A).stalk y ⊤_ C

If y ∉ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is isomorphic to a terminal object.

Equations
noncomputable def skyscraper_presheaf_stalk_of_not_specializes_is_terminal {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : ¬p₀ y) :

If y ∉ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is a terminal object

Equations
theorem skyscraper_presheaf_is_sheaf {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C)  :
noncomputable def skyscraper_sheaf {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (A : C)  :
X

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
noncomputable def skyscraper_sheaf_functor {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :
C X

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
noncomputable def stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {𝓕 : X} {c : C} (f : 𝓕.stalk p₀ c) :
𝓕

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
@[simp]
theorem stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf_app {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {𝓕 : X} {c : C} (f : 𝓕.stalk p₀ c) (U : ᵒᵖ) :
= dite (p₀ (λ (h : p₀ , 𝓕.germ p₀, h⟩ (λ (h : p₀ , .from (𝓕.obj U))
noncomputable def stalk_skyscraper_presheaf_adjunction_auxs.from_stalk {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {𝓕 : X} {c : C} (f : 𝓕 ) :
𝓕.stalk p₀ c

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
theorem stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_from_stalk {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {𝓕 : X} {c : C} (f : 𝓕 ) :
theorem stalk_skyscraper_presheaf_adjunction_auxs.from_stalk_to_skyscraper {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} {𝓕 : X} {c : C} (f : 𝓕.stalk p₀ c) :
@[simp]
theorem stalk_skyscraper_presheaf_adjunction_auxs.unit_app {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (𝓕 : X) :
= (𝟙 (((𝟭 X)).obj 𝓕).stalk p₀))
@[protected]
noncomputable def stalk_skyscraper_presheaf_adjunction_auxs.unit {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :
𝟭 X)

The unit in presheaf.stalk ⊣ skyscraper_presheaf_functor

Equations
@[simp]
theorem stalk_skyscraper_presheaf_adjunction_auxs.counit_app {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v} (c : C) :
@[protected]
noncomputable def stalk_skyscraper_presheaf_adjunction_auxs.counit {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :

The counit in presheaf.stalk ⊣ skyscraper_presheaf_functor

Equations
noncomputable def skyscraper_presheaf_stalk_adjunction {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :

skyscraper_presheaf_functor is the right adjoint of presheaf.stalk_functor

Equations
@[protected, instance]
noncomputable def skyscraper_presheaf_functor.category_theory.is_right_adjoint {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :
Equations
@[protected, instance]
noncomputable def Top.presheaf.stalk_functor.category_theory.is_left_adjoint {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :
Equations
noncomputable def stalk_skyscraper_sheaf_adjunction {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :

Taking stalks of a sheaf is the left adjoint functor to skyscraper_sheaf_functor

Equations
@[protected, instance]
noncomputable def skyscraper_sheaf_functor.category_theory.is_right_adjoint {X : Top} (p₀ : X) [Π (U : , decidable (p₀ U)] {C : Type v}  :
Equations