Homogeneous submodules of a symmetric algebra

For a module M over a commutative semiring R, this file defines the degree-n piece of SymmetricAlgebra R M to be the n-th power of the range of the canonical generator map, identifies it with the span of the products of exactly n generators, and records that degrees add under multiplication and that scaling linear evaluation scales degree-n values by the n-th power. The pieces span the whole symmetric algebra, but no internal direct-sum decomposition is proven here. A derivation of the symmetric algebra that sends every generator to degree one preserves every homogeneous submodule.

Main definitions and results

• TauCeti.SymmetricAlgebra.homogeneousSubmodule: the degree-n homogeneous submodule.
• TauCeti.SymmetricAlgebra.homogeneousSubmodule_eq_span: it is spanned by the products of exactly n generators.
• TauCeti.SymmetricAlgebra.iSup_homogeneousSubmodule_eq_top: the homogeneous pieces span the whole symmetric algebra.
• TauCeti.SymmetricAlgebra.instGradedMonoid: the homogeneous submodules form a graded monoid.
• TauCeti.SymmetricAlgebra.homogeneousSubmoduleZeroEquiv, TauCeti.SymmetricAlgebra.homogeneousSubmoduleOneEquiv: the homogeneous pieces of degree zero and one are the scalars and the module itself.
• TauCeti.SymmetricAlgebra.derivation_mem_homogeneousSubmodule: a derivation sending generators to degree one preserves every homogeneous submodule.

This is the homogeneous-piece prerequisite for the degreewise PBW comparison map in Layer 3, “PBW, a substantial sub-project”, of the highest-weight roadmap.

@[reducible, inline]

abbrev TauCeti.SymmetricAlgebra.homogeneousSubmodule (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : Submodule R (SymmetricAlgebra R M)

The degree-n homogeneous part of SymmetricAlgebra R M: the n-th power of the range of the canonical generator map.

Equations

• TauCeti.SymmetricAlgebra.homogeneousSubmodule R M n = (SymmetricAlgebra.ι R M).range ^ n

theorem TauCeti.SymmetricAlgebra.ι_mem_homogeneousSubmodule (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : M) : (SymmetricAlgebra.ι R M) x ∈ homogeneousSubmodule R M 1

A symmetric-algebra generator is homogeneous of degree one.

theorem TauCeti.SymmetricAlgebra.lift_smul_of_mem_homogeneousSubmodule (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] {A : Type u_1} [CommSemiring A] [Algebra R A] (f : M →ₗ[R] A) (r : R) {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ homogeneousSubmodule R M n) : (SymmetricAlgebra.lift (r • f)) p = r ^ n • (SymmetricAlgebra.lift f) p

Scaling a linear evaluation by r scales the value of a homogeneous polynomial of degree n by rⁿ.

theorem TauCeti.SymmetricAlgebra.prod_map_ι_mem_homogeneousSubmodule (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (l : List M) : (List.map (⇑(SymmetricAlgebra.ι R M)) l).prod ∈ homogeneousSubmodule R M l.length

A product of n symmetric-algebra generators is homogeneous of degree n.

theorem TauCeti.SymmetricAlgebra.homogeneousSubmodule_eq_span_of_span (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_1} (e : ι → M) (he : Submodule.span R (Set.range e) = ⊤) (n : ℕ) : homogeneousSubmodule R M n = Submodule.span R {p : SymmetricAlgebra R M | ∃ (l : List ι), l.length = n ∧ (List.map (fun (i : ι) => (SymmetricAlgebra.ι R M) (e i)) l).prod = p}

Products of exactly n elements from a spanning family span the degree-n homogeneous submodule.

theorem TauCeti.SymmetricAlgebra.homogeneousSubmodule_eq_span (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (n : ℕ) : homogeneousSubmodule R M n = Submodule.span R {p : SymmetricAlgebra R M | ∃ (l : List M), l.length = n ∧ (List.map (⇑(SymmetricAlgebra.ι R M)) l).prod = p}

The degree-n homogeneous submodule is spanned by the products of exactly n generators.

theorem TauCeti.SymmetricAlgebra.iSup_homogeneousSubmodule_eq_top (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : ⨆ (n : ℕ), homogeneousSubmodule R M n = ⊤

The homogeneous submodules span the whole symmetric algebra. This is the spanning half of an internal grading; directness is not asserted here.

noncomputable def TauCeti.SymmetricAlgebra.homogeneousSubmoduleZeroEquiv (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : ↥(homogeneousSubmodule R M 0) ≃ₗ[R] R

The degree-zero homogeneous submodule of a symmetric algebra is the image of the scalars, which embed injectively.

Equations

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

@[simp]

theorem TauCeti.SymmetricAlgebra.coe_homogeneousSubmoduleZeroEquiv_symm_apply (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (r : R) : ↑((homogeneousSubmoduleZeroEquiv R M).symm r) = (algebraMap R (SymmetricAlgebra R M)) r

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

@[simp]

theorem TauCeti.SymmetricAlgebra.algebraMap_homogeneousSubmoduleZeroEquiv_apply (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : ↥(homogeneousSubmodule R M 0)) : (algebraMap R (SymmetricAlgebra R M)) ((homogeneousSubmoduleZeroEquiv R M) x) = ↑x

A degree-zero element of a symmetric algebra is the image of the scalar homogeneousSubmoduleZeroEquiv assigns to it.

noncomputable def TauCeti.SymmetricAlgebra.homogeneousSubmoduleOneEquiv (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : ↥(homogeneousSubmodule R M 1) ≃ₗ[R] M

The degree-one homogeneous submodule of a symmetric algebra is the image of the module, which embeds injectively.

Equations

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

@[simp]

theorem TauCeti.SymmetricAlgebra.coe_homogeneousSubmoduleOneEquiv_symm_apply (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) : ↑((homogeneousSubmoduleOneEquiv R M).symm m) = (SymmetricAlgebra.ι R M) m

The inverse of homogeneousSubmoduleOneEquiv sends an element of the module to its generator.

@[simp]

theorem TauCeti.SymmetricAlgebra.ι_homogeneousSubmoduleOneEquiv_apply (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (x : ↥(homogeneousSubmodule R M 1)) : (SymmetricAlgebra.ι R M) ((homogeneousSubmoduleOneEquiv R M) x) = ↑x

A degree-one element of a symmetric algebra is the generator of the element of the module homogeneousSubmoduleOneEquiv assigns to it.

instance TauCeti.SymmetricAlgebra.instGradedMonoid (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] : SetLike.GradedMonoid (homogeneousSubmodule R M)

The homogeneous submodules form a graded monoid: the unit is homogeneous of degree zero, and multiplication adds degrees.

theorem TauCeti.SymmetricAlgebra.derivation_mem_homogeneousSubmodule (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (D : Derivation R (SymmetricAlgebra R M) (SymmetricAlgebra R M)) (hD : ∀ (x : M), D ((SymmetricAlgebra.ι R M) x) ∈ homogeneousSubmodule R M 1) {n : ℕ} {p : SymmetricAlgebra R M} (hp : p ∈ homogeneousSubmodule R M n) : D p ∈ homogeneousSubmodule R M n

A derivation of the symmetric algebra sending every generator into degree one preserves every homogeneous submodule.