Multiplication of symmetric powers of sheaves of modules

Let R be a sheaf of commutative rings on a small site. For a sheaf of R-modules M, the symmetric powers Symⁿ M are the graded pieces of the symmetric algebra Sym M = ⨁ₙ Symⁿ M. This file constructs its multiplication SheafOfModules.symmetricPowerMul M i j : Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M in the symmetric monoidal category of sheaves of R-modules: it is the sheafification of the sectionwise multiplication PresheafOfModulesOfCommRing.symmetricPowerMul, composed with the tensor comparison of the monoidal functor sheafification.

Together with the unit R ≅ Sym⁰ M of SheafOfModules.symmetricPowerZeroIso, the multiplication is natural in M and satisfies the graded unit, associativity and commutativity laws. These are the homogeneous laws taken by CategoryTheory.GradedObject.monObjOfHomogeneous and CategoryTheory.GradedObject.isCommMonObj_monObjOfHomogeneous, which assemble such data into a commutative algebra object in graded objects; on a scheme this is the input for the graded symmetric algebra of an 𝒪_X-module, whose relative spectrum is the associated linear scheme. The laws are transported from the sectionwise ones along sheafification, which is a braided monoidal functor.

Main declarations

• SheafOfModules.symmetricPowerMul: the multiplication Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M, with defining equation SheafOfModules.symmetricPowerMul_def;
• SheafOfModules.symmetricPowerMul_naturality: naturality in M;
• SheafOfModules.epi_symmetricPowerMul: the multiplication is an epimorphism; in particular so is Symⁿ M ⊗ Sym¹ M ⟶ Symⁿ⁺¹ M, which is the sense in which the symmetric algebra is generated in degree one;
• SheafOfModules.symmetricPowerMul_assoc, symmetricPowerMul_comm, symmetricPowerMul_one_mul and symmetricPowerMul_mul_one: the graded associativity, commutativity and unit laws;
• TauCeti.SheafOfModules.symmetricPowerLift_mul: sheafifying sectionwise maps out of symmetric powers preserves compatibility with multiplications.

noncomputable def SheafOfModules.symmetricPowerMul {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (i j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj ((symmetricPower R i).obj M) ((symmetricPower R j).obj M) ⟶ (symmetricPower R (i + j)).obj M

The multiplication Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M of symmetric powers of a sheaf of modules: the sheafification of the sectionwise multiplication of symmetric powers, preceded by the tensor comparison of sheafification.

theorem SheafOfModules.symmetricPowerMul_def {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (i j : ℕ) : M.symmetricPowerMul i j = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symmetricPowerIso i M).hom (symmetricPowerIso j M).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)) ((PresheafOfModulesOfCommRing.symmetricPower i).obj M.val) ((PresheafOfModulesOfCommRing.symmetricPower j).obj M.val)) (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id (TauCeti.SheafOfModules.ringCatSheaf R).obj)).map (PresheafOfModulesOfCommRing.symmetricPowerMul M.val i j)) (symmetricPowerIso (i + j) M).inv))

The defining equation of the multiplication of symmetric powers of a sheaf of modules, through the identifications symmetricPowerIso of symmetric powers with sheafified sectionwise symmetric powers.

theorem SheafOfModules.symmetricPowerMul_naturality {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (φ : M ⟶ N) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((symmetricPower R i).map φ) ((symmetricPower R j).map φ)) (N.symmetricPowerMul i j) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) ((symmetricPower R (i + j)).map φ)

The multiplication of symmetric powers is natural in the sheaf of modules.

theorem SheafOfModules.symmetricPowerMul_naturality_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M N : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (φ : M ⟶ N) (i j : ℕ) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : (symmetricPower R (i + j)).obj N ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom ((symmetricPower R i).map φ) ((symmetricPower R j).map φ)) (CategoryTheory.CategoryStruct.comp (N.symmetricPowerMul i j) h) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) (CategoryTheory.CategoryStruct.comp ((symmetricPower R (i + j)).map φ) h)

The multiplication of symmetric powers is natural in the sheaf of modules.

