Additive maps from stalks

Compatible additive maps on sections of an additive-group-valued presheaf induce an additive map from each stalk. Its value on a germ is the prescribed value of the section map.

noncomputable def TopCat.Presheaf.stalkLiftAddHom {X : TopCat} (F : Presheaf AddCommGrpCat X) (x : ↑X) {T : Type u} [AddCommGroup T] (f : (U : TopologicalSpace.Opens ↑X) → x ∈ U → ↑(F.obj (Opposite.op U)) →+ T) (hf : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (hx : x ∈ U) (m : ↑(F.obj (Opposite.op V))), (f U hx) ((CategoryTheory.ConcreteCategory.hom (F.map i.op)) m) = (f V ⋯) m) : ↑(F.stalk x) →+ T

The additive universal property of a presheaf stalk, using maps compatible with restriction.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TopCat.Presheaf.stalkLiftAddHom_germ {X : TopCat} (F : Presheaf AddCommGrpCat X) (x : ↑X) {T : Type u} [AddCommGroup T] (f : (U : TopologicalSpace.Opens ↑X) → x ∈ U → ↑(F.obj (Opposite.op U)) →+ T) (hf : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (hx : x ∈ U) (m : ↑(F.obj (Opposite.op V))), (f U hx) ((CategoryTheory.ConcreteCategory.hom (F.map i.op)) m) = (f V ⋯) m) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (m : ↑(F.obj (Opposite.op U))) : (F.stalkLiftAddHom x f ⋯) ((CategoryTheory.ConcreteCategory.hom (F.germ U x hx)) m) = (f U hx) m

The additive map induced from compatible section maps takes a germ to its prescribed value.