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 : 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).toPrefunctor.map i = if h : p₀ ∈ V.unop then CategoryTheory.eqToHom (_ : (fun (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) => if p₀ ∈ U.unop then A else ⊤_ C) U = (fun (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) => 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 : (TopologicalSpace.Opens ↑X)ᵒᵖ) => 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).toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

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).toPrefunctor.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.

Equations

• One or more equations did not get rendered due to their size.

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_1 Y : C} (f : X_1 ⟶ Y), (skyscraperPresheafFunctor p₀).toPrefunctor.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₀).toPrefunctor.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.

Equations

• skyscraperPresheafFunctor p₀ = CategoryTheory.Functor.mk { obj := skyscraperPresheaf p₀, map := fun {X_1 Y : C} => SkyscraperPresheafFunctor.map' p₀ }

@[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 skyscraperPresheaf p₀ A when y ∈ closure {p₀}

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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 skyscraperPresheaf p₀ A at y is A.

Equations

• One or more equations did not get rendered due to their size.

@[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)).toPrefunctor.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 skyscraperPresheaf p₀ A when y ∉ closure {p₀}

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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 skyscraperPresheaf p₀ A at y is isomorphic to a terminal object.

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• skyscraperPresheafStalkOfNotSpecializesIsTerminal p₀ A h = CategoryTheory.Limits.IsTerminal.ofIso CategoryTheory.Limits.terminalIsTerminal (skyscraperPresheafStalkOfNotSpecializes p₀ A h).symm

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.

Equations

• skyscraperSheaf p₀ A = { val := skyscraperPresheaf p₀ A, cond := (_ : TopCat.Presheaf.IsSheaf (skyscraperPresheaf p₀ A)) }

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.

Equations

• One or more equations did not get rendered due to their size.

@[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) (𝓕.toPrefunctor.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 𝓕 ⟶ 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.

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 : 𝓕 ⟶ 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.

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)).toPrefunctor.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.stalkFunctor ⊣ skyscraperPresheafFunctor

Equations

• One or more equations did not get rendered due to their size.

@[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.stalkFunctor ⊣ skyscraperPresheafFunctor

Equations

• StalkSkyscraperPresheafAdjunctionAuxs.counit p₀ = CategoryTheory.NatTrans.mk fun (c : C) => (skyscraperPresheafStalkOfSpecializes p₀ c (_ : p₀ ⤳ p₀)).hom

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• instIsLeftAdjointPresheafInstCategoryPresheafStalkFunctor p₀ = { right := skyscraperPresheafFunctor p₀, adj := skyscraperPresheafStalkAdjunction 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 skyscraperSheafFunctor

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.