The sheaf associated with a tensor product of modules

For a commutative ring R, the functor M ↦ M~ from R-modules to 𝒪_{Spec R}-modules is strong monoidal: (M ⊗_R N)~ ≅ M~ ⊗ N~ naturally in M and N, and R~ = 𝒪_{Spec R}.

The comparison maps come from adjunction. Taking global sections is lax monoidal: it is taking sections over ⊤ of the underlying presheaf of modules, whose tensor product is computed sectionwise, followed by restriction of scalars along R ≅ Γ(Spec R, ⊤). Its left adjoint M ↦ M~ is therefore oplax monoidal. Its unit comparison is the identification of R~ with 𝒪_{Spec R}. For a fixed M, the tensor comparison (M ⊗_R N)~ ⟶ M~ ⊗ N~ is a natural transformation between functors of N which preserve colimits, since M ↦ M~ and both tensor products are left adjoints. By unitality it is invertible at N = R, hence everywhere (TauCeti.ModuleCat.isIso_of_isIso_app_self).

Main declarations

• TauCeti.AlgebraicGeometry.tildeMonoidal: the functor M ↦ M~ is monoidal;
• TauCeti.AlgebraicGeometry.tilde_ε and TauCeti.AlgebraicGeometry.tilde_η: its unit comparisons are the identification AlgebraicGeometry.tildeSelf of R~ with 𝒪_{Spec R};
• TauCeti.AlgebraicGeometry.tilde_μ_app_top_toOpen: on global sections, the tensor comparison sends the product of the sections m and n to the section m ⊗ₜ n.

References

• R. Hartshorne, Algebraic Geometry, Proposition II.5.2 (b)

@[instance_reducible]

noncomputable instance TauCeti.AlgebraicGeometry.tildeMonoidal {R : CommRingCat} : (AlgebraicGeometry.tilde.functor R).Monoidal

The functor M ↦ M~ from R-modules to 𝒪_{Spec R}-modules is monoidal: (M ⊗_R N)~ ≅ M~ ⊗ N~ and R~ = 𝒪_{Spec R}. Its inverse comparison maps are the mates, under the tilde--global sections adjunction, of the lax monoidal structure of global sections.

Equations

• TauCeti.AlgebraicGeometry.tildeMonoidal = CategoryTheory.Functor.Monoidal.ofOplaxMonoidal (AlgebraicGeometry.tilde.functor R)

@[simp]

theorem TauCeti.AlgebraicGeometry.tilde_η {R : CommRingCat} : CategoryTheory.Functor.OplaxMonoidal.η (AlgebraicGeometry.tilde.functor R) = AlgebraicGeometry.tildeSelf.hom

The inverse unit comparison R~ ⟶ 𝒪_{Spec R} of M ↦ M~ is the identification AlgebraicGeometry.tildeSelf of R~ with 𝒪_{Spec R}.

@[simp]

theorem TauCeti.AlgebraicGeometry.tilde_ε {R : CommRingCat} : CategoryTheory.Functor.LaxMonoidal.ε (AlgebraicGeometry.tilde.functor R) = AlgebraicGeometry.tildeSelf.inv

The unit comparison 𝒪_{Spec R} ⟶ R~ of M ↦ M~ is the identification AlgebraicGeometry.tildeSelf of R~ with 𝒪_{Spec R}.

theorem TauCeti.AlgebraicGeometry.tilde_μ_app_top_toOpen {R : CommRingCat} (M N : ModuleCat ↑R) (m : ↑M) (n : ↑N) : (CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' ((SheafOfModules.forget (AlgebraicGeometry.Spec R).ringCatSheaf).map (CategoryTheory.Functor.LaxMonoidal.μ (AlgebraicGeometry.tilde.functor R) M N)) (Opposite.op ⊤))) ((CategoryTheory.ConcreteCategory.hom (PresheafOfModules.Hom.app' (CategoryTheory.Functor.LaxMonoidal.μ (SheafOfModules.forget (AlgebraicGeometry.Spec R).ringCatSheaf) (AlgebraicGeometry.tilde M) (AlgebraicGeometry.tilde N)) (Opposite.op ⊤))) ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen M ⊤)) m ⊗ₜ[↑((AlgebraicGeometry.Spec R).presheaf.obj (Opposite.op ⊤))] (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen N ⊤)) n)) = (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.tilde.toOpen (CategoryTheory.MonoidalCategoryStruct.tensorObj M N) ⊤)) (m ⊗ₜ[↑R] n)

On global sections, the tensor comparison M~ ⊗ N~ ⟶ (M ⊗_R N)~ of M ↦ M~ sends the product of the sections m and n to the section m ⊗ₜ n. Here the product of two sections is their image under the tensor map of the inclusion of sheaves of modules into presheaves of modules, whose tensor product is computed sectionwise.