mathlib documentation

topology.sheaves.stalks

Stalks #

For a presheaf F on a topological space X, valued in some category C, the stalk of F at the point x : X is defined as the colimit of the following functor

(nhds x)ᵒᵖ ⥤ (opens X)ᵒᵖ ⥤ C

where the functor on the left is the inclusion of categories and the functor on the right is F. For an open neighborhood U of x, we define the map F.germ x : F.obj (op U) ⟶ F.stalk x as the canonical morphism into this colimit.

Taking stalks is functorial: For every point x : X we define a functor stalk_functor C x, sending presheaves on X to objects of C. In is_iso_iff_stalk_functor_map_iso, we prove that a map f : F ⟶ G between Type-valued sheaves is an isomorphism if and only if all the maps F.stalk x ⟶ G.stalk x (given by the stalk functor on f) are isomorphisms.

For a map f : X ⟶ Y between topological spaces, we define stalk_pushforward as the induced map on the stalks (f _* ℱ).stalk (f x) ⟶ ℱ.stalk x.

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)) (h : 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))} (ih : (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} (ih : ∀ (U : topological_space.opens X) (hxU : x U), F.germ x, hxU⟩ f₁ = F.germ x, hxU⟩ f₂) :
f₁ = f₂
theorem Top.presheaf.section_ext {X : Top} (F : Top.sheaf (Type v) X) (U : topological_space.opens X) (s t : F.presheaf.obj (opposite.op U)) :
(∀ (x : U), F.presheaf.germ x s = F.presheaf.germ x t)s = t

If two sections agree on all stalks, they must be equal

@[simp]
theorem Top.presheaf.stalk_functor_map_germ_apply {X : Top} (U : topological_space.opens X) (x : U) {F G : Top.presheaf (Type v) X} (f : F G) (s : F.obj (opposite.op U)) :
(Top.presheaf.stalk_functor (Type v) x.val).map f (F.germ x s) = G.germ x (f.app (opposite.op U) s)

If all the stalk maps of map f : F ⟶ G of Type-valued sheaves are isomorphisms, then f is an isomorphism.

A morphism of Type-valued sheaves f : F ⟶ G is an isomorphism if and only if all the stalk maps are isomorphisms