Stalks and tensor products of presheaves of modules #
Let R be a presheaf of commutative rings on a topological space X, and let M and P be
presheaves of R-modules. This file proves
stalkTensorEquiv : Mₓ ⊗[Rₓ] Pₓ ≃ₗ[Rₓ] (M ⊗ P)ₓ,
the statement that taking stalks commutes with the tensor product of presheaves of modules.
Main definitions #
PresheafOfModules.stalkTensorBackward—Mₓ ⊗[Rₓ] Pₓ → (M ⊗ P)ₓ, built from the biadditivePresheafOfModules.germTmulBiaddbyTensorProduct.lift;PresheafOfModules.stalkTensorForward—(M ⊗ P)ₓ → Mₓ ⊗[Rₓ] Pₓ, the colimit map of the cocone whose legs sendm ⊗ ptogerm m ⊗ germ p;PresheafOfModules.stalkTensorEquiv— the two assembled into anRₓ-linear equivalence;PresheafOfModules.stalkMap— the stalk map of a morphism of presheaves of modules, as anRₓ-linear map.
Main results #
PresheafOfModules.stalkTensorEquiv_naturality— naturality of the tensor-stalk equivalence in both module-presheaf inputs;PresheafOfModules.isIso_stalkMapAdd_whiskerLeft— whiskering preserves stalkwise isomorphisms, for an arbitrary whiskering factor. Tensoring is only right exact, but tensoring with an isomorphism is an isomorphism, andPresheafOfModules.stalkTensorEquivis what makes that visible on stalks.
Every declaration in this module intrinsically uses the topology of X through open
neighbourhoods, germs, or stalk functors. It is therefore the topological comparison root used
by DerivedAlgGeo.Topology.Sheaves.ModuleTensor, not ordinary ModuleCat algebra.
Implementation notes #
The backward map starts with tensors of stalk elements, whose representatives may lie over
different neighbourhoods. It restricts both representatives to their intersection and descends
through two colimits, first via PresheafOfModules.germTmulRight and then via
PresheafOfModules.germTmulBiadd. The identity PresheafOfModules.germ_smul expresses
compatibility with scalars along the ring germ map; choosing a common neighbourhood for a scalar
and both sections then establishes bilinearity over the stalk ring.
References #
The comparison extends Mathlib's module-presheaf stalk and monoidal APIs.
Tags #
module presheaf, stalk, tensor product, naturality
Mₓ ⊗ Pₓ, the target of the comparison.
Equations
- M.StalkTensor P x = TensorProduct ↑(R.stalk x) ↑(TopCat.Presheaf.stalk M.presheaf x) ↑(TopCat.Presheaf.stalk P.presheaf x)
Instances For
Mₓ ⊗ Pₓ viewed over R(U) for a neighbourhood U of x, via the germ map.
Equations
- M.stalkTensorModuleAt P x U hx = Module.compHom (M.StalkTensor P x) (CommRingCat.Hom.hom (R.germ U x hx))
Instances For
The R(U)-bilinear map (m, p) ↦ germ m ⊗ germ p.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Restriction of a section, stated at the plain module type rather than through
ModuleCat.restrictScalars. Reducible, so that rw still sees through it.
Equations
Instances For
For a section m of M over U and a section p of P over V, the germ at x of
m ⊗ p restricted to U ⊓ V. This is the value the backward map must take on germs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Shrinking the neighbourhood of m does not change the germ of m ⊗ p.
Shrinking the neighbourhood of p does not change the germ of m ⊗ p.
PresheafOfModules.germTmul depends only on the two germs, not on the sections representing
them.
Over a single neighbourhood, PresheafOfModules.germTmul is just the germ of the pure tensor.
The scalar action on the stalk, over a single neighbourhood: this is the Rₓ-linearity
of the backward map, before the three neighbourhoods are separated.
Rₓ-linearity of PresheafOfModules.germTmul in the M slot, with the scalar, the section of
M and the
section of P over three different neighbourhoods.
PresheafOfModules.germTmul is additive in the M slot, over a fixed pair of neighbourhoods.
PresheafOfModules.germTmul is additive in the P slot, over a fixed pair of neighbourhoods.
For a fixed section m of M over U, the germs m ⊗ p form a cocone on the P-diagram:
the legs are additive by PresheafOfModules.germTmul_add_right and natural by
PresheafOfModules.germTmul_res_right.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Tensoring a fixed section m of M against the stalk of P.
Equations
- M.germTmulRight P x U hxU m = CategoryTheory.Limits.colimit.desc ((TopologicalSpace.OpenNhds.inclusion x).op.comp P.presheaf) (M.germTmulCoconeRight P x U hxU m)
Instances For
The defining computation rule for PresheafOfModules.germTmulRight, which is a
CategoryTheory.Limits.colimit.desc and so is
pinned down entirely by its values on germs. Every later proof about it goes through here.
PresheafOfModules.germTmulRight is unchanged by shrinking the neighbourhood of m: the
naturality the outer
cocone needs, now at the level of the induced morphism rather than of germs.
PresheafOfModules.germTmulRight is additive in m, pointwise on the stalk of P.
The outer cocone, in the M variable: legs additive by PresheafOfModules.germTmulRight_add,
natural by
PresheafOfModules.germTmulRight_res_left. Its point is the additive maps out of the stalk of P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The biadditive map Mₓ → Pₓ → (M ⊗ P)ₓ underlying the backward comparison.
Equations
- M.germTmulBiadd P x = CategoryTheory.Limits.colimit.desc ((TopologicalSpace.OpenNhds.inclusion x).op.comp M.presheaf) (M.germTmulCoconeLeft P x)
Instances For
Both colimit stages unwound at once. Since every element of a stalk is a germ, this and
additivity determine PresheafOfModules.germTmulBiadd completely — it is the only handle the
bilinearity and
inverse proofs use.
Right-slot analogue of PresheafOfModules.germ_smul_germTmul_self: over a single neighbourhood
the scalar
may be moved into the P factor. Unlike the M slot this is not definitional — it is
TensorProduct.tmul_smul, and so uses commutativity of R(U).
PresheafOfModules.germTmulBiadd is Rₓ-linear in the M slot.
PresheafOfModules.germTmulBiadd is Rₓ-linear in the P slot.
PresheafOfModules.germTmulBiadd is additive in the M slot, at the level of stalks.
The Rₓ-bilinear map Mₓ → Pₓ → (M ⊗ P)ₓ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The backward comparison Mₓ ⊗[Rₓ] Pₓ → (M ⊗ P)ₓ.
Equations
- M.stalkTensorBackward P x = TensorProduct.lift (M.germTmulBilin P x)
Instances For
The backward map computes on a pure tensor of stalk elements.
The backward map sends a pure tensor of germs to the germ of the pure tensor, taken over the intersection of the two neighbourhoods.
The leg of the forward cocone at a neighbourhood U of x: the map
(M ⊗ P)(U) → Mₓ ⊗ Pₓ sending m ⊗ p to germ m ⊗ germ p.
Equations
- M.stalkTensorLeg P x U hx = AddCommGrpCat.ofHom (TensorProduct.lift (M.stalkTensorBilin P x U hx)).toAddMonoidHom
Instances For
The forward leg computes on a pure tensor of sections.
The forward legs are compatible with restriction: this is the naturality the cocone needs.
The cocone on the (M ⊗ P)-diagram whose legs are PresheafOfModules.stalkTensorLeg.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward comparison (M ⊗ P)ₓ → Mₓ ⊗[Rₓ] Pₓ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The forward map computes on a germ, by the leg at that neighbourhood.
The forward map computes on the germs of pure tensors: this is the exact converse of
PresheafOfModules.stalkTensorBackward_germ_tmul_germ.
The forward map is a retraction of the backward map.
The backward map is a retraction of the forward map.
The stalk of a tensor product of presheaves of modules is the tensor product of the
stalks, over the stalk of the ring: (M ⊗ P)ₓ ≅ Mₓ ⊗[Rₓ] Pₓ.
Equations
- M.stalkTensorEquiv P x = { toLinearMap := M.stalkTensorBackward P x, invFun := ⇑(CategoryTheory.ConcreteCategory.hom (M.stalkTensorForward P x)), left_inv := ⋯, right_inv := ⋯ }
Instances For
PresheafOfModules.stalkTensorEquiv computes on a pure tensor of germs.
The inverse of PresheafOfModules.stalkTensorEquiv computes on a germ.
The stalk map of a morphism of presheaves of modules, as a morphism of abelian groups.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stalk map is computed by applying the morphism to a representing section: this is
TopCat.Presheaf.stalkFunctor_map_germ_apply, restated at the spelling
PresheafOfModules uses so that rw can see it.
The stalk map of a morphism of presheaves of modules is Rₓ-linear.
Equations
- PresheafOfModules.stalkMap g x = { toFun := ⇑(CategoryTheory.ConcreteCategory.hom (PresheafOfModules.stalkMapAdd g x)), map_add' := ⋯, map_smul' := ⋯ }
Instances For
PresheafOfModules.stalkMap has the same computation rule as PresheafOfModules.stalkMapAdd;
the two differ only in carrying
the Rₓ-module structure.
The tensor-stalk equivalence is natural in both module-presheaf inputs. The proof computes on pure tensors of germs and then uses additivity.
Whiskering acts on a pure tensor of sections in the obvious way.
PresheafOfModules.stalkTensorEquiv is natural in the second variable. Under the
identification of
(M ⊗ P)ₓ with Mₓ ⊗ Pₓ, the stalk map of M ◁ g is Mₓ ⊗ (stalk map of g). This is what
turns a stalkwise iso into a stalkwise iso after whiskering.
Whiskering preserves stalkwise isomorphisms. If g is a stalk isomorphism at x, so is
M ◁ g — for any M, with no flatness or local-freeness hypothesis. Tensoring is only right
exact in general, but tensoring with an isomorphism is an isomorphism, and
PresheafOfModules.stalkTensorEquiv
is what makes that visible on stalks.