mathlib documentation

topology.sheaves.stalks

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

The germ of a section of a presheaf over an open at a point of that open.

Equations
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)) :
F.germ x, mU⟩ s = F.germ x, mV⟩ t(∃ (W : topological_space.opens X) (m : x W) (iU : W U) (iV : W V), F.map iU.op s = F.map iV.op 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) :
F.map i.op F.germ x = F.germ (i x)

@[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)) :
F.germ x (F.map i.op f) = F.germ (i x) f

@[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) :
F.germ x (F.map i f) = F.germ ((i.unop) x) f

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))} :
(F.map iWU.op) sU = (F.map iWV.op) sV(F.germ x, hxU⟩) sU = (F.germ x, hxV⟩) 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} :
(∀ (U : topological_space.opens X) (hxU : x U), F.germ x, hxU⟩ f₁ = F.germ x, hxU⟩ f₂)f₁ = f₂