# 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 point pโ with value A.
• skyscraperSheaf: the skyscraper presheaf satisfies the sheaf condition.

## Main statements #

• skyscraperPresheafStalkOfSpecializes: if y โ closure {pโ} then the stalk of skyscraperPresheaf pโ A at y is A.
• skyscraperPresheafStalkOfNotSpecializes: if y โ closure {pโ} then the stalk of skyscraperPresheaf 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) :
(skyscraperPresheaf pโ A).map i = if h : pโ โ V.unop then else (โฏ โธ CategoryTheory.Limits.terminalIsTerminal).from ((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 : ()แตแต) :
(skyscraperPresheaf pโ A).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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem skyscraperPresheaf_eq_pushforward {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (A : C) [hd : (U : TopologicalSpace.Opens โ) โ ] :
skyscraperPresheaf pโ A = ContinuousMap.const (โ) pโ _*
@[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 else (โฏ โธ CategoryTheory.Limits.terminalIsTerminal).from ((skyscraperPresheaf pโ a).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.

Equations
• One or more equations did not get rendered due to their size.
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_1 Y : C} (f : X_1 โถ Y), ().map f =
@[simp]
theorem skyscraperPresheafFunctor_obj {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (A : C) :
().obj A = skyscraperPresheaf pโ 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.

Equations
• = { obj := , map := fun {X_1 Y : C} => , map_id := โฏ, map_comp := โฏ }
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 =
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 skyscraperPresheaf pโ A when y โ closure {pโ}

Equations
• = { pt := A, ฮน := { app := fun (U : ) => , naturality := โฏ } }
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 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
noncomputable def skyscraperPresheafStalkOfSpecializes {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (A : C) {y : โX} (h : pโ โคณ y) :
(skyscraperPresheaf pโ A).stalk y โ A

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
@[simp]
theorem skyscraperPresheafCocone_ฮน_app {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (A : C) (y : โX) :
โ (x : ), (skyscraperPresheafCocone pโ A y).ฮน.app x = CategoryTheory.Limits.terminal.from ((.comp (skyscraperPresheaf pโ A)).obj x)
@[simp]
theorem skyscraperPresheafCocone_pt {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (A : C) (y : โX) :
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 skyscraperPresheaf pโ A when y โ closure {pโ}

Equations
• One or more equations did not get rendered due to their size.
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 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
noncomputable def skyscraperPresheafStalkOfNotSpecializes {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (A : C) {y : โX} (h : ยฌpโ โคณ y) :
(skyscraperPresheaf pโ A).stalk y โ โค_ C

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
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 skyscraperPresheaf pโ A at y is a terminal object

Equations
• = CategoryTheory.Limits.terminalIsTerminal.ofIso ().symm
Instances For
theorem skyscraperPresheaf_isSheaf {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (A : C) :
(skyscraperPresheaf pโ A).IsSheaf
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.

Equations
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.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} {๐ : } {c : C} (f : ๐.stalk pโ โถ c) (U : ()แตแต) :
= if h : pโ โ U.unop then CategoryTheory.CategoryStruct.comp (๐.germ โจpโ, hโฉ) else (โฏ โธ CategoryTheory.Limits.terminalIsTerminal).from (๐.obj U)
def StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} {๐ : } {c : C} (f : ๐.stalk pโ โถ c) :
๐ โถ skyscraperPresheaf pโ c

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
def StalkSkyscraperPresheafAdjunctionAuxs.fromStalk {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} {๐ : } {c : C} (f : ๐ โถ skyscraperPresheaf pโ c) :
๐.stalk pโ โถ c

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
theorem StalkSkyscraperPresheafAdjunctionAuxs.to_skyscraper_fromStalk {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} {๐ : } {c : C} (f : ๐ โถ skyscraperPresheaf pโ c) :
theorem StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} {๐ : } {c : C} (f : ๐.stalk pโ โถ c) :
@[simp]
theorem StalkSkyscraperPresheafAdjunctionAuxs.unit_app {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (๐ : ) :
.app ๐ = StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf pโ (CategoryTheory.CategoryStruct.id ((.obj ๐).stalk pโ))
def StalkSkyscraperPresheafAdjunctionAuxs.unit {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} :
โถ ().comp ()

The unit in Presheaf.stalkFunctor โฃ skyscraperPresheafFunctor

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem StalkSkyscraperPresheafAdjunctionAuxs.counit_app {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} (c : C) :
.app c = ().hom
def StalkSkyscraperPresheafAdjunctionAuxs.counit {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} :
().comp () โถ

The counit in Presheaf.stalkFunctor โฃ skyscraperPresheafFunctor

Equations
• = { app := fun (c : C) => ().hom, naturality := โฏ }
Instances For
def skyscraperPresheafStalkAdjunction {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} :

skyscraperPresheafFunctor is the right adjoint of Presheaf.stalkFunctor

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} :
Equations
• โฏ = โฏ
instance instIsLeftAdjointPresheafStalkFunctor {X : TopCat} (pโ : โX) {C : Type v} :
Equations
• โฏ = โฏ
def stalkSkyscraperSheafAdjunction {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} :
().comp () โฃ

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.
Instances For
instance instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits {X : TopCat} (pโ : โX) [(U : ) โ Decidable (pโ โ U)] {C : Type v} :