Documentation

TauCeti.LinearAlgebra.SymmetricAlgebra.Grading

The grading of a symmetric algebra #

Let M be a module over a commutative semiring. The powers of the image of M in its symmetric algebra are not merely a spanning family: they form an internal direct sum. Thus every element of the symmetric algebra has a unique finite decomposition into homogeneous terms.

Consequently a map out of the symmetric algebra can be studied degree by degree: it is determined by its restrictions to the homogeneous pieces, so two such maps agreeing on all of them agree, and if it carries each piece into a corresponding summand of an internal decomposition of its target, then it is injective as soon as all of those restrictions are.

Directness comes from the universal property: the external direct sum of the homogeneous pieces is again a commutative algebra, so sending a generator to its degree-one copy produces an algebra map splitting the recomposition map. No freeness of M is needed. This argument follows Mathlib's TensorAlgebra.gradedAlgebra, in Mathlib/LinearAlgebra/TensorAlgebra/Grading.lean, which grades the tensor algebra the same way.

Main results #

source
noncomputable def TauCeti.SymmetricAlgebra.GradedAlgebra.ι (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] :
M →ₗ[R] DirectSum ℕ fun (n : ℕ) => ↥(homogeneousSubmodule R M n)

A version of SymmetricAlgebra.ι that maps directly into the graded structure. This is primarily an auxiliary construction used to provide gradedAlgebra.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem TauCeti.SymmetricAlgebra.GradedAlgebra.ι_apply (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] (m : M) :
    (ι R M) m = (DirectSum.of (fun (n : ℕ) => ↥(homogeneousSubmodule R M n)) 1) ⟨(SymmetricAlgebra.ι R M) m, ⋯⟩

    The defining formula for GradedAlgebra.ι.

    source
    @[instance_reducible]
    noncomputable instance TauCeti.SymmetricAlgebra.gradedAlgebra (R : Type u) (M : Type v) [CommSemiring R] [AddCommMonoid M] [Module R M] :
    GradedAlgebra (homogeneousSubmodule R M)

    A symmetric algebra is graded by its homogeneous pieces, without a freeness assumption on M. This supplies both the canonical decomposition and the multiplicative graded-algebra API.

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