def
Top.presheaf.stalk_functor
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(x : ↥X) :
Top.presheaf C X ⥤ C
Stalks are functorial with respect to morphisms of presheaves over a fixed X.
def
Top.presheaf.stalk
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(ℱ : Top.presheaf C X)
(x : ↥X) :
C
The stalk of a presheaf F at a point x is calculated as the colimit of the functor
nbhds x ⥤ opens F.X ⥤ C
Equations
- ℱ.stalk x = (Top.presheaf.stalk_functor C x).obj ℱ
@[simp]
theorem
Top.presheaf.stalk_functor_obj
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(ℱ : Top.presheaf C X)
(x : ↥X) :
(Top.presheaf.stalk_functor C x).obj ℱ = ℱ.stalk x
def
Top.presheaf.germ
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(F : Top.presheaf C X)
{U : topological_space.opens ↥X}
(x : ↥U) :
F.obj (opposite.op U) ⟶ F.stalk ↑x
The germ of a section of a presheaf over an open at a point of that open.
Equations
- F.germ x = category_theory.limits.colimit.ι ((topological_space.open_nhds.inclusion x.val).op ⋙ F) (opposite.op ⟨U, _⟩)
theorem
Top.presheaf.germ_exist
{X : Top}
(F : Top.presheaf (Type v) X)
(x : ↥X)
(t : F.stalk x) :
∃ (U : topological_space.opens ↥X) (m : x ∈ U) (s : F.obj (opposite.op U)), F.germ ⟨x, m⟩ s = t
For a Type valued presheaf, every point in a stalk is a germ.
theorem
Top.presheaf.germ_eq
{X : Top}
(F : Top.presheaf (Type v) X)
{U V : topological_space.opens ↥X}
(x : ↥X)
(mU : x ∈ U)
(mV : x ∈ V)
(s : F.obj (opposite.op U))
(t : F.obj (opposite.op V))
(h : F.germ ⟨x, mU⟩ s = F.germ ⟨x, mV⟩ t) :
@[simp]
theorem
Top.presheaf.germ_res
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(F : Top.presheaf C X)
{U V : topological_space.opens ↥X}
(i : U ⟶ V)
(x : ↥U) :
@[simp]
theorem
Top.presheaf.germ_res_apply
{X : Top}
(F : Top.presheaf (Type v) X)
{U V : topological_space.opens ↥X}
(i : U ⟶ V)
(x : ↥U)
(f : F.obj (opposite.op V)) :
@[simp]
theorem
Top.presheaf.germ_res_apply'
{X : Top}
(F : Top.presheaf (Type v) X)
{U V : (topological_space.opens ↥X)ᵒᵖ}
(i : V ⟶ U)
(x : ↥(opposite.unop U))
(f : F.obj V) :
A variant when the open sets are written in (opens X)ᵒᵖ.
@[ext]
theorem
Top.presheaf.germ_ext
{X : Top}
{D : Type u}
[category_theory.category D]
[category_theory.concrete_category D]
[category_theory.limits.has_colimits D]
(F : Top.presheaf D X)
{U V : topological_space.opens ↥X}
{x : ↥X}
{hxU : x ∈ U}
{hxV : x ∈ V}
(W : topological_space.opens ↥X)
(hxW : x ∈ W)
(iWU : W ⟶ U)
(iWV : W ⟶ V)
{sU : ↥(F.obj (opposite.op U))}
{sV : ↥(F.obj (opposite.op V))}
(ih : ⇑(F.map iWU.op) sU = ⇑(F.map iWV.op) sV) :
theorem
Top.presheaf.stalk_hom_ext
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(F : Top.presheaf C X)
{x : ↥X}
{Y : C}
{f₁ f₂ : F.stalk x ⟶ Y}
(ih : ∀ (U : topological_space.opens ↥X) (hxU : x ∈ U), F.germ ⟨x, hxU⟩ ≫ f₁ = F.germ ⟨x, hxU⟩ ≫ f₂) :
f₁ = f₂
def
Top.presheaf.stalk_pushforward
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y : Top}
(f : X ⟶ Y)
(ℱ : Top.presheaf C X)
(x : ↥X) :
Equations
- Top.presheaf.stalk_pushforward C f ℱ x = category_theory.limits.colim.map (category_theory.whisker_right (category_theory.nat_trans.op (topological_space.open_nhds.inclusion_map_iso f x).inv) ℱ) ≫ category_theory.limits.colimit.pre (((category_theory.whiskering_left (topological_space.open_nhds x)ᵒᵖ (topological_space.opens ↥X)ᵒᵖ C).obj (topological_space.open_nhds.inclusion x).op).obj ℱ) (topological_space.open_nhds.map f x).op
@[simp]
theorem
Top.presheaf.stalk_pushforward.id
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X : Top}
(ℱ : Top.presheaf C X)
(x : ↥X) :
Top.presheaf.stalk_pushforward C (𝟙 X) ℱ x = (Top.presheaf.stalk_functor C x).map (Top.presheaf.pushforward.id ℱ).hom
@[simp]
theorem
Top.presheaf.stalk_pushforward.comp
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_colimits C]
{X Y Z : Top}
(ℱ : Top.presheaf C X)
(f : X ⟶ Y)
(g : Y ⟶ Z)
(x : ↥X) :
Top.presheaf.stalk_pushforward C (f ≫ g) ℱ x = Top.presheaf.stalk_pushforward C g (f _* ℱ) (⇑f x) ≫ Top.presheaf.stalk_pushforward C f ℱ x