Tensor products and stalks of sheaves of modules

This file constructs, over an arbitrary topological space and for arbitrary sheaves of modules M, N, the canonical linear map from the stalk of their tensor product to the tensor product of their stalks over the ring stalk, and computes its values on germs of sheafified pure tensors. The comparison is a linear equivalence, with no finiteness or quasi-coherence hypotheses.

It is the sectionwise comparison PresheafOfModules.tensorStalkComparison, precomposed with the inverse of the identification PresheafOfModules.sheafificationStalkEquiv of a stalk with the stalk of the sheafification, and with the stalk map (PresheafOfModules.stalkMapCommRing) of the defining isomorphism tensorProductIso.

Main declarations

• SheafOfModules.tensorStalkComparison: the comparison as a linear map over the ring stalk;
• SheafOfModules.tensorStalkEquiv: the same comparison as a linear equivalence;
• SheafOfModules.tensorStalkEquiv_naturality: compatibility with morphisms in both factors;
• SheafOfModules.tensorStalkEquiv_symm_tmul_germ: its inverse on tensors of germs;
• SheafOfModules.tensorStalkComparison_apply: its description as the composite above;
• SheafOfModules.tensorStalkComparison_germ_unit_tmul: its value on the germ of a sheafified pure tensor.

noncomputable def TauCeti.SheafOfModules.tensorStalkComparison {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) (x : ↑X) : ↑(TopCat.Presheaf.stalk (tensorProduct R M N).val.presheaf x) →ₗ[↑(TopCat.Presheaf.stalk R.obj x)] TensorProduct ↑(TopCat.Presheaf.stalk R.obj x) ↑(TopCat.Presheaf.stalk M.val.presheaf x) ↑(TopCat.Presheaf.stalk N.val.presheaf x)

The canonical linear map from the stalk of the tensor product of two sheaves of modules to the tensor product of their stalks.

Equations

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

theorem TauCeti.SheafOfModules.tensorStalkComparison_apply {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) (x : ↑X) (s : ↑(TopCat.Presheaf.stalk (tensorProduct R M N).val.presheaf x)) : (tensorStalkComparison R M N x) s = (M.val.tensorStalkComparison N.val x) ((PresheafOfModules.sheafificationStalkEquiv R (PresheafOfModulesOfCommRing.Monoidal.tensorObj M.val N.val) x).symm ((PresheafOfModules.stalkMapCommRing x (tensorProductIso R M N).hom.val) s))

The tensor stalk comparison is the sectionwise comparison, applied after transporting along tensorProductIso and identifying the stalk of the sheafification with the original stalk.

@[simp]

theorem TauCeti.SheafOfModules.tensorStalkComparison_germ_unit_tmul {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) (x : ↑X) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (m : ↑(M.val.obj (Opposite.op U))) (n : ↑(N.val.obj (Opposite.op U))) : (tensorStalkComparison R M N x) ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ (tensorProduct R M N).val.presheaf U x hx)) ((CategoryTheory.ConcreteCategory.hom ((tensorProductIso R M N).inv.val.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj M.val N.val)).app (Opposite.op U))) (m ⊗ₜ[↑(R.obj.obj (Opposite.op U))] n)))) = (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.val.presheaf U x hx)) m ⊗ₜ[↑(TopCat.Presheaf.stalk R.obj x)] (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N.val.presheaf U x hx)) n

The tensor stalk comparison sends the germ of the pure tensor m ⊗ₜ n, pushed through the sheafification unit and transported along tensorProductIso, to the tensor product of the germs of m and n.

theorem TauCeti.SheafOfModules.tensorStalkComparison_bijective {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) (x : ↑X) : Function.Bijective ⇑(tensorStalkComparison R M N x)

The canonical tensor stalk comparison is bijective for arbitrary sheaves of modules.

noncomputable def TauCeti.SheafOfModules.tensorStalkEquiv {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) (x : ↑X) : ↑(TopCat.Presheaf.stalk (tensorProduct R M N).val.presheaf x) ≃ₗ[↑(TopCat.Presheaf.stalk R.obj x)] TensorProduct ↑(TopCat.Presheaf.stalk R.obj x) ↑(TopCat.Presheaf.stalk M.val.presheaf x) ↑(TopCat.Presheaf.stalk N.val.presheaf x)

The stalk of the sheaf tensor product is canonically the tensor product of the stalks over the ring stalk. Its forward map is the existing tensor stalk comparison.

Equations

• TauCeti.SheafOfModules.tensorStalkEquiv R M N x = LinearEquiv.ofBijective (TauCeti.SheafOfModules.tensorStalkComparison R M N x) ⋯

@[simp]

theorem TauCeti.SheafOfModules.tensorStalkEquiv_apply {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) (x : ↑X) (t : ↑(TopCat.Presheaf.stalk (tensorProduct R M N).val.presheaf x)) : (tensorStalkEquiv R M N x) t = (tensorStalkComparison R M N x) t

The tensor stalk equivalence is the canonical comparison.

@[simp]

theorem TauCeti.SheafOfModules.tensorStalkEquiv_symm_tmul_germ {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) (x : ↑X) (U : TopologicalSpace.Opens ↑X) (hx : x ∈ U) (m : ↑(M.val.obj (Opposite.op U))) (n : ↑(N.val.obj (Opposite.op U))) : (tensorStalkEquiv R M N x).symm ((CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ M.val.presheaf U x hx)) m ⊗ₜ[↑(TopCat.Presheaf.stalk R.obj x)] (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ N.val.presheaf U x hx)) n) = (CategoryTheory.ConcreteCategory.hom (TopCat.Presheaf.germ (tensorProduct R M N).val.presheaf U x hx)) ((CategoryTheory.ConcreteCategory.hom ((tensorProductIso R M N).inv.val.app (Opposite.op U))) ((CategoryTheory.ConcreteCategory.hom (((PresheafOfModules.sheafificationAdjunction (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).unit.app (CategoryTheory.MonoidalCategoryStruct.tensorObj M.val N.val)).app (Opposite.op U))) (m ⊗ₜ[↑(R.obj.obj (Opposite.op U))] n)))

The inverse sends a tensor of germs to the germ of the sheafified tensor of their representatives on a common neighborhood.

theorem TauCeti.SheafOfModules.tensorStalkEquiv_naturality {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) CommRingCat) (M N : SheafOfModules (ringCatSheaf R)) (x : ↑X) {M' N' : SheafOfModules (ringCatSheaf R)} (f : M ⟶ M') (g : N ⟶ N') : (↑(tensorStalkEquiv R M' N' x) ∘ₗ have this := PresheafOfModules.stalkMapCommRing x (CategoryTheory.CategoryStruct.comp (tensorProductIso R M N).hom (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (ringCatSheaf R).obj)).map (CategoryTheory.MonoidalCategoryStruct.tensorHom f.val g.val)) (tensorProductIso R M' N').inv)).val; this) = TensorProduct.map (have this := PresheafOfModules.stalkMapCommRing x f.val; this) (have this := PresheafOfModules.stalkMapCommRing x g.val; this) ∘ₗ ↑(tensorStalkEquiv R M N x)

The tensor stalk equivalence commutes with morphisms in both factors. The map on the sheaf tensor product is the sheafification of the sectionwise tensor map, read through tensorProductIso.