Documentation

Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

The monoidal category structure on presheaves of modules #

Given a presheaf of commutative rings R : Cᵒᵖ ⥤ CommRingCat, we construct the monoidal category structure on the category of presheaves of modules PresheafOfModules (R ⋙ forget₂ _ _). The tensor product M₁ ⊗ M₂ is defined as the presheaf of modules which sends X : Cᵒᵖ to M₁.obj X ⊗ M₂.obj X.

Notes #

This contribution was created as part of the AIM workshop "Formalizing algebraic geometry" in June 2024.

The tensor product of two presheaves of modules.

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

The tensor product of two morphisms of presheaves of modules.

Equations