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 TauCeti.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

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

def TauCeti.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

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

theorem TauCeti.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 TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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

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

@[simp]

theorem TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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 TauCeti.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.