instance SheafOfModules.epi_symmetricPowerMul {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (i j : ℕ) : CategoryTheory.Epi (M.symmetricPowerMul i j)

The multiplication of symmetric powers of a sheaf of modules is an epimorphism: it is the sheafification of the sectionwise multiplication, which is an epimorphism, up to isomorphisms.

theorem SheafOfModules.symmetricPowerMul_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (i j k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (M.symmetricPowerMul i j) ((symmetricPower R k).obj M)) (M.symmetricPowerMul (i + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((symmetricPower R i).obj M) ((symmetricPower R j).obj M) ((symmetricPower R k).obj M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((symmetricPower R i).obj M) (M.symmetricPowerMul j k)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i (j + k)) (CategoryTheory.eqToHom ⋯)))

The multiplication of symmetric powers of a sheaf of modules is associative, up to the identification of the degrees i + (j + k) and i + j + k.

theorem SheafOfModules.symmetricPowerMul_assoc_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (i j k : ℕ) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : (symmetricPower R (i + j + k)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (M.symmetricPowerMul i j) ((symmetricPower R k).obj M)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul (i + j) k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator ((symmetricPower R i).obj M) ((symmetricPower R j).obj M) ((symmetricPower R k).obj M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((symmetricPower R i).obj M) (M.symmetricPowerMul j k)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i (j + k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)))

The multiplication of symmetric powers of a sheaf of modules is associative, up to the identification of the degrees i + (j + k) and i + j + k.

theorem SheafOfModules.symmetricPowerMul_comm {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (β_ ((symmetricPower R i).obj M) ((symmetricPower R j).obj M)).hom (M.symmetricPowerMul j i) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) (CategoryTheory.eqToHom ⋯)

The multiplication of symmetric powers of a sheaf of modules is commutative, up to the identification of the degrees i + j and j + i.

theorem SheafOfModules.symmetricPowerMul_comm_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (i j : ℕ) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : (symmetricPower R (j + i)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ ((symmetricPower R i).obj M) ((symmetricPower R j).obj M)).hom (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul j i) h) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The multiplication of symmetric powers of a sheaf of modules is commutative, up to the identification of the degrees i + j and j + i.

theorem SheafOfModules.symmetricPowerMul_one_mul {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((symmetricPowerZeroIso R).inv.app M) ((symmetricPower R n).obj M)) (M.symmetricPowerMul 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((symmetricPower R n).obj M)).hom (CategoryTheory.eqToHom ⋯)

The unit R ≅ Sym⁰ M is a left identity for the multiplication of symmetric powers, up to the identification of the degrees 0 + n and n.

theorem SheafOfModules.symmetricPowerMul_one_mul_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (n : ℕ) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : (symmetricPower R (0 + n)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight ((symmetricPowerZeroIso R).inv.app M) ((symmetricPower R n).obj M)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul 0 n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor ((symmetricPower R n).obj M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The unit R ≅ Sym⁰ M is a left identity for the multiplication of symmetric powers, up to the identification of the degrees 0 + n and n.

theorem SheafOfModules.symmetricPowerMul_mul_one {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((symmetricPower R n).obj M) ((symmetricPowerZeroIso R).inv.app M)) (M.symmetricPowerMul n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((symmetricPower R n).obj M)).hom (CategoryTheory.eqToHom ⋯)

The unit R ≅ Sym⁰ M is a right identity for the multiplication of symmetric powers, up to the identification of the degrees n + 0 and n.

theorem SheafOfModules.symmetricPowerMul_mul_one_assoc {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} (M : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)) (n : ℕ) {Z : SheafOfModules (TauCeti.SheafOfModules.ringCatSheaf R)} (h : (symmetricPower R (n + 0)).obj M ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft ((symmetricPower R n).obj M) ((symmetricPowerZeroIso R).inv.app M)) (CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul n 0) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor ((symmetricPower R n).obj M)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

The unit R ≅ Sym⁰ M is a right identity for the multiplication of symmetric powers, up to the identification of the degrees n + 0 and n.

theorem TauCeti.SheafOfModules.symmetricPowerLift_mul {C : Type u} [CategoryTheory.SmallCategory C] {J : CategoryTheory.GrothendieckTopology C} [J.HasSheafCompose (CategoryTheory.forget₂ CommRingCat RingCat)] [CategoryTheory.HasWeakSheafify J AddCommGrpCat] [J.WEqualsLocallyBijective AddCommGrpCat] {R : CategoryTheory.Sheaf J CommRingCat} {M : SheafOfModules (ringCatSheaf R)} {B : ℕ → SheafOfModules (ringCatSheaf R)} (ψ : (n : ℕ) → (PresheafOfModulesOfCommRing.symmetricPower n).obj M.val ⟶ (B n).val) (mul : (i j : ℕ) → CategoryTheory.MonoidalCategoryStruct.tensorObj (B i) (B j) ⟶ B (i + j)) (h : ∀ (i j : ℕ), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (ψ i) (ψ j)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ (SheafOfModules.forget (ringCatSheaf R)) (B i) (B j)) (mul i j).val) = CategoryTheory.CategoryStruct.comp (PresheafOfModulesOfCommRing.symmetricPowerMul M.val i j) (ψ (i + j))) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (symmetricPowerLift (ψ i)) (symmetricPowerLift (ψ j))) (mul i j) = CategoryTheory.CategoryStruct.comp (M.symmetricPowerMul i j) (symmetricPowerLift (ψ (i + j)))

Sectionwise maps out of symmetric powers compatible with the multiplications lift along sheafification to maps compatible with the multiplications.