Linear maps from stalks of presheaves of modules

Mathlib endows the stalk of a presheaf of modules with a module structure over the stalk of its ring presheaf, without requiring commutativity. This file gives its linear universal property: compatible additive maps on sections that respect scalar multiplication by germs induce a linear map from the stalk. Over commutative coefficients, germSemilinear bundles the germ map of sections as a map semilinear along the ring germ map, and stalkMapCommRing is the stalk map of a morphism, linear over the commutative-ring stalk. It also constructs the stalk map of a morphism defined on a neighborhood, for use with local morphisms such as sections of an internal Hom.

noncomputable def PresheafOfModules.stalkLift {X : TopCat} {R : TopCat.Presheaf RingCat X} (M : PresheafOfModules R) (x : ↑X) {T : Type u} [AddCommGroup T] [Module (↑(R.stalk x)) T] (f : (U : TopologicalSpace.Opens ↑X) → x ∈ U → ↑(M.obj (Opposite.op U)) →+ T) (hf : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (hx : x ∈ U) (m : ↑(M.obj (Opposite.op V))), (f U hx) ((CategoryTheory.ConcreteCategory.hom (M.map i.op)) m) = (f V ⋯) m) (hs : ∀ (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (r : ↑(R.obj (Opposite.op U))) (m : ↑(M.obj (Opposite.op U))), (f U hx) (r • m) = (CategoryTheory.ConcreteCategory.hom (R.germ U x hx)) r • (f U hx) m) : ↑(TopCat.Presheaf.stalk M.presheaf x) →ₗ[↑(R.stalk x)] T

Compatible section maps that are linear for the ring germ maps induce a linear map from the module stalk.

Equations

• M.stalkLift x f hf hs = { toFun := ⇑(TopCat.Presheaf.stalkLiftAddHom M.presheaf x f ⋯), map_add' := ⋯, map_smul' := ⋯ }

theorem PresheafOfModules.stalkLift_germ {X : TopCat} {R : TopCat.Presheaf RingCat X} (M : PresheafOfModules R) (x : ↑X) {T : Type u} [AddCommGroup T] [Module (↑(R.stalk x)) T] (f : (U : TopologicalSpace.Opens ↑X) → x ∈ U → ↑(M.obj (Opposite.op U)) →+ T) (hf : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (hx : x ∈ U) (m : ↑(M.obj (Opposite.op V))), (f U hx) ((CategoryTheory.ConcreteCategory.hom (M.map i.op)) m) = (f V ⋯) m) (hs : ∀ (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (r : ↑(R.obj (Opposite.op U))) (m : ↑(M.obj (Opposite.op U))), (f U hx) (r • m) = (CategoryTheory.ConcreteCategory.hom (R.germ U x hx)) r • (f U hx) m) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (m : ↑(M.obj (Opposite.op U))) : (M.stalkLift x f ⋯ hs) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf U x hx)) m) = (f U hx) m

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

noncomputable def PresheafOfModules.stalkLiftCommRing {X : TopCat} (x : ↑X) {T : Type u} [AddCommGroup T] {S : TopCat.Presheaf CommRingCat X} (N : PresheafOfModules (CategoryTheory.Functor.comp S (CategoryTheory.forget₂ CommRingCat RingCat))) [Module (↑(S.stalk x)) T] (f : (U : TopologicalSpace.Opens ↑X) → x ∈ U → ↑(N.obj (Opposite.op U)) →+ T) (hf : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (hx : x ∈ U) (m : ↑(N.obj (Opposite.op V))), (f U hx) ((CategoryTheory.ConcreteCategory.hom (N.map i.op)) m) = (f V ⋯) m) (hs : ∀ (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (r : ↑(S.obj (Opposite.op U))) (m : ↑(N.obj (Opposite.op U))), (f U hx) (r • m) = (CategoryTheory.ConcreteCategory.hom (S.germ U x hx)) r • (f U hx) m) : ↑(TopCat.Presheaf.stalk N.presheaf x) →ₗ[↑(S.stalk x)] T

Compatible section maps linear for the original commutative-ring germs induce a linear map from the module stalk. This retains the commutative-ring stalk carrier, which differs from the stalk of the presheaf obtained by forgetting commutativity.

Equations

• PresheafOfModules.stalkLiftCommRing x N f hf hs = { toFun := ⇑(TopCat.Presheaf.stalkLiftAddHom N.presheaf x f ⋯), map_add' := ⋯, map_smul' := ⋯ }

theorem PresheafOfModules.stalkLiftCommRing_germ {X : TopCat} (x : ↑X) {T : Type u} [AddCommGroup T] {S : TopCat.Presheaf CommRingCat X} (N : PresheafOfModules (CategoryTheory.Functor.comp S (CategoryTheory.forget₂ CommRingCat RingCat))) [Module (↑(S.stalk x)) T] (f : (U : TopologicalSpace.Opens ↑X) → x ∈ U → ↑(N.obj (Opposite.op U)) →+ T) (hf : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V) (hx : x ∈ U) (m : ↑(N.obj (Opposite.op V))), (f U hx) ((CategoryTheory.ConcreteCategory.hom (N.map i.op)) m) = (f V ⋯) m) (hs : ∀ (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (r : ↑(S.obj (Opposite.op U))) (m : ↑(N.obj (Opposite.op U))), (f U hx) (r • m) = (CategoryTheory.ConcreteCategory.hom (S.germ U x hx)) r • (f U hx) m) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (m : ↑(N.obj (Opposite.op U))) : (stalkLiftCommRing x N f ⋯ hs) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N.presheaf U x hx)) m) = (f U hx) m

