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 : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v} [CategoryTheory.Category.{w, v} C] [CategoryTheory.Limits.HasTerminal C] (A : C) {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {V : (TopologicalSpace.Opens ↑X)ᵒᵖ} (i : U ⟶ V) : (skyscraperPresheaf p₀ A).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 : 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₀ ∈ U.unop then A else ⊤_ C

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.

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 = ContinuousMap.const (↑(TopCat.of PUnit.{u + 1} )) p₀ _* skyscraperPresheaf PUnit.unit A

@[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 : C} {b : C} (f : a ⟶ b) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (SkyscraperPresheafFunctor.map' p₀ f).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) ((skyscraperPresheaf p₀ a).obj U)

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 : C} {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.

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} : SkyscraperPresheafFunctor.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 : C} {b : C} {c : C} (f : a ⟶ b) (g : b ⟶ c) : SkyscraperPresheafFunctor.map' p₀ (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (SkyscraperPresheafFunctor.map' p₀ f) (SkyscraperPresheafFunctor.map' p₀ g)

@[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

@[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

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

@[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 (_ : (if p₀ ∈ U.unop.obj.carrier then A else ⊤_ C) = A)

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 (CategoryTheory.Functor.comp (TopologicalSpace.OpenNhds.inclusion y).op (skyscraperPresheaf p₀ A))

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

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 skyscraper_presheaf 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) : TopCat.Presheaf.stalk (skyscraperPresheaf p₀ A) y ≅ A

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

@[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 ((CategoryTheory.Functor.comp (TopologicalSpace.OpenNhds.inclusion y).op (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

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 (CategoryTheory.Functor.comp (TopologicalSpace.OpenNhds.inclusion y).op (skyscraperPresheaf p₀ A))

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

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 skyscraper_presheaf 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) : TopCat.Presheaf.stalk (skyscraperPresheaf p₀ A) y ≅ ⊤_ C

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

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 (TopCat.Presheaf.stalk (skyscraperPresheaf p₀ A) y)

If y ∉ closure {p₀}, then the stalk of skyscraper_presheaf 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] : TopCat.Presheaf.IsSheaf (skyscraperPresheaf p₀ A)

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.

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.

@[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 : TopCat.Presheaf.stalk 𝓕 p₀ ⟶ c) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f).app 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 : 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 : TopCat.Presheaf.stalk 𝓕 p₀ ⟶ c) : 𝓕 ⟶ skyscraperPresheaf 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.

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) : TopCat.Presheaf.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.

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) : StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ (StalkSkyscraperPresheafAdjunctionAuxs.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 : TopCat.Presheaf.stalk 𝓕 p₀ ⟶ c) : StalkSkyscraperPresheafAdjunctionAuxs.fromStalk p₀ (StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ f) = f

@[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] (𝓕 : TopCat.Presheaf C X) : (StalkSkyscraperPresheafAdjunctionAuxs.unit p₀).app 𝓕 = StalkSkyscraperPresheafAdjunctionAuxs.toSkyscraperPresheaf p₀ (CategoryTheory.CategoryStruct.id (TopCat.Presheaf.stalk ((CategoryTheory.Functor.id (TopCat.Presheaf C X)).obj 𝓕) p₀))

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) ⟶ CategoryTheory.Functor.comp (TopCat.Presheaf.stalkFunctor C p₀) (skyscraperPresheafFunctor p₀)

The unit in presheaf.stalk ⊣ skyscraper_presheaf_functor

@[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 (_ : p₀ ⤳ p₀)).hom

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] : CategoryTheory.Functor.comp (skyscraperPresheafFunctor p₀) (TopCat.Presheaf.stalkFunctor C p₀) ⟶ CategoryTheory.Functor.id C

The counit in presheaf.stalk ⊣ skyscraper_presheaf_functor

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₀

skyscraper_presheaf_functor is the right adjoint of presheaf.stalk_functor

instance instIsRightAdjointPresheafInstCategoryPresheafSkyscraperPresheafFunctorOpensαTopologicalSpaceTopologicalSpace_coe {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.IsRightAdjoint (skyscraperPresheafFunctor p₀)

instance instIsLeftAdjointPresheafInstCategoryPresheafStalkFunctor {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.IsLeftAdjoint (TopCat.Presheaf.stalkFunctor C p₀)

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] : CategoryTheory.Functor.comp (TopCat.Sheaf.forget C X) (TopCat.Presheaf.stalkFunctor C p₀) ⊣ skyscraperSheafFunctor p₀

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

instance instIsRightAdjointSheafSheafCatSkyscraperSheafFunctorOpensαTopologicalSpaceTopologicalSpace_coe {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.IsRightAdjoint (skyscraperSheafFunctor p₀)