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. TODO(@joelriou): refactor the definitions in this file so as to make them particular cases of general constructions for points of sites from Mathlib/CategoryTheory/Sites/Point/Skyscraper.lean.

noncomputable def skyscraperPresheaf {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) : TopCat.Presheaf 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.

@[simp]

theorem skyscraperPresheaf_obj {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (skyscraperPresheaf p₀ A).obj U = if p₀ ∈ Opposite.unop U then A else ⊤_ C

@[simp]

theorem skyscraperPresheaf_map {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : (skyscraperPresheaf p₀ A).map i = if h : p₀ ∈ Opposite.unop V then CategoryTheory.eqToHom ⋯ else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (if p₀ ∈ Opposite.unop U then A else ⊤_ C)

theorem skyscraperPresheaf_eq_pushforward {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) [hd : (U : TopologicalSpace.Opens ↑(TopCat.of PUnit.{u + 1})) → Decidable (PUnit.unit ∈ U)] : skyscraperPresheaf p₀ A = (TopCat.Presheaf.pushforward C (TopCat.ofHom (ContinuousMap.const (↑(TopCat.of PUnit.{u + 1})) p₀))).obj (skyscraperPresheaf PUnit.unit A)

noncomputable def SkyscraperPresheafFunctor.map' {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] {a b : C} (f : a ⟶ b) : skyscraperPresheaf p₀ a ⟶ skyscraperPresheaf p₀ 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.

@[simp]

theorem SkyscraperPresheafFunctor.map'_app {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] {a b : C} (f : a ⟶ b) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (map' p₀ f).app U = if h : p₀ ∈ Opposite.unop U then CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯)) else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)

theorem SkyscraperPresheafFunctor.map'_id {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] {a : C} : map' p₀ (CategoryTheory.CategoryStruct.id a) = CategoryTheory.CategoryStruct.id (skyscraperPresheaf p₀ a)

theorem SkyscraperPresheafFunctor.map'_comp {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] {a b c : C} (f : a ⟶ b) (g : b ⟶ c) : map' p₀ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (map' p₀ f) (map' p₀ g)

