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) :
skyscraper_presheaf_functor.map' pā (f ā« g) = skyscraper_presheaf_functor.map' pā f ā« skyscraper_presheaf_functor.map' pā g
@[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) :
(skyscraper_presheaf_functor pā).map f = skyscraper_presheaf_functor.map' pā f
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)įµįµ) :
(skyscraper_presheaf_cocone_of_specializes pā A h).Ī¹.app U = category_theory.eq_to_hom _
@[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.
Equations
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.
Equations
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) :
category_theory.limits.is_terminal ((skyscraper_presheaf pā A).stalk 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) :
(stalk_skyscraper_presheaf_adjunction_auxs.counit pā).app c = (skyscraper_presheaf_stalk_of_specializes pā c _).hom
@[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] :
Top.presheaf.stalk_functor C pā ā£ skyscraper_presheaf_functor pā
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
- skyscraper_presheaf_functor.category_theory.is_right_adjoint pā = {left := Top.presheaf.stalk_functor C pā, adj := skyscraper_presheaf_stalk_adjunction pā _inst_4}
@[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] :
Top.sheaf.forget C X ā Top.presheaf.stalk_functor C pā ā£ skyscraper_sheaf_functor pā
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}