Skyscraper (pre)sheaves #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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₀ Ais the skyscraper presheaf at pointp₀with valueA.skyscraper_sheaf: the skyscraper presheaf satisfies the sheaf condition.
Main statements #
skyscraper_presheaf_stalk_of_specializes: ify ∈ closure {p₀}then the stalk ofskyscraper_presheaf p₀ AatyisA.skyscraper_presheaf_stalk_of_not_specializes: ify ∉ closure {p₀}then the stalk ofskyscraper_presheaf p₀ Aatyis*the terminal object.
TODO: generalize universe level when calculating stalks, after generalizing universe level of stalk.
@[simp]
theorem
skyscraper_presheaf_obj
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(A : C)
(U : (topological_space.opens ↥X)ᵒᵖ) :
(skyscraper_presheaf p₀ A).obj U = ite (p₀ ∈ opposite.unop U) A (⊤_ C)
@[simp]
theorem
skyscraper_presheaf_map
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(A : C)
(U V : (topological_space.opens ↥X)ᵒᵖ)
(i : U ⟶ V) :
(skyscraper_presheaf p₀ A).map i = dite (p₀ ∈ opposite.unop V) (λ (h : p₀ ∈ opposite.unop V), category_theory.eq_to_hom _) (λ (h : p₀ ∉ opposite.unop V), (eq.rec category_theory.limits.terminal_is_terminal _).from (ite (p₀ ∈ opposite.unop U) A (⊤_ C)))
noncomputable
def
skyscraper_presheaf
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(A : C) :
Top.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
- skyscraper_presheaf p₀ A = {obj := λ (U : (topological_space.opens ↥X)ᵒᵖ), ite (p₀ ∈ opposite.unop U) A (⊤_ C), map := λ (U V : (topological_space.opens ↥X)ᵒᵖ) (i : U ⟶ V), dite (p₀ ∈ opposite.unop V) (λ (h : p₀ ∈ opposite.unop V), category_theory.eq_to_hom _) (λ (h : p₀ ∉ opposite.unop V), (eq.rec category_theory.limits.terminal_is_terminal _).from (ite (p₀ ∈ opposite.unop U) A (⊤_ C))), map_id' := _, map_comp' := _}
theorem
skyscraper_presheaf_eq_pushforward
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(A : C)
[hd : Π (U : topological_space.opens ↥(Top.of punit)), decidable (punit.star ∈ U)] :
skyscraper_presheaf p₀ A = continuous_map.const ↥(Top.of punit) p₀ _* skyscraper_presheaf punit.star A
@[simp]
theorem
skyscraper_presheaf_functor.map'_app
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
{a b : C}
(f : a ⟶ b)
(U : (topological_space.opens ↥X)ᵒᵖ) :
(skyscraper_presheaf_functor.map' p₀ f).app U = dite (p₀ ∈ opposite.unop U) (λ (h : p₀ ∈ opposite.unop U), category_theory.eq_to_hom _ ≫ f ≫ category_theory.eq_to_hom _) (λ (h : p₀ ∉ opposite.unop U), (eq.rec category_theory.limits.terminal_is_terminal _).from ((skyscraper_presheaf p₀ a).obj U))
noncomputable
def
skyscraper_presheaf_functor.map'
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
{a b : C}
(f : a ⟶ b) :
skyscraper_presheaf p₀ a ⟶ skyscraper_presheaf 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
- skyscraper_presheaf_functor.map' p₀ f = {app := λ (U : (topological_space.opens ↥X)ᵒᵖ), dite (p₀ ∈ opposite.unop U) (λ (h : p₀ ∈ opposite.unop U), category_theory.eq_to_hom _ ≫ f ≫ category_theory.eq_to_hom _) (λ (h : p₀ ∉ opposite.unop U), (eq.rec category_theory.limits.terminal_is_terminal _).from ((skyscraper_presheaf p₀ a).obj U)), naturality' := _}
theorem
skyscraper_presheaf_functor.map'_id
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
{a : C} :
skyscraper_presheaf_functor.map' p₀ (𝟙 a) = 𝟙 (skyscraper_presheaf p₀ a)
theorem
skyscraper_presheaf_functor.map'_comp
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
{a b c : C}
(f : a ⟶ b)
(g : b ⟶ c) :
@[simp]
theorem
skyscraper_presheaf_functor_obj
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(A : C) :
(skyscraper_presheaf_functor p₀).obj A = skyscraper_presheaf p₀ A
@[simp]
theorem
skyscraper_presheaf_functor_map
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
(_x _x_1 : C)
(f : _x ⟶ _x_1) :
noncomputable
def
skyscraper_presheaf_functor
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C] :
C ⥤ Top.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
- skyscraper_presheaf_functor p₀ = {obj := skyscraper_presheaf p₀ _inst_3, map := λ (_x _x_1 : C), skyscraper_presheaf_functor.map' p₀, map_id' := _, map_comp' := _}
Instances for skyscraper_presheaf_functor
@[simp]
theorem
skyscraper_presheaf_cocone_of_specializes_ι_app
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
{y : ↥X}
(h : p₀ ⤳ y)
(U : (topological_space.open_nhds y)ᵒᵖ) :
@[simp]
theorem
skyscraper_presheaf_cocone_of_specializes_X
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
{y : ↥X}
(h : p₀ ⤳ y) :
(skyscraper_presheaf_cocone_of_specializes p₀ A h).X = A
noncomputable
def
skyscraper_presheaf_cocone_of_specializes
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
{y : ↥X}
(h : p₀ ⤳ y) :
The cocone at A for the stalk functor of skyscraper_presheaf p₀ A when y ∈ closure {p₀}
Equations
- skyscraper_presheaf_cocone_of_specializes p₀ A h = {X := A, ι := {app := λ (U : (topological_space.open_nhds y)ᵒᵖ), category_theory.eq_to_hom _, naturality' := _}}
noncomputable
def
skyscraper_presheaf_cocone_is_colimit_of_specializes
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
{y : ↥X}
(h : p₀ ⤳ y) :
The cocone at A for the stalk functor of skyscraper_presheaf p₀ A when y ∈ closure {p₀} is a
colimit
Equations
- skyscraper_presheaf_cocone_is_colimit_of_specializes p₀ A h = {desc := λ (c : category_theory.limits.cocone ((topological_space.open_nhds.inclusion y).op ⋙ skyscraper_presheaf p₀ A)), category_theory.eq_to_hom _ ≫ c.ι.app (opposite.op ⊤), fac' := _, uniq' := _}
noncomputable
def
skyscraper_presheaf_stalk_of_specializes
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
{y : ↥X}
(h : p₀ ⤳ y) :
(skyscraper_presheaf p₀ A).stalk y ≅ A
If y ∈ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is A.
noncomputable
def
skyscraper_presheaf_cocone
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
(y : ↥X) :
The cocone at * for the stalk functor of skyscraper_presheaf p₀ A when y ∉ closure {p₀}
Equations
- skyscraper_presheaf_cocone p₀ A y = {X := ⊤_ C, ι := {app := λ (U : (topological_space.open_nhds y)ᵒᵖ), category_theory.limits.terminal.from (((topological_space.open_nhds.inclusion y).op ⋙ skyscraper_presheaf p₀ A).obj U), naturality' := _}}
@[simp]
theorem
skyscraper_presheaf_cocone_ι_app
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
(y : ↥X)
(U : (topological_space.open_nhds y)ᵒᵖ) :
(skyscraper_presheaf_cocone p₀ A y).ι.app U = category_theory.limits.terminal.from (((topological_space.open_nhds.inclusion y).op ⋙ skyscraper_presheaf p₀ A).obj U)
@[simp]
theorem
skyscraper_presheaf_cocone_X
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
(y : ↥X) :
(skyscraper_presheaf_cocone p₀ A y).X = ⊤_ C
noncomputable
def
skyscraper_presheaf_cocone_is_colimit_of_not_specializes
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
{y : ↥X}
(h : ¬p₀ ⤳ y) :
The cocone at * for the stalk functor of skyscraper_presheaf p₀ A when y ∉ closure {p₀} is a
colimit
Equations
- skyscraper_presheaf_cocone_is_colimit_of_not_specializes p₀ A h = let h1 : ∃ (U : topological_space.open_nhds y), p₀ ∉ U.obj := _ in {desc := λ (c : category_theory.limits.cocone ((topological_space.open_nhds.inclusion y).op ⋙ skyscraper_presheaf p₀ A)), category_theory.eq_to_hom _ ≫ c.ι.app (opposite.op h1.some), fac' := _, uniq' := _}
noncomputable
def
skyscraper_presheaf_stalk_of_not_specializes
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
{y : ↥X}
(h : ¬p₀ ⤳ y) :
(skyscraper_presheaf p₀ A).stalk y ≅ ⊤_ C
If y ∉ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is isomorphic to a
terminal object.
noncomputable
def
skyscraper_presheaf_stalk_of_not_specializes_is_terminal
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
{y : ↥X}
(h : ¬p₀ ⤳ y) :
If y ∉ closure {p₀}, then the stalk of skyscraper_presheaf p₀ A at y is a terminal object
theorem
skyscraper_presheaf_is_sheaf
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C] :
(skyscraper_presheaf p₀ A).is_sheaf
noncomputable
def
skyscraper_sheaf
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
(A : C)
[category_theory.limits.has_terminal C] :
Top.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
- skyscraper_sheaf p₀ A = {val := skyscraper_presheaf p₀ A, cond := _}
noncomputable
def
skyscraper_sheaf_functor
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C] :
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
- skyscraper_sheaf_functor p₀ = {obj := λ (c : C), skyscraper_sheaf p₀ c, map := λ (a b : C) (f : a ⟶ b), {val := (skyscraper_presheaf_functor p₀).map f}, map_id' := _, map_comp' := _}
Instances for skyscraper_sheaf_functor
noncomputable
def
stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
{𝓕 : Top.presheaf C X}
{c : C}
(f : 𝓕.stalk p₀ ⟶ c) :
𝓕 ⟶ skyscraper_presheaf 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.
Equations
- stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf p₀ f = {app := λ (U : (topological_space.opens ↥X)ᵒᵖ), dite (p₀ ∈ opposite.unop U) (λ (h : p₀ ∈ opposite.unop U), 𝓕.germ ⟨p₀, h⟩ ≫ f ≫ category_theory.eq_to_hom _) (λ (h : p₀ ∉ opposite.unop U), (eq.rec category_theory.limits.terminal_is_terminal _).from (𝓕.obj U)), naturality' := _}
@[simp]
theorem
stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf_app
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
{𝓕 : Top.presheaf C X}
{c : C}
(f : 𝓕.stalk p₀ ⟶ c)
(U : (topological_space.opens ↥X)ᵒᵖ) :
(stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf p₀ f).app U = dite (p₀ ∈ opposite.unop U) (λ (h : p₀ ∈ opposite.unop U), 𝓕.germ ⟨p₀, h⟩ ≫ f ≫ category_theory.eq_to_hom _) (λ (h : p₀ ∉ opposite.unop U), (eq.rec category_theory.limits.terminal_is_terminal _).from (𝓕.obj U))
noncomputable
def
stalk_skyscraper_presheaf_adjunction_auxs.from_stalk
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
{𝓕 : Top.presheaf C X}
{c : C}
(f : 𝓕 ⟶ skyscraper_presheaf 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.
Equations
- stalk_skyscraper_presheaf_adjunction_auxs.from_stalk p₀ f = let χ : category_theory.limits.cocone ((topological_space.open_nhds.inclusion p₀).op ⋙ 𝓕) := {X := c, ι := {app := λ (U : (topological_space.open_nhds p₀)ᵒᵖ), f.app (opposite.op (opposite.unop U).obj) ≫ category_theory.eq_to_hom _, naturality' := _}} in category_theory.limits.colimit.desc ((topological_space.open_nhds.inclusion p₀).op ⋙ 𝓕) χ
theorem
stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_from_stalk
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
{𝓕 : Top.presheaf C X}
{c : C}
(f : 𝓕 ⟶ skyscraper_presheaf p₀ c) :
theorem
stalk_skyscraper_presheaf_adjunction_auxs.from_stalk_to_skyscraper
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
{𝓕 : Top.presheaf C X}
{c : C}
(f : 𝓕.stalk p₀ ⟶ c) :
@[simp]
theorem
stalk_skyscraper_presheaf_adjunction_auxs.unit_app
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
(𝓕 : Top.presheaf C X) :
(stalk_skyscraper_presheaf_adjunction_auxs.unit p₀).app 𝓕 = stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf p₀ (𝟙 (((𝟭 (Top.presheaf C X)).obj 𝓕).stalk p₀))
@[protected]
noncomputable
def
stalk_skyscraper_presheaf_adjunction_auxs.unit
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C] :
𝟭 (Top.presheaf C X) ⟶ Top.presheaf.stalk_functor C p₀ ⋙ skyscraper_presheaf_functor p₀
The unit in presheaf.stalk ⊣ skyscraper_presheaf_functor
Equations
- stalk_skyscraper_presheaf_adjunction_auxs.unit p₀ = {app := λ (𝓕 : Top.presheaf C X), stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf p₀ (𝟙 (((𝟭 (Top.presheaf C X)).obj 𝓕).stalk p₀)), naturality' := _}
@[simp]
theorem
stalk_skyscraper_presheaf_adjunction_auxs.counit_app
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C]
(c : C) :
@[protected]
noncomputable
def
stalk_skyscraper_presheaf_adjunction_auxs.counit
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C] :
skyscraper_presheaf_functor p₀ ⋙ Top.presheaf.stalk_functor C p₀ ⟶ 𝟭 C
The counit in presheaf.stalk ⊣ skyscraper_presheaf_functor
Equations
- stalk_skyscraper_presheaf_adjunction_auxs.counit p₀ = {app := λ (c : C), (skyscraper_presheaf_stalk_of_specializes p₀ c _).hom, naturality' := _}
noncomputable
def
skyscraper_presheaf_stalk_adjunction
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C] :
skyscraper_presheaf_functor is the right adjoint of presheaf.stalk_functor
Equations
- skyscraper_presheaf_stalk_adjunction p₀ = {hom_equiv := λ (c : Top.presheaf C X) (𝓕 : C), {to_fun := stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf p₀ 𝓕, inv_fun := stalk_skyscraper_presheaf_adjunction_auxs.from_stalk p₀ 𝓕, left_inv := _, right_inv := _}, unit := stalk_skyscraper_presheaf_adjunction_auxs.unit p₀ _inst_4, counit := stalk_skyscraper_presheaf_adjunction_auxs.counit p₀ _inst_4, hom_equiv_unit' := _, hom_equiv_counit' := _}
@[protected, instance]
noncomputable
def
skyscraper_presheaf_functor.category_theory.is_right_adjoint
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C] :
Equations
@[protected, instance]
noncomputable
def
Top.presheaf.stalk_functor.category_theory.is_left_adjoint
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C] :
Equations
- Top.presheaf.stalk_functor.category_theory.is_left_adjoint p₀ = {right := skyscraper_presheaf_functor p₀ _inst_3, adj := skyscraper_presheaf_stalk_adjunction p₀ _inst_4}
noncomputable
def
stalk_skyscraper_sheaf_adjunction
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C] :
Taking stalks of a sheaf is the left adjoint functor to skyscraper_sheaf_functor
Equations
- stalk_skyscraper_sheaf_adjunction p₀ = {hom_equiv := λ (𝓕 : Top.sheaf C X) (c : C), {to_fun := λ (f : (Top.sheaf.forget C X ⋙ Top.presheaf.stalk_functor C p₀).obj 𝓕 ⟶ c), {val := stalk_skyscraper_presheaf_adjunction_auxs.to_skyscraper_presheaf p₀ f}, inv_fun := λ (g : 𝓕 ⟶ (skyscraper_sheaf_functor p₀).obj c), stalk_skyscraper_presheaf_adjunction_auxs.from_stalk p₀ g.val, left_inv := _, right_inv := _}, unit := {app := λ (𝓕 : Top.sheaf C X), {val := (stalk_skyscraper_presheaf_adjunction_auxs.unit p₀).app 𝓕.val}, naturality' := _}, counit := stalk_skyscraper_presheaf_adjunction_auxs.counit p₀ _inst_4, hom_equiv_unit' := _, hom_equiv_counit' := _}
@[protected, instance]
noncomputable
def
skyscraper_sheaf_functor.category_theory.is_right_adjoint
{X : Top}
(p₀ : ↥X)
[Π (U : topological_space.opens ↥X), decidable (p₀ ∈ U)]
{C : Type v}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_colimits C] :
Equations
- skyscraper_sheaf_functor.category_theory.is_right_adjoint p₀ = {left := Top.sheaf.forget C X ⋙ Top.presheaf.stalk_functor C p₀, adj := stalk_skyscraper_sheaf_adjunction p₀ _inst_4}