noncomputable def skyscraperPresheafFunctor {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor C (TopCat.Presheaf 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.

@[simp]

theorem skyscraperPresheafFunctor_obj {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) : (skyscraperPresheafFunctor p₀).obj A = skyscraperPresheaf p₀ A

@[simp]

theorem skyscraperPresheafFunctor_map {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : (skyscraperPresheafFunctor p₀).map f = SkyscraperPresheafFunctor.map' p₀ f

def skyscraperPresheafCoconeOfSpecializes {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : p₀ ⤳ y) : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A))

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

@[simp]

theorem skyscraperPresheafCoconeOfSpecializes_ι_app {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : p₀ ⤳ y) (U : (TopologicalSpace.OpenNhds y)ᵒᵖ) : (skyscraperPresheafCoconeOfSpecializes p₀ A h).ι.app U = CategoryTheory.eqToHom ⋯

@[simp]

theorem skyscraperPresheafCoconeOfSpecializes_pt {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : p₀ ⤳ y) : (skyscraperPresheafCoconeOfSpecializes p₀ A h).pt = A

noncomputable def skyscraperPresheafCoconeIsColimitOfSpecializes {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : p₀ ⤳ y) : CategoryTheory.Limits.IsColimit (skyscraperPresheafCoconeOfSpecializes p₀ A h)

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

noncomputable def skyscraperPresheafStalkOfSpecializes {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits 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.

@[simp]

theorem germ_skyscraperPresheafStalkOfSpecializes_hom {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y) (U : TopologicalSpace.Opens ↑X) (hU : y ∈ U) : CategoryTheory.CategoryStruct.comp ((skyscraperPresheaf p₀ A).germ U y hU) (skyscraperPresheafStalkOfSpecializes p₀ A h).hom = CategoryTheory.eqToHom ⋯

@[simp]

theorem germ_skyscraperPresheafStalkOfSpecializes_hom_assoc {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y) (U : TopologicalSpace.Opens ↑X) (hU : y ∈ U) {Z : C} (h✝ : A ⟶ Z) : CategoryTheory.CategoryStruct.comp ((skyscraperPresheaf p₀ A).germ U y hU) (CategoryTheory.CategoryStruct.comp (skyscraperPresheafStalkOfSpecializes p₀ A h).hom h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h✝

noncomputable def skyscraperPresheafCocone {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] (y : ↑X) : CategoryTheory.Limits.Cocone ((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A))

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

@[simp]

theorem skyscraperPresheafCocone_ι_app {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] (y : ↑X) (x✝ : (TopologicalSpace.OpenNhds y)ᵒᵖ) : (skyscraperPresheafCocone p₀ A y).ι.app x✝ = CategoryTheory.Limits.terminal.from (((TopologicalSpace.OpenNhds.inclusion y).op.comp (skyscraperPresheaf p₀ A)).obj x✝)

@[simp]

theorem skyscraperPresheafCocone_pt {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] (y : ↑X) : (skyscraperPresheafCocone p₀ A y).pt = ⊤_ C

noncomputable def skyscraperPresheafCoconeIsColimitOfNotSpecializes {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] {y : ↑X} (h : ¬p₀ ⤳ y) : CategoryTheory.Limits.IsColimit (skyscraperPresheafCocone p₀ A y)

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

noncomputable def skyscraperPresheafStalkOfNotSpecializes {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits 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.

noncomputable def skyscraperPresheafStalkOfNotSpecializesIsTerminal {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : ¬p₀ ⤳ y) : CategoryTheory.Limits.IsTerminal ((skyscraperPresheaf p₀ A).stalk y)

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

theorem skyscraperPresheaf_isSheaf {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] : (skyscraperPresheaf p₀ A).IsSheaf

noncomputable def skyscraperSheaf {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] (A : C) [CategoryTheory.Limits.HasTerminal C] : TopCat.Sheaf 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.

noncomputable def skyscraperSheafFunctor {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] : CategoryTheory.Functor C (TopCat.Sheaf 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.

noncomputable def StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {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.

@[simp]

theorem StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf_app {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (toSkyscraperPresheaf p₀ f).app U = if h : p₀ ∈ Opposite.unop U then CategoryTheory.CategoryStruct.comp (𝓕.germ (Opposite.unop U) p₀ h) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯)) else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from (𝓕.obj U)

noncomputable def StalkSkyscraperPresheafAdjunctionAuxs.fromStalk {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {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.

@[simp]

theorem StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕 ⟶ skyscraperPresheaf p₀ c) (U : TopologicalSpace.Opens ↑X) (hU : p₀ ∈ U) : CategoryTheory.CategoryStruct.comp (𝓕.germ U p₀ hU) (fromStalk p₀ f) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (CategoryTheory.eqToHom ⋯)

@[simp]

theorem StalkSkyscraperPresheafAdjunctionAuxs.germ_fromStalk_assoc {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕 ⟶ skyscraperPresheaf p₀ c) (U : TopologicalSpace.Opens ↑X) (hU : p₀ ∈ U) {Z : C} (h : c ⟶ Z) : CategoryTheory.CategoryStruct.comp (𝓕.germ U p₀ hU) (CategoryTheory.CategoryStruct.comp (fromStalk p₀ f) h) = CategoryTheory.CategoryStruct.comp (f.app (Opposite.op U)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

theorem StalkSkyscraperPresheafAdjunctionAuxs.to_skyscraper_fromStalk {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕 ⟶ skyscraperPresheaf p₀ c) : toSkyscraperPresheaf p₀ (fromStalk p₀ f) = f

theorem StalkSkyscraperPresheafAdjunctionAuxs.fromStalk_to_skyscraper {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] {𝓕 : TopCat.Presheaf C X} {c : C} (f : 𝓕.stalk p₀ ⟶ c) : fromStalk p₀ (toSkyscraperPresheaf p₀ f) = f

noncomputable def StalkSkyscraperPresheafAdjunctionAuxs.unit {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : CategoryTheory.Functor.id (TopCat.Presheaf C X) ⟶ (TopCat.Presheaf.stalkFunctor C p₀).comp (skyscraperPresheafFunctor p₀)

The unit in Presheaf.stalkFunctor ⊣ skyscraperPresheafFunctor

@[simp]

theorem StalkSkyscraperPresheafAdjunctionAuxs.unit_app {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] (x✝ : TopCat.Presheaf C X) : (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app x✝ = toSkyscraperPresheaf p₀ (CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.id (TopCat.Presheaf C X)).obj x✝).stalk p₀))

noncomputable def StalkSkyscraperPresheafAdjunctionAuxs.counit {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : (skyscraperPresheafFunctor p₀).comp (TopCat.Presheaf.stalkFunctor C p₀) ⟶ CategoryTheory.Functor.id C

The counit in Presheaf.stalkFunctor ⊣ skyscraperPresheafFunctor

@[simp]

theorem StalkSkyscraperPresheafAdjunctionAuxs.counit_app {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] (c : C) : (StalkSkyscraperPresheafAdjunctionAuxs.counit p₀).app c = (skyscraperPresheafStalkOfSpecializes p₀ c ⋯).hom

noncomputable def skyscraperPresheafStalkAdjunction {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : TopCat.Presheaf.stalkFunctor C p₀ ⊣ skyscraperPresheafFunctor p₀

skyscraperPresheafFunctor is the right adjoint of Presheaf.stalkFunctor

instance instIsRightAdjointPresheafSkyscraperPresheafFunctorOfHasColimits {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : (skyscraperPresheafFunctor p₀).IsRightAdjoint

instance instIsLeftAdjointPresheafStalkFunctor {X : TopCat} (p₀ : ↑X) {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : (TopCat.Presheaf.stalkFunctor C p₀).IsLeftAdjoint

noncomputable def stalkSkyscraperSheafAdjunction {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : (TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C p₀) ⊣ skyscraperSheafFunctor p₀

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

instance instIsLeftAdjointSheafCompPresheafForgetStalkFunctor {X : TopCat} (p₀ : ↑X) {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : ((TopCat.Sheaf.forget C X).comp (TopCat.Presheaf.stalkFunctor C p₀)).IsLeftAdjoint

instance instIsRightAdjointSheafSkyscraperSheafFunctorOfHasColimits {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : (skyscraperSheafFunctor p₀).IsRightAdjoint

noncomputable def skyscraperSheafForgetAdjunction {X : TopCat} (p₀ : ↑X) [(U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{u, v} C] [CategoryTheory.Limits.HasTerminal C] [CategoryTheory.Limits.HasColimits C] : TopCat.Presheaf.stalkFunctor C p₀ ⊣ (skyscraperSheafFunctor p₀).comp (TopCat.Sheaf.forget C X)

Taking stalks is the left adjoint of skyscraperSheafFunctor ⋙ Sheaf.forget. Useful only when the fact that skyscraperPresheafFunctor factors through Sheaf C X is relevant.