The commutative-ring linear stalk lift takes a germ to its prescribed value.

noncomputable def PresheafOfModules.germSemilinear {X : TopCat} (x : ↑X) {S : TopCat.Presheaf CommRingCat X} (N : PresheafOfModules (CategoryTheory.Functor.comp S (CategoryTheory.forget₂ CommRingCat RingCat))) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) : ↑(N.obj (Opposite.op U)) →ₛₗ[CommRingCat.Hom.hom (S.germ U x hx)] ↑(TopCat.Presheaf.stalk N.presheaf x)

The germ map of a presheaf of modules over a presheaf of commutative rings, as a map semilinear along the ring germ map.

Equations

• PresheafOfModules.germSemilinear x N U hx = { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N.presheaf U x hx)), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem PresheafOfModules.germSemilinear_apply {X : TopCat} (x : ↑X) {S : TopCat.Presheaf CommRingCat X} (N : PresheafOfModules (CategoryTheory.Functor.comp S (CategoryTheory.forget₂ CommRingCat RingCat))) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (m : ↑(N.obj (Opposite.op U))) : (germSemilinear x N U hx) m = (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N.presheaf U x hx)) m

The semilinear germ map is the germ map.

noncomputable def PresheafOfModules.stalkMapCommRing {X : TopCat} (x : ↑X) {S : TopCat.Presheaf CommRingCat X} {N N' : PresheafOfModules (CategoryTheory.Functor.comp S (CategoryTheory.forget₂ CommRingCat RingCat))} (f : N ⟶ N') : ↑(TopCat.Presheaf.stalk N.presheaf x) →ₗ[↑(S.stalk x)] ↑(TopCat.Presheaf.stalk N'.presheaf x)

A morphism of presheaves of modules over a presheaf of commutative rings induces a map on stalks, linear over the commutative-ring stalk.

Equations

• PresheafOfModules.stalkMapCommRing x f = PresheafOfModules.stalkLiftCommRing x N (PresheafOfModules.stalkMapCommRingSection✝ x f) ⋯ ⋯

@[simp]

theorem PresheafOfModules.stalkMapCommRing_germ {X : TopCat} (x : ↑X) {S : TopCat.Presheaf CommRingCat X} {N N' : PresheafOfModules (CategoryTheory.Functor.comp S (CategoryTheory.forget₂ CommRingCat RingCat))} (f : N ⟶ N') (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (m : ↑(N.obj (Opposite.op U))) : (stalkMapCommRing x f) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N.presheaf U x hx)) m) = (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N'.presheaf U x hx)) ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op U))) m)

The stalk map of a morphism sends a germ to the germ of its image.

noncomputable def PresheafOfModules.stalkMapOver {X : TopCat} {R : TopCat.Presheaf RingCat X} (M : PresheafOfModules R) (x : ↑X) {N : PresheafOfModules R} (U : TopologicalSpace.Opens ↑X) (φ : (pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (pushforward₀ (CategoryTheory.Over.forget U) R).obj N) (hxU : x ∈ U) : ↑(TopCat.Presheaf.stalk M.presheaf x) →ₗ[↑(R.stalk x)] ↑(TopCat.Presheaf.stalk N.presheaf x)

A morphism defined on the slice over a neighborhood induces a map on stalks at every point of that neighborhood.

Equations

• M.stalkMapOver x U φ hxU = M.stalkLift x (PresheafOfModules.stalkMapOverSection✝ M x U φ hxU) ⋯ ⋯

theorem PresheafOfModules.stalkMapOver_germ {X : TopCat} {R : TopCat.Presheaf RingCat X} (M : PresheafOfModules R) (x : ↑X) {N : PresheafOfModules R} (U : TopologicalSpace.Opens ↑X) (φ : (pushforward₀ (CategoryTheory.Over.forget U) R).obj M ⟶ (pushforward₀ (CategoryTheory.Over.forget U) R).obj N) (hxU : x ∈ U) (V : TopologicalSpace.Opens ↑X) (i : V ⟶ U) (hxV : x ∈ V) (m : ↑(M.obj (Opposite.op V))) : (M.stalkMapOver x U φ hxU) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.presheaf V x hxV)) m) = (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N.presheaf V x hxV)) ((CategoryTheory.ConcreteCategory.hom (φ.app (Opposite.op (CategoryTheory.Over.mk i)))) m)

The stalk map of a local morphism is computed on any representative inside its domain.