# Documentation

Mathlib.Topology.Sheaves.Skyscraper

# 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 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 skyscraperPresheaf_map {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) {U : } {V : } (i : U V) :
().map i = if h : p₀ V.unop then CategoryTheory.eqToHom (_ : (fun U => if p₀ U.unop then A else ⊤_ C) U = (fun U => if p₀ U.unop then A else ⊤_ C) V) else CategoryTheory.Limits.IsTerminal.from ((_ : (⊤_ C) = if p₀ V.unop then A else ⊤_ C)CategoryTheory.Limits.terminalIsTerminal) ((fun U => if p₀ U.unop then A else ⊤_ C) U)
@[simp]
theorem skyscraperPresheaf_obj {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) (U : ) :
().obj U = if p₀ U.unop then A else ⊤_ C
def skyscraperPresheaf {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (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.

Instances For
theorem skyscraperPresheaf_eq_pushforward {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) [hd : (U : ) → Decidable ()] :
@[simp]
theorem SkyscraperPresheafFunctor.map'_app {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {a : C} {b : C} (f : a b) (U : ) :
().app U = if h : p₀ U.unop then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (if p₀ U.unop then a else ⊤_ C) = a)) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom (_ : b = if p₀ U.unop then b else ⊤_ C))) else CategoryTheory.Limits.IsTerminal.from ((_ : (⊤_ C) = if p₀ U.unop then b else ⊤_ C)CategoryTheory.Limits.terminalIsTerminal) (().obj U)
def SkyscraperPresheafFunctor.map' {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {a : C} {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.

Instances For
theorem SkyscraperPresheafFunctor.map'_id {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {a : C} :
theorem SkyscraperPresheafFunctor.map'_comp {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {a : C} {b : C} {c : C} (f : a b) (g : b c) :
@[simp]
theorem skyscraperPresheafFunctor_map {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} :
∀ {X Y : C} (f : X Y), ().map f =
@[simp]
theorem skyscraperPresheafFunctor_obj {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) :
().obj A =
def skyscraperPresheafFunctor {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} :

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
@[simp]
theorem skyscraperPresheafCoconeOfSpecializes_pt {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : p₀ y) :
().pt = A
@[simp]
theorem skyscraperPresheafCoconeOfSpecializes_ι_app {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : p₀ y) (U : ) :
().ι.app U = CategoryTheory.eqToHom (_ : (if p₀ U.unop.obj.carrier then A else ⊤_ C) = A)
def skyscraperPresheafCoconeOfSpecializes {X : TopCat} (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₀}

Instances For
noncomputable def skyscraperPresheafCoconeIsColimitOfSpecializes {X : TopCat} (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

Instances For
noncomputable def skyscraperPresheafStalkOfSpecializes {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) {y : X} (h : p₀ y) :
A

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

Instances For
@[simp]
theorem skyscraperPresheafCocone_ι_app {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) (y : X) :
∀ (x : ), ().ι.app x =
@[simp]
theorem skyscraperPresheafCocone_pt {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) (y : X) :
().pt = ⊤_ C
def skyscraperPresheafCocone {X : TopCat} (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₀}

Instances For
noncomputable def skyscraperPresheafCoconeIsColimitOfNotSpecializes {X : TopCat} (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

Instances For
noncomputable def skyscraperPresheafStalkOfNotSpecializes {X : TopCat} (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 isomorphic to a terminal object.

Instances For
def skyscraperPresheafStalkOfNotSpecializesIsTerminal {X : TopCat} (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

Instances For
theorem skyscraperPresheaf_isSheaf {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : C) :
def skyscraperSheaf {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (A : 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.

Instances For
def skyscraperSheafFunctor {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} :

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
@[simp]
theorem StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {𝓕 : } {c : C} (f : c) (U : ) :
= if h : p₀ U.unop then CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.germ 𝓕 { val := p₀, property := h }) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom (_ : c = if p₀ U.unop then c else ⊤_ C))) else CategoryTheory.Limits.IsTerminal.from ((_ : (⊤_ C) = if p₀ U.unop then c else ⊤_ C)CategoryTheory.Limits.terminalIsTerminal) (𝓕.obj U)
def StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {𝓕 : } {c : C} (f : 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.

Instances For
def StalkSkyscraperPresheafAdjunctionAuxs.fromStalk {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {𝓕 : } {c : C} (f : 𝓕 ) :
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.

Instances For
theorem StalkSkyscraperPresheafAdjunctionAuxs.to_skyscraper_fromStalk {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {𝓕 : } {c : C} (f : 𝓕 ) :
theorem StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} {𝓕 : } {c : C} (f : c) :
@[simp]
theorem StalkSkyscraperPresheafAdjunctionAuxs.unit_app {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (𝓕 : ) :
=
def StalkSkyscraperPresheafAdjunctionAuxs.unit {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} :

The unit in presheaf.stalk ⊣ skyscraper_presheaf_functor

Instances For
@[simp]
theorem StalkSkyscraperPresheafAdjunctionAuxs.counit_app {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} (c : C) :
= (skyscraperPresheafStalkOfSpecializes p₀ c (_ : p₀ p₀)).hom
def StalkSkyscraperPresheafAdjunctionAuxs.counit {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} :

The counit in presheaf.stalk ⊣ skyscraper_presheaf_functor

Instances For
def skyscraperPresheafStalkAdjunction {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} :

skyscraper_presheaf_functor is the right adjoint of presheaf.stalk_functor

Instances For
instance instIsLeftAdjointPresheafInstCategoryPresheafStalkFunctor {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} :
def stalkSkyscraperSheafAdjunction {X : TopCat} (p₀ : X) [(U : ) → Decidable (p₀ U)] {C : Type v} :

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

Instances For