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.

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.

@[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 : (TopologicalSpace.Opens ↑X)ᵒᵖ} {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 ((fun (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) => if p₀ ∈ Opposite.unop U then A else ⊤_ C) U)

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

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.

@[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₀ ∈ 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} : 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)

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₀ = { obj := skyscraperPresheaf p₀, map := fun {X_1 Y : C} => SkyscraperPresheafFunctor.map' p₀, map_id := ⋯, map_comp := ⋯ }

@[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_1 Y : C} (f : X_1 ⟶ 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₀}

Equations

• skyscraperPresheafCoconeOfSpecializes p₀ A h = { pt := A, ι := { app := fun (U : (TopologicalSpace.OpenNhds y)ᵒᵖ) => CategoryTheory.eqToHom ⋯, naturality := ⋯ } }

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

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) : (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.

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

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

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

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) : (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.

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

Equations

• skyscraperPresheafStalkOfNotSpecializesIsTerminal p₀ A h = CategoryTheory.Limits.terminalIsTerminal.ofIso (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] : (skyscraperPresheaf p₀ A).IsSheaf

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 := ⋯ }

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.

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.

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 : 𝓕.stalk p₀ ⟶ c) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (StalkSkyscraperPresheafAdjunctionAuxs.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)

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.

Equations

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

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

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

Equations

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

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

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

Equations

• StalkSkyscraperPresheafAdjunctionAuxs.counit p₀ = { app := fun (c : C) => (skyscraperPresheafStalkOfSpecializes p₀ c ⋯).hom, naturality := ⋯ }

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

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

Equations

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

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

Equations

• ⋯ = ⋯