The word filtration generated by a linear map

Let A be an associative algebra and let f : M →ₗ[R] A be a linear family of elements of A. This file defines Ado.Algebra.wordFiltration f k, the submodule spanned by products of at most k elements in the range of f. This is the canonical increasing filtration on any algebra generated by a linear family.

The construction is factored out of the Clifford and universal-enveloping-algebra filtrations. In both cases the defining relations can lower word length, so the quotient is filtered rather than graded by length. The generic construction records the properties independent of those relations: monotonicity, multiplicativity, the first two steps, comparison with powers of the range of f, and exhaustivity onto the subalgebra generated by f.

Main definitions and results

• Ado.Algebra.wordFiltration: powers of the scalar-and-generator submodule.
• Ado.Algebra.wordFiltration.previousRestricted: the preceding step inside the current step.
• Ado.Algebra.wordFiltration_eq_pow: its defining equation as that power.
• Ado.Algebra.wordFiltration_mul: multiplication adds filtration degrees.
• Ado.Algebra.span_prod_map_eq_wordFiltration: words in a spanning family span each filtration step.
• Ado.Algebra.span_prod_map_eq_range_pow: words of length exactly n span the n-th power of the generator range.
• Ado.Algebra.map_wordFiltration_le: algebra maps sending generators into degree one preserve every filtration step.
• Ado.Algebra.map_wordFiltration_eq: an algebra map carrying the scalar-and-generator submodule exactly onto another does the same in every filtration degree.
• Ado.Algebra.map_wordFiltration_eq_of_surjective: a compatible algebra map carries every filtration step onto the corresponding target step when the map between generators is surjective.
• Ado.Algebra.wordFiltration_eq_iSup_pow: comparison with powers of LinearMap.range f.
• Ado.Algebra.iSup_wordFiltration_eq_adjoin: the filtration exhausts precisely the subalgebra generated by f.
• Ado.Algebra.exists_mem_wordFiltration_of_iSup_eq_top and Ado.Algebra.exists_mem_notMem_wordFiltrationPrevious: elementwise consequences of exhaustivity, the second producing the leading degree of a nonzero element.
• Ado.Algebra.wordFiltration.instGradedMonoid and Ado.Algebra.wordFiltration.instIsRingFiltration: the bundled multiplicativity and filtration instances.

def Ado.Algebra.wordFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) : Submodule R A

The degree filtration generated by a linear map f : M →ₗ[R] A.

The k-th step is the k-th submodule power of the scalars together with the range of f. It is equivalently the R-span of products of at most k elements in the range of f, including the empty product; see wordFiltration_le_iff.

Equations

• Ado.Algebra.wordFiltration f k = (1 ⊔ f.range) ^ k

theorem Ado.Algebra.wordFiltration_eq_pow {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) : wordFiltration f k = (1 ⊔ f.range) ^ k

The defining equation of the word filtration: degree k is the k-th submodule power of the scalars together with the range of f.

def Ado.Algebra.wordFiltrationPrevious {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : ℕ → Submodule R A

The step preceding degree k, with bottom in degree zero.

Equations

• Ado.Algebra.wordFiltrationPrevious f 0 = ⊥
• Ado.Algebra.wordFiltrationPrevious f k.succ = Ado.Algebra.wordFiltration f k

@[simp]

theorem Ado.Algebra.wordFiltrationPrevious_zero {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : wordFiltrationPrevious f 0 = ⊥

The preceding word filtration is trivial in degree zero.

@[simp]

theorem Ado.Algebra.wordFiltrationPrevious_succ {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) : wordFiltrationPrevious f (k + 1) = wordFiltration f k

In successor degree, the preceding word filtration is the previous filtration step.

theorem Ado.Algebra.prod_map_mem_range_pow {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (l : List M) : (List.map (⇑f) l).prod ∈ f.range ^ l.length

A word of length n lies in the n-th power of the range of the generators.

theorem Ado.Algebra.span_prod_map_eq_range_pow_of_span {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {ι : Type u_1} (e : ι → M) (he : Submodule.span R (Set.range e) = ⊤) (n : ℕ) : Submodule.span R {a : A | ∃ (l : List ι), l.length = n ∧ (List.map (fun (i : ι) => f (e i)) l).prod = a} = f.range ^ n

Words of length exactly n in a spanning family span the n-th power of the generator range.

theorem Ado.Algebra.span_prod_map_eq_range_pow {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (n : ℕ) : Submodule.span R {a : A | ∃ (l : List M), l.length = n ∧ (List.map (⇑f) l).prod = a} = f.range ^ n

Words of length exactly n span the n-th power of the generator range.

theorem Ado.Algebra.prod_map_mem_wordFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {k : ℕ} {l : List M} (hl : l.length ≤ k) : (List.map (⇑f) l).prod ∈ wordFiltration f k

A word of length at most k belongs to the k-th word-filtration step.

theorem Ado.Algebra.wordFiltration_le_iff {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {k : ℕ} {p : Submodule R A} : wordFiltration f k ≤ p ↔ ∀ (l : List M), l.length ≤ k → (List.map (⇑f) l).prod ∈ p

A submodule contains the k-th filtration step exactly when it contains every word of length at most k.

theorem Ado.Algebra.span_prod_map_eq_wordFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {ι : Type u_1} (e : ι → M) (he : Submodule.span R (Set.range e) = ⊤) (k : ℕ) : Submodule.span R {a : A | ∃ (word : List ι), word.length ≤ k ∧ (List.map (fun (i : ι) => f (e i)) word).prod = a} = wordFiltration f k

Products of at most k images of a spanning family span the k-th word-filtration step.

theorem Ado.Algebra.map_wordFiltration_le {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {N : Type u_1} {B : Type u_2} [Semiring B] [Algebra R B] [AddCommMonoid N] [Module R N] (g : A →ₐ[R] B) (f' : N →ₗ[R] B) (h : ∀ (m : M), g (f m) ∈ wordFiltration f' 1) (k : ℕ) : Submodule.map g.toLinearMap (wordFiltration f k) ≤ wordFiltration f' k

An algebra homomorphism that sends each source generator into target filtration degree one preserves word-filtration degree.

theorem Ado.Algebra.map_mem_wordFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {N : Type u_1} {B : Type u_2} [Semiring B] [Algebra R B] [AddCommMonoid N] [Module R N] (g : A →ₐ[R] B) (f' : N →ₗ[R] B) (h : ∀ (m : M), g (f m) ∈ wordFiltration f' 1) {k : ℕ} {x : A} (hx : x ∈ wordFiltration f k) : g x ∈ wordFiltration f' k

The membership form of map_wordFiltration_le: an algebra homomorphism that sends source generators into target filtration degree one preserves every filtration step.

theorem Ado.Algebra.map_wordFiltration_eq {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {N : Type u_1} {B : Type u_2} [Semiring B] [Algebra R B] [AddCommMonoid N] [Module R N] (g : A →ₐ[R] B) (f' : N →ₗ[R] B) (h : Submodule.map g.toLinearMap (1 ⊔ f.range) = 1 ⊔ f'.range) (k : ℕ) : Submodule.map g.toLinearMap (wordFiltration f k) = wordFiltration f' k

An algebra homomorphism that maps one scalar-and-generator submodule exactly onto another maps every corresponding word-filtration step exactly onto the other.

theorem Ado.Algebra.map_wordFiltration_eq_of_surjective {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {N : Type u_1} {B : Type u_2} [Semiring B] [Algebra R B] [AddCommMonoid N] [Module R N] (q : M →ₗ[R] N) (hq : Function.Surjective ⇑q) (g : A →ₐ[R] B) (f' : N →ₗ[R] B) (h : g.toLinearMap ∘ₗ f = f' ∘ₗ q) (k : ℕ) : Submodule.map g.toLinearMap (wordFiltration f k) = wordFiltration f' k

A compatible algebra homomorphism maps every word-filtration step onto the corresponding target step when its map on the generating modules is surjective.

theorem Ado.Algebra.wordFiltration_mono {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : Monotone (wordFiltration f)

The word filtration is increasing.

@[simp]

theorem Ado.Algebra.wordFiltration_zero {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : wordFiltration f 0 = 1

The zeroth word-filtration step consists of the scalars.

theorem Ado.Algebra.one_mem_wordFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) : 1 ∈ wordFiltration f k

The empty word puts 1 in every filtration step.

theorem Ado.Algebra.algebraMap_mem_wordFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (r : R) (k : ℕ) : (algebraMap R A) r ∈ wordFiltration f k

Every scalar belongs to every filtration step.

theorem Ado.Algebra.apply_mem_wordFiltration_one {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (m : M) : f m ∈ wordFiltration f 1

Each generator belongs to the first filtration step.

theorem Ado.Algebra.range_le_wordFiltration_one {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : f.range ≤ wordFiltration f 1

The range of the generating linear map lies in the first filtration step.

theorem Ado.Algebra.wordFiltration_mul {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (i j : ℕ) : wordFiltration f i * wordFiltration f j = wordFiltration f (i + j)

Multiplication adds word-filtration degrees. In fact the product of the two filtration steps equals the step in the sum degree.

theorem Ado.Algebra.mul_mem_wordFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {i j : ℕ} {x y : A} (hx : x ∈ wordFiltration f i) (hy : y ∈ wordFiltration f j) : x * y ∈ wordFiltration f (i + j)

The elementwise multiplicativity of the word filtration.

theorem Ado.Algebra.mul_mem_wordFiltrationPrevious_left {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {i j : ℕ} {x y : A} (hx : x ∈ wordFiltrationPrevious f i) (hy : y ∈ wordFiltration f j) : x * y ∈ wordFiltrationPrevious f (i + j)

Multiplying an element of degree strictly below i by an element of degree at most j produces an element of degree strictly below i + j.

theorem Ado.Algebra.mul_mem_wordFiltrationPrevious_right {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {i j : ℕ} {x y : A} (hx : x ∈ wordFiltration f i) (hy : y ∈ wordFiltrationPrevious f j) : x * y ∈ wordFiltrationPrevious f (i + j)

Multiplying an element of degree at most i by an element of degree strictly below j produces an element of degree strictly below i + j.

theorem Ado.Algebra.range_pow_le_wordFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (n : ℕ) : f.range ^ n ≤ wordFiltration f n

The n-th power of the generator range lies in filtration degree n.

theorem Ado.Algebra.wordFiltration_eq_iSup_pow {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) : wordFiltration f k = ⨆ (i : { i : ℕ // i ≤ k }), f.range ^ ↑i

The k-th word-filtration step is the supremum of the powers of the generator range of degree at most k.

theorem Ado.Algebra.wordFiltration_succ_eq_sup {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) : wordFiltration f (k + 1) = wordFiltration f k ⊔ f.range ^ (k + 1)

The successor filtration step adjoins words of exactly the new degree.

@[simp]

theorem Ado.Algebra.wordFiltration_one {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : wordFiltration f 1 = 1 ⊔ f.range

The first filtration step consists of the scalars and the generator range.

theorem Ado.Algebra.wordFiltration_pow {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (i n : ℕ) : wordFiltration f i ^ n = wordFiltration f (i * n)

Powers of a filtration step multiply its degree.

theorem Ado.Algebra.iSup_wordFiltration_eq_adjoin {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : ⨆ (k : ℕ), wordFiltration f k = Subalgebra.toSubmodule (Algebra.adjoin R (Set.range ⇑f))

The word filtration exhausts exactly the subalgebra generated by the range of f.

theorem Ado.Algebra.exists_mem_wordFiltration_of_iSup_eq_top {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (h : ⨆ (k : ℕ), wordFiltration f k = ⊤) (a : A) : ∃ (k : ℕ), a ∈ wordFiltration f k

An exhaustive word filtration covers the algebra elementwise: if the filtration steps supremum to ⊤, every element lies in one of them.

theorem Ado.Algebra.exists_mem_notMem_wordFiltrationPrevious {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {a : A} (ha : a ≠ 0) (hex : ∃ (k : ℕ), a ∈ wordFiltration f k) : ∃ (k : ℕ), a ∈ wordFiltration f k ∧ a ∉ wordFiltrationPrevious f k

A nonzero element of an exhaustive word filtration has a leading degree: a degree it belongs to but whose preceding step it misses.

@[reducible, inline]

abbrev Ado.Algebra.wordFiltration.previousRestricted {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) : Submodule R ↥(wordFiltration f k)

The preceding word-filtration step, viewed as a submodule of the current step.

Equations

• Ado.Algebra.wordFiltration.previousRestricted f k = (Ado.Algebra.wordFiltrationPrevious f k).submoduleOf (Ado.Algebra.wordFiltration f k)

@[simp]

theorem Ado.Algebra.wordFiltration.mem_previousRestricted_iff {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) (x : ↥(wordFiltration f k)) : x ∈ previousRestricted f k ↔ ↑x ∈ wordFiltrationPrevious f k

Membership in the restricted preceding step is ambient membership in the preceding step.

@[simp]

theorem Ado.Algebra.wordFiltration.previousRestricted_zero {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : previousRestricted f 0 = ⊥

The restricted preceding word filtration is trivial in degree zero.

@[simp]

theorem Ado.Algebra.wordFiltration.previousRestricted_succ {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) (k : ℕ) : previousRestricted f (k + 1) = Submodule.comap (wordFiltration f (k + 1)).subtype (wordFiltration f k)

In successor degree, the restricted preceding word filtration is the previous step viewed inside the current step.

@[simp]

theorem Ado.Algebra.wordFiltration.wordFiltration_coe_cast {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) {i j : ℕ} (h : i = j) (x : ↥(wordFiltration f i)) : ↑(cast ⋯ x) = ↑x

Casting a filtered element between equal degrees does not change its value in the ambient algebra.

instance Ado.Algebra.wordFiltration.instGradedMonoid {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : SetLike.GradedMonoid (wordFiltration f)

Word filtrations are multiplicative families of submodules.

instance Ado.Algebra.wordFiltration.instIsRingFiltration {R : Type u} {M : Type v} {A : Type w} [CommSemiring R] [Semiring A] [Algebra R A] [AddCommMonoid M] [Module R M] (f : M →ₗ[R] A) : IsRingFiltration (wordFiltration f) (wordFiltrationPrevious f)

The word filtration, with the preceding step at each degree, is a ring filtration.