Multiplication of symmetric powers in the category of modules

For M : ModuleCat R the product in the symmetric algebra of M sends the symmetric powers Symⁱ M and Symʲ M into Symⁱ⁺ʲ M. This file packages it as a morphism ModuleCat.symmetricPower.mul M i j : Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M of the monoidal category ModuleCat R, natural in M, and proves that together with the unit R ≅ Sym⁰ M it is unital, associative and commutative up to the identifications of degrees. These are the homogeneous laws of a commutative monoid object in graded modules, in the form taken by CategoryTheory.GradedObject.monObjOfHomogeneous; they are the sectionwise input for the graded symmetric algebra of a sheaf of modules.

The bilinear multiplication is Mathlib's DirectSum.gMulLHom for the grading TauCeti.SymmetricAlgebra.gradedAlgebra of the symmetric algebra by its homogeneous pieces, as Mathlib's exteriorPower.wedge does for exterior powers.

Main declarations

• ModuleCat.symmetricPower.mul: the multiplication Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M, computed by ModuleCat.symmetricPower.coe_mul_tmul;
• ModuleCat.symmetricPower.mul_naturality: naturality in M;
• ModuleCat.symmetricPower.mul_surjective: the multiplication is surjective, since Symⁱ⁺ʲ M is spanned by products of elements of Symⁱ M and Symʲ M; hence it is an epimorphism (ModuleCat.symmetricPower.epi_mul);
• ModuleCat.symmetricPower.mul_assoc, mul_comm, one_mul and mul_one: the graded associativity, commutativity and unit laws.

noncomputable def ModuleCat.symmetricPower.mul {R : Type u} [CommRing R] (M : ModuleCat R) (i j : ℕ) : CategoryTheory.MonoidalCategoryStruct.tensorObj (M.symmetricPower i) (M.symmetricPower j) ⟶ M.symmetricPower (i + j)

The multiplication of the symmetric algebra of M, restricted to the symmetric powers Symⁱ M and Symʲ M, as a morphism Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M in ModuleCat R.

@[simp]

theorem ModuleCat.symmetricPower.coe_mul_tmul {R : Type u} [CommRing R] (M : ModuleCat R) {i j : ℕ} (x : ↑(M.symmetricPower i)) (y : ↑(M.symmetricPower j)) : ↑((CategoryTheory.ConcreteCategory.hom (mul M i j)) (x ⊗ₜ[R] y)) = ↑x * ↑y

The multiplication of symmetric powers is the product in the symmetric algebra.

@[simp]

theorem ModuleCat.symmetricPower.coe_eqToHom_apply {R : Type u} [CommRing R] (M : ModuleCat R) {i j : ℕ} (h : i = j) (x : ↑(M.symmetricPower i)) : ↑((CategoryTheory.ConcreteCategory.hom (CategoryTheory.eqToHom ⋯)) x) = ↑x

Transport along an equality of degrees does not change the underlying element of the symmetric algebra.

theorem ModuleCat.symmetricPower.mul_naturality {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map f i) (map f j)) (mul N i j) = CategoryTheory.CategoryStruct.comp (mul M i j) (map f (i + j))

The multiplication of symmetric powers is natural in the module.

theorem ModuleCat.symmetricPower.mul_naturality_assoc {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) (i j : ℕ) {Z : ModuleCat R} (h : N.symmetricPower (i + j) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (map f i) (map f j)) (CategoryTheory.CategoryStruct.comp (mul N i j) h) = CategoryTheory.CategoryStruct.comp (mul M i j) (CategoryTheory.CategoryStruct.comp (map f (i + j)) h)

The multiplication of symmetric powers is natural in the module.

theorem ModuleCat.symmetricPower.mul_surjective {R : Type u} [CommRing R] (M : ModuleCat R) (i j : ℕ) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (mul M i j))

The multiplication Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M is surjective: Symⁱ⁺ʲ M is the product of the submodules Symⁱ M and Symʲ M of the symmetric algebra.

instance ModuleCat.symmetricPower.epi_mul {R : Type u} [CommRing R] (M : ModuleCat R) (i j : ℕ) : CategoryTheory.Epi (mul M i j)

The multiplication Symⁱ M ⊗ Symʲ M ⟶ Symⁱ⁺ʲ M is an epimorphism.

theorem ModuleCat.symmetricPower.mul_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (i j k : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mul M i j) (M.symmetricPower k)) (mul M (i + j) k) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (M.symmetricPower i) (M.symmetricPower j) (M.symmetricPower k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M.symmetricPower i) (mul M j k)) (CategoryTheory.CategoryStruct.comp (mul M i (j + k)) (CategoryTheory.eqToHom ⋯)))

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

theorem ModuleCat.symmetricPower.mul_assoc_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (i j k : ℕ) {Z : ModuleCat R} (h : M.symmetricPower (i + j + k) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (mul M i j) (M.symmetricPower k)) (CategoryTheory.CategoryStruct.comp (mul M (i + j) k) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (M.symmetricPower i) (M.symmetricPower j) (M.symmetricPower k)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M.symmetricPower i) (mul M j k)) (CategoryTheory.CategoryStruct.comp (mul M i (j + k)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)))

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

theorem ModuleCat.symmetricPower.mul_comm {R : Type u} [CommRing R] (M : ModuleCat R) (i j : ℕ) : CategoryTheory.CategoryStruct.comp (β_ (M.symmetricPower i) (M.symmetricPower j)).hom (mul M j i) = CategoryTheory.CategoryStruct.comp (mul M i j) (CategoryTheory.eqToHom ⋯)

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

theorem ModuleCat.symmetricPower.mul_comm_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (i j : ℕ) {Z : ModuleCat R} (h : M.symmetricPower (j + i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ (M.symmetricPower i) (M.symmetricPower j)).hom (CategoryTheory.CategoryStruct.comp (mul M j i) h) = CategoryTheory.CategoryStruct.comp (mul M i j) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h)

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

theorem ModuleCat.symmetricPower.one_mul {R : Type u} [CommRing R] (M : ModuleCat R) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (iso₀ M).inv (M.symmetricPower n)) (mul M 0 n) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M.symmetricPower n)).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 ModuleCat.symmetricPower.one_mul_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (n : ℕ) {Z : ModuleCat R} (h : M.symmetricPower (0 + n) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (iso₀ M).inv (M.symmetricPower n)) (CategoryTheory.CategoryStruct.comp (mul M 0 n) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (M.symmetricPower n)).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 ModuleCat.symmetricPower.mul_one {R : Type u} [CommRing R] (M : ModuleCat R) (n : ℕ) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M.symmetricPower n) (iso₀ M).inv) (mul M n 0) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M.symmetricPower n)).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 ModuleCat.symmetricPower.mul_one_assoc {R : Type u} [CommRing R] (M : ModuleCat R) (n : ℕ) {Z : ModuleCat R} (h : M.symmetricPower (n + 0) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (M.symmetricPower n) (iso₀ M).inv) (CategoryTheory.CategoryStruct.comp (mul M n 0) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (M.symmetricPower n)).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.