The symmetric powers as functors on the category of modules

Given M : ModuleCat R over a commutative ring R and n : ℕ, this file defines M.symmetricPower n : ModuleCat R as the degree-n homogeneous submodule TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n of the symmetric algebra of M, and extends it to a functor ModuleCat.symmetricPower.functor R n. The zeroth and first symmetric powers are identified with R and with M, naturally.

The degree-n piece of the symmetric algebra is used rather than the symmetric tensor power Sym[R]^n M: Mathlib's SymmetricPower R ι M requires the index type ι to live in the universe of R, so Sym[R]^n M = Sym[R] (Fin n) M is only available for rings in Type, while the homogeneous pieces exist in every universe and assemble into the graded symmetric algebra.

This is the analogue of Mathlib's ModuleCat.exteriorPower, and it is the sectionwise input for the symmetric powers of presheaves and sheaves of modules.

@[reducible, inline]

abbrev ModuleCat.symmetricPower {R : Type u} [CommRing R] (M : ModuleCat R) (n : ℕ) : ModuleCat R

The n-th symmetric power of an object of ModuleCat R: the degree-n homogeneous submodule of its symmetric algebra.

theorem ModuleCat.symmetricPower.hom_ext {R : Type u} [CommRing R] {M : ModuleCat R} {N : ModuleCat R} {n : ℕ} {f g : M.symmetricPower n ⟶ N} (h : ∀ (l : List ↑M), l.length = n → ∀ (hl : (List.map (⇑(SymmetricAlgebra.ι R ↑M)) l).prod ∈ TauCeti.SymmetricAlgebra.homogeneousSubmodule R (↑M) n), (CategoryTheory.ConcreteCategory.hom f) ⟨(List.map (⇑(SymmetricAlgebra.ι R ↑M)) l).prod, hl⟩ = (CategoryTheory.ConcreteCategory.hom g) ⟨(List.map (⇑(SymmetricAlgebra.ι R ↑M)) l).prod, hl⟩) : f = g

Two morphisms out of M.symmetricPower n agree when they agree on every product of n generators.

noncomputable def ModuleCat.symmetricPower.map {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) (n : ℕ) : M.symmetricPower n ⟶ N.symmetricPower n

The morphism on n-th symmetric powers induced by a morphism of modules: the restriction of the induced map of symmetric algebras.

@[simp]

theorem ModuleCat.symmetricPower.coe_map_apply {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) (n : ℕ) (x : ↑(M.symmetricPower n)) : ↑((CategoryTheory.ConcreteCategory.hom (map f n)) x) = (SymmetricAlgebra.map R (Hom.hom f)) ↑x

The morphism induced on symmetric powers is the induced map of symmetric algebras.

theorem ModuleCat.symmetricPower.coe_map_apply_eq_mapₛₗ {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) (n : ℕ) (x : ↑(M.symmetricPower n)) : ↑((CategoryTheory.ConcreteCategory.hom (map f n)) x) = (SymmetricAlgebra.mapₛₗ (Hom.hom f)) ↑x

The morphism induced on symmetric powers is the ring homomorphism of symmetric algebras induced by the underlying linear map, regarded as a semilinear map.

noncomputable def ModuleCat.symmetricPower.functor (R : Type u) [CommRing R] (n : ℕ) : CategoryTheory.Functor (ModuleCat R) (ModuleCat R)

The functor ModuleCat R ⥤ ModuleCat R which sends a module to its n-th symmetric power.

@[simp]

theorem ModuleCat.symmetricPower.functor_obj {R : Type u} [CommRing R] (n : ℕ) (M : ModuleCat R) : (functor R n).obj M = M.symmetricPower n

@[simp]

theorem ModuleCat.symmetricPower.functor_map {R : Type u} [CommRing R] (n : ℕ) {M N : ModuleCat R} (f : M ⟶ N) : (functor R n).map f = map f n

noncomputable def ModuleCat.symmetricPower.iso₀ {R : Type u} [CommRing R] (M : ModuleCat R) : M.symmetricPower 0 ≅ ↧R

The isomorphism M.symmetricPower 0 ≅ ModuleCat.of R R.

@[simp]

theorem ModuleCat.symmetricPower.coe_iso₀_inv_apply {R : Type u} [CommRing R] (M : ModuleCat R) (r : R) : ↑((CategoryTheory.ConcreteCategory.hom (iso₀ M).inv) r) = (algebraMap R (SymmetricAlgebra R ↑M)) r

The inverse of iso₀ sends a scalar to its image in the symmetric algebra.

@[simp]

theorem ModuleCat.symmetricPower.algebraMap_iso₀_hom_apply {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(M.symmetricPower 0)) : (algebraMap R (SymmetricAlgebra R ↑M)) ((CategoryTheory.ConcreteCategory.hom (iso₀ M).hom) x) = ↑x

A degree-zero element is the image of the scalar iso₀ assigns to it.

@[simp]

theorem ModuleCat.symmetricPower.iso₀_hom_naturality {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (map f 0) (iso₀ N).hom = (iso₀ M).hom

@[simp]

theorem ModuleCat.symmetricPower.iso₀_hom_naturality_assoc {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) {Z : ModuleCat R} (h : ↧R ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f 0) (CategoryTheory.CategoryStruct.comp (iso₀ N).hom h) = CategoryTheory.CategoryStruct.comp (iso₀ M).hom h

noncomputable def ModuleCat.symmetricPower.iso₁ {R : Type u} [CommRing R] (M : ModuleCat R) : M.symmetricPower 1 ≅ M

The isomorphism M.symmetricPower 1 ≅ M.

@[simp]

theorem ModuleCat.symmetricPower.coe_iso₁_inv_apply {R : Type u} [CommRing R] (M : ModuleCat R) (m : ↑M) : ↑((CategoryTheory.ConcreteCategory.hom (iso₁ M).inv) m) = (SymmetricAlgebra.ι R ↑M) m

The inverse of iso₁ sends an element of the module to its generator in the symmetric algebra.

@[simp]

theorem ModuleCat.symmetricPower.ι_iso₁_hom_apply {R : Type u} [CommRing R] (M : ModuleCat R) (x : ↑(M.symmetricPower 1)) : (SymmetricAlgebra.ι R ↑M) ((CategoryTheory.ConcreteCategory.hom (iso₁ M).hom) x) = ↑x

A degree-one element is the generator of the element iso₁ assigns to it.

@[simp]

theorem ModuleCat.symmetricPower.iso₁_hom_naturality {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) : CategoryTheory.CategoryStruct.comp (map f 1) (iso₁ N).hom = CategoryTheory.CategoryStruct.comp (iso₁ M).hom f

@[simp]

theorem ModuleCat.symmetricPower.iso₁_hom_naturality_assoc {R : Type u} [CommRing R] {M N : ModuleCat R} (f : M ⟶ N) {Z : ModuleCat R} (h : N ⟶ Z) : CategoryTheory.CategoryStruct.comp (map f 1) (CategoryTheory.CategoryStruct.comp (iso₁ N).hom h) = CategoryTheory.CategoryStruct.comp (iso₁ M).hom (CategoryTheory.CategoryStruct.comp f h)