Associated-graded algebra of a word filtration

This file packages the homogeneous pieces of the word filtration generated by a linear map f : M →ₗ[R] A into a direct-sum associated-graded algebra. The Clifford degree filtration uses this construction. The PBW filtration of a universal enveloping algebra is also a word filtration, so this construction applies at UniversalEnvelopingAlgebra.ι R.

The construction is independent of the relations in A: multiplication on a homogeneous piece is induced by multiplication in A, and changing either representative by an element of strictly lower degree changes the product by an element of strictly lower total degree.

Its graded-algebra packaging adapts the pattern in Mathlib's TensorPower construction.

Main definitions

• TauCeti.Algebra.wordFiltration.GradedPiece f k: the degree-k successive quotient.
• TauCeti.Algebra.wordFiltration.AssociatedGraded f: the direct sum ⨁ k, GradedPiece f k of the homogeneous pieces.
• TauCeti.Algebra.wordFiltration.gradedMul: the product of two homogeneous pieces, induced by multiplication in A through wordFiltration_mul.
• TauCeti.Algebra.wordFiltration.gradedOne and TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀: the degree-zero unit and the degree-zero image of a scalar.

Main results

• The graded structure instances assembling those pieces: TauCeti.Algebra.wordFiltration.gradedGOne, gradedGMul, gradedGMonoid, gradedGRing, gradedGSemiring and gradedGAlgebra, culminating in TauCeti.Algebra.wordFiltration.associatedGradedRing, the ring structure on the direct sum.
• TauCeti.Algebra.wordFiltration.gradedPiece_mk_eq_zero_iff: a class in a graded piece vanishes exactly when its representative lies in the preceding filtration step.
• TauCeti.Algebra.wordFiltration.gradedPiece_mk_prod_map_eq_zero_of_length_lt: a word of length strictly below k has zero class in degree k.
• TauCeti.Algebra.wordFiltration.gradedPiece_induction_on: the classes of words of length exactly k span the degree-k graded piece.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter V, §17.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2.7.
• C. Chevalley, The Algebraic Theory of Spinors (1954), Chapter II.
• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I.

Implementation notes

gradedGSemiring and associatedGradedRing are stated explicitly rather than left to instance search. DirectSum.GRing is declared over [∀ i, AddCommGroup (A i)], so DirectSum.GRing.toGSemiring supplies the pointwise AddCommMonoid through AddCommGroup.toAddCommMonoid, which does not match the one instance search finds directly for GradedPiece; without these two declarations neither DirectSum.GSemiring (GradedPiece f) nor Ring (AssociatedGraded f) is synthesizable.

@[reducible, inline]

abbrev TauCeti.Algebra.wordFiltration.GradedPiece {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (k : ℕ) : Type w

The degree-k quotient of a word filtration by its preceding step.

Equations

• TauCeti.Algebra.wordFiltration.GradedPiece f k = (↥(TauCeti.Algebra.wordFiltration f k) ⧸ TauCeti.Algebra.wordFiltration.previousRestricted f k)

theorem TauCeti.Algebra.wordFiltration.gradedPiece_mk_eq_zero_iff {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {k : ℕ} (x : ↥(wordFiltration f k)) : Submodule.Quotient.mk x = 0 ↔ ↑x ∈ wordFiltrationPrevious f k

The class of a filtered element in the graded piece of its degree vanishes exactly when the element already lies in the preceding filtration step.

@[reducible, inline]

abbrev TauCeti.Algebra.wordFiltration.AssociatedGraded {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) : Type w

The direct sum of the homogeneous pieces of the word filtration generated by f.

Equations

• TauCeti.Algebra.wordFiltration.AssociatedGraded f = DirectSum ℕ fun (k : ℕ) => TauCeti.Algebra.wordFiltration.GradedPiece f k

noncomputable def TauCeti.Algebra.wordFiltration.gradedMul {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (i j : ℕ) : GradedPiece f i →ₗ[R] GradedPiece f j →ₗ[R] GradedPiece f (i + j)

Multiplication of two homogeneous pieces of the associated graded algebra of the word filtration.

Equations

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

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedMul_apply_mk {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (i j : ℕ) (x : ↥(wordFiltration f i)) (y : ↥(wordFiltration f j)) : ((gradedMul f i j) (Submodule.Quotient.mk x)) (Submodule.Quotient.mk y) = Submodule.Quotient.mk ⟨↑x * ↑y, ⋯⟩

On quotient representatives, the homogeneous product is induced by multiplication in A.

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedPiece_cast_mk {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {i j : ℕ} (h : i = j) (x : ↥(wordFiltration f i)) : cast ⋯ (Submodule.Quotient.mk x) = Submodule.Quotient.mk (cast ⋯ x)

Casting a quotient class between equal degrees casts its filtration representative.

theorem TauCeti.Algebra.wordFiltration.gradedMul_assoc {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (i j k : ℕ) (x : GradedPiece f i) (y : GradedPiece f j) (z : GradedPiece f k) : cast ⋯ (((gradedMul f (i + j) k) (((gradedMul f i j) x) y)) z) = ((gradedMul f i (j + k)) x) (((gradedMul f j k) y) z)

Homogeneous word-filtration multiplication is associative after reindexing degrees.

noncomputable def TauCeti.Algebra.wordFiltration.gradedOne {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) : GradedPiece f 0

The degree-zero unit of the homogeneous word-filtration pieces.

Equations

• TauCeti.Algebra.wordFiltration.gradedOne f = Submodule.Quotient.mk ⟨1, ⋯⟩

theorem TauCeti.Algebra.wordFiltration.gradedOne_def {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) : gradedOne f = Submodule.Quotient.mk ⟨1, ⋯⟩

The degree-zero unit is the quotient class of (1 : A).

@[simp]

theorem TauCeti.Algebra.wordFiltration.mk_one_eq_gradedOne {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) : Submodule.Quotient.mk ⟨1, ⋯⟩ = gradedOne f

The quotient class of (1 : A) is the degree-zero homogeneous unit.

noncomputable def TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀ {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) : R →+ GradedPiece f 0

The degree-zero class of a scalar in the associated graded of the word filtration.

Equations

• TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀ f = { toFun := fun (r : R) => Submodule.Quotient.mk ⟨(algebraMap R A) r, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

theorem TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀_apply {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (r : R) : (gradedAlgebraMap₀ f) r = Submodule.Quotient.mk ⟨(algebraMap R A) r, ⋯⟩

The degree-zero scalar map is the quotient class of its ambient scalar.

@[simp]

theorem TauCeti.Algebra.wordFiltration.mk_algebraMap_eq_gradedAlgebraMap₀ {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (r : R) : Submodule.Quotient.mk ⟨(algebraMap R A) r, ⋯⟩ = (gradedAlgebraMap₀ f) r

The quotient class of an ambient scalar is its degree-zero homogeneous class.

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀_one {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) : (gradedAlgebraMap₀ f) 1 = gradedOne f

The degree-zero scalar map sends 1 to the homogeneous unit.

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedOne_mul {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (k : ℕ) (x : GradedPiece f k) : ((gradedMul f 0 k) (gradedOne f)) x = cast ⋯ x

The degree-zero homogeneous unit acts on the left.

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedMul_one {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (k : ℕ) (x : GradedPiece f k) : ((gradedMul f k 0) x) (gradedOne f) = cast ⋯ x

The degree-zero homogeneous unit acts on the right.

@[instance_reducible]

noncomputable instance TauCeti.Algebra.wordFiltration.gradedGOne {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : GradedMonoid.GOne (GradedPiece f)

The homogeneous degree-zero class supplies the GOne structure on filtration pieces.

Equations

• TauCeti.Algebra.wordFiltration.gradedGOne = { one := TauCeti.Algebra.wordFiltration.gradedOne f }

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedGOne_one {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : GradedMonoid.GOne.one = gradedOne f

The graded unit field is the named degree-zero unit.

@[instance_reducible]

noncomputable instance TauCeti.Algebra.wordFiltration.gradedGMul {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : GradedMonoid.GMul (GradedPiece f)

Homogeneous filtration multiplication supplies the GMul structure on filtration pieces.

Equations

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

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedGMul_mul {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} {i j : ℕ} (x : GradedPiece f i) (y : GradedPiece f j) : GradedMonoid.GMul.mul x y = ((gradedMul f i j) x) y

The graded multiplication field is the named homogeneous multiplication.

@[instance_reducible]

noncomputable instance TauCeti.Algebra.wordFiltration.gradedGMonoid {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : GradedMonoid.GMonoid (GradedPiece f)

The homogeneous unit and multiplication form a graded monoid of filtration pieces.

Equations

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

@[instance_reducible]

noncomputable instance TauCeti.Algebra.wordFiltration.gradedGRing {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : DirectSum.GRing (GradedPiece f)

Bilinearity and scalar casts make the homogeneous pieces a direct-sum graded ring.

Equations

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

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀_mul {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (r : R) (k : ℕ) (x : GradedPiece f k) : cast ⋯ (((gradedMul f 0 k) ((gradedAlgebraMap₀ f) r)) x) = r • x

Left multiplication by a degree-zero scalar class is scalar multiplication.

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀_mul_algebraMap₀ {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (r s : R) : ((gradedMul f 0 0) ((gradedAlgebraMap₀ f) r)) ((gradedAlgebraMap₀ f) s) = (gradedAlgebraMap₀ f) (r * s)

Degree-zero scalar classes multiply by multiplying their scalars.

theorem TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀_commutes {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (r : R) (k : ℕ) (x : GradedPiece f k) : cast ⋯ (((gradedMul f 0 k) ((gradedAlgebraMap₀ f) r)) x) = ((gradedMul f k 0) x) ((gradedAlgebraMap₀ f) r)

Degree-zero scalar classes commute with homogeneous products after reindexing degrees.

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedMul_algebraMap₀ {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) (r : R) (k : ℕ) (x : GradedPiece f k) : ((gradedMul f k 0) x) ((gradedAlgebraMap₀ f) r) = r • x

Right multiplication by a degree-zero scalar class is scalar multiplication.

@[instance_reducible]

noncomputable instance TauCeti.Algebra.wordFiltration.gradedGSemiring {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : DirectSum.GSemiring (GradedPiece f)

The graded-ring structure supplies the semiring structure needed by the direct sum.

Equations

• TauCeti.Algebra.wordFiltration.gradedGSemiring = TauCeti.Algebra.wordFiltration.gradedGRing.toGSemiring

@[instance_reducible]

noncomputable instance TauCeti.Algebra.wordFiltration.gradedGAlgebra {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : DirectSum.GAlgebra R (GradedPiece f)

Degree-zero scalar classes make the homogeneous pieces into a graded R-algebra.

Equations

• TauCeti.Algebra.wordFiltration.gradedGAlgebra = { toFun := TauCeti.Algebra.wordFiltration.gradedAlgebraMap₀ f, map_one := ⋯, map_mul := ⋯, commutes := ⋯, smul_def := ⋯ }

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedGAlgebra_toFun {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} (r : R) : DirectSum.GAlgebra.toFun r = (gradedAlgebraMap₀ f) r

The graded scalar-map field is the named degree-zero scalar map.

@[instance_reducible]

noncomputable instance TauCeti.Algebra.wordFiltration.associatedGradedRing {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : Ring (AssociatedGraded f)

The direct sum of homogeneous filtration pieces inherits its associated-graded ring structure.

Equations

• TauCeti.Algebra.wordFiltration.associatedGradedRing = inferInstance

@[simp]

theorem TauCeti.Algebra.wordFiltration.associatedGraded_of_gradedOne {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} : (DirectSum.of (GradedPiece f) 0) (gradedOne f) = 1

The degree-zero homogeneous unit generates the unit of the associated graded.

@[simp]

theorem TauCeti.Algebra.wordFiltration.associatedGraded_of_gradedAlgebraMap₀ {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} (r : R) : (DirectSum.of (GradedPiece f) 0) ((gradedAlgebraMap₀ f) r) = (algebraMap R (AssociatedGraded f)) r

The degree-zero homogeneous scalar class generates its scalar in the associated graded.

@[simp]

theorem TauCeti.Algebra.wordFiltration.associatedGraded_of_mul_of {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] {f : M →ₗ[R] A} {i j : ℕ} (x : GradedPiece f i) (y : GradedPiece f j) : (DirectSum.of (GradedPiece f) i) x * (DirectSum.of (GradedPiece f) j) y = (DirectSum.of (GradedPiece f) (i + j)) (((gradedMul f i j) x) y)

The product of two homogeneous generators in the associated graded is their named homogeneous product.

@[simp]

theorem TauCeti.Algebra.wordFiltration.gradedPiece_mk_prod_map_eq_zero_of_length_lt {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {k : ℕ} {l : List M} (hl : l.length < k) : Submodule.Quotient.mk ⟨(List.map (⇑f) l).prod, ⋯⟩ = 0

A word of length strictly below k has zero class in the degree-k graded piece.

theorem TauCeti.Algebra.wordFiltration.gradedPiece_induction_on_of_span {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {ι : Type u_1} (e : ι → M) (he : Submodule.span R (Set.range e) = ⊤) {k : ℕ} {motive : GradedPiece f k → Prop} (x : GradedPiece f k) (word : ∀ (l : List ι) (hl : l.length = k), motive (Submodule.Quotient.mk ⟨(List.map (fun (i : ι) => f (e i)) l).prod, ⋯⟩)) (zero : motive 0) (add : ∀ (x y : GradedPiece f k), motive x → motive y → motive (x + y)) (smul : ∀ (r : R) (x : GradedPiece f k), motive x → motive (r • x)) : motive x

Words in a spanning family span the graded pieces. To prove a statement about every element of the degree-k graded piece of a word filtration it suffices to treat the classes of length-k words in a spanning family, and to check that the statement is closed under zero, addition and scalar multiplication. Shorter words are covered by the zero case, since their classes vanish in degree k.

theorem TauCeti.Algebra.wordFiltration.gradedPiece_induction_on {R : Type u} {M : Type v} {A : Type w} [CommRing R] [AddCommMonoid M] [Module R M] [Ring A] [Algebra R A] (f : M →ₗ[R] A) {k : ℕ} {motive : GradedPiece f k → Prop} (x : GradedPiece f k) (word : ∀ (l : List M) (hl : l.length = k), motive (Submodule.Quotient.mk ⟨(List.map (⇑f) l).prod, ⋯⟩)) (zero : motive 0) (add : ∀ (x y : GradedPiece f k), motive x → motive y → motive (x + y)) (smul : ∀ (r : R) (x : GradedPiece f k), motive x → motive (r • x)) : motive x

To prove a statement about every element of a graded piece, it suffices to treat all words of the exact degree and check closure under the module operations.