Lemma 6.4 for a split semisimple S = Λ₀

lem:split-positive-deformation (positive-deformations.tex): "Let k be any field, let Λ be a finite-dimensional nonnegatively graded algebra with split semisimple S = Λ₀, and let B be a positive filtered deformation of Λ. Then S lifts to a unital subalgebra of B, and the filtration of B splits as S-bimodules. […] each μ_q raises internal degree by q, is S-relative, and vanishes when an input belongs to S."

A split semisimple S ≅ ∏_a M_{n_a}(k) is recorded by a complete system of matrix units spanning Λ₀ (MatUnits: E_{ij} for i, j in one block, the block of i named by a root rt i). The diagonal units lift to orthogonal idempotents f_i (through the nilpotent ideal F¹), the units E_{i,rt i}, E_{rt i,i} lift to x_i, y_i with x_i y_i = f_i after inverting x_i y_i in the corner f_iBf_i (geometric series), and then y_i x_i = f_{rt i} (an idempotent congruent to f_{rt i} modulo F¹); L_{ij} = x_i y_j are lifted matrix units (L_mul, σ_L). The splitting of the corners (φ0, from the diagonal idempotents) is transported from the root corners: Φ(a) = Σ_{i,j} L_{i,rt i} φ0(E_{rt i,i} a E_{j,rt j}) L_{rt j,j}, which is S-bilinear (Φ_left, Φ_right), unital and has leading term the identity (Φ_lead). The statement is splitPositiveDeformation_ss.

structure MultiplicativeBasisDeformations.LenGrading.MatUnits {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) : Type u_2

A split semisimple degree-zero part Λ₀ ≅ ∏_a M_{n_a}(k): a complete system of matrix units of degree 0 spanning Λ₀. Indices in one block have the same root rt i; E_{ij} is defined for i, j in one block and zero otherwise.

• n : ℕ
• rt : Fin self.n → Fin self.n
• rt_rt (i : Fin self.n) : self.rt (self.rt i) = self.rt i
• E : Fin self.n → Fin self.n → Λ
• E_mul (i j l m : Fin self.n) : self.rt i = self.rt j → self.rt l = self.rt m → self.E i j * self.E l m = if j = l then self.E i m else 0
• E_off (i j : Fin self.n) : self.rt i ≠ self.rt j → self.E i j = 0
• sum_E : ∑ i : Fin self.n, self.E i i = 1
• deg0 (i j : Fin self.n) : G.IsHom 0 (self.E i j)
• span0 (a : Λ) : G.IsHom 0 a → ∃ (c : Fin self.n → Fin self.n → k), a = ∑ i : Fin self.n, ∑ j : Fin self.n, c i j • self.E i j

theorem MultiplicativeBasisDeformations.LenGrading.MatUnits.diag_complete {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (M : G.MatUnits) : CompleteOrthogonalIdempotents fun (i : Fin M.n) => M.E i i

theorem MultiplicativeBasisDeformations.LenGrading.MatUnits.diag_mul_mul_diag {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (M : G.MatUnits) (i l m : Fin M.n) : M.E i i * M.E l m * M.E i i = if l = i ∧ m = i then M.E i i else 0

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.LenGrading.MatUnits.diag {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (M : G.MatUnits) : G.Diag

The diagonal matrix units as diagonal idempotents (e_i Λ₀ e_i = k e_i).

theorem MultiplicativeBasisDeformations.LenGrading.MatUnits.diag_e {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (M : G.MatUnits) (i : Fin M.n) : M.diag.e i = M.E i i

theorem MultiplicativeBasisDeformations.LenGrading.MatUnits.rt_eq {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (M : G.MatUnits) (i : Fin M.n) : M.rt (M.rt i) = M.rt i

theorem MultiplicativeBasisDeformations.LenGrading.MatUnits.E_rt_mul {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (M : G.MatUnits) (i : Fin M.n) : M.E i (M.rt i) * M.E (M.rt i) i = M.E i i

E_{i,rt i} E_{rt i,i} = E_{ii}.

Linear maps with leading term the identity

theorem MultiplicativeBasisDeformations.PosFiltration.lead_ge {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (Ψ : Λ →ₗ[k] B) (hΨ : ∀ (d : ℕ) (a : Λ), G.IsHom d a → Ψ a ∈ P.F d ∧ (P.σ d) (Ψ a) = a) {d : ℕ} {a : Λ} (ha : G.Ge d a) : Ψ a ∈ P.F d

theorem MultiplicativeBasisDeformations.PosFiltration.lead_surj_aux {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (Ψ : Λ →ₗ[k] B) (hΨ : ∀ (d : ℕ) (a : Λ), G.IsHom d a → Ψ a ∈ P.F d ∧ (P.σ d) (Ψ a) = a) (n d : ℕ) : P.M ≤ d + n → ∀ x ∈ P.F d, ∃ (a : Λ), G.Ge d a ∧ Ψ a = x

theorem MultiplicativeBasisDeformations.PosFiltration.lead_injective {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (Ψ : Λ →ₗ[k] B) (hΨ : ∀ (d : ℕ) (a : Λ), G.IsHom d a → Ψ a ∈ P.F d ∧ (P.σ d) (Ψ a) = a) : Function.Injective ⇑Ψ

noncomputable def MultiplicativeBasisDeformations.PosFiltration.splitOfLead {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (Ψ : Λ →ₗ[k] B) (hΨ : ∀ (d : ℕ) (a : Λ), G.IsHom d a → Ψ a ∈ P.F d ∧ (P.σ d) (Ψ a) = a) (h1 : Ψ 1 = 1) : P.Split

A unital linear map with leading term the identity is a splitting.

theorem MultiplicativeBasisDeformations.PosFiltration.splitOfLead_φ {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (Ψ : Λ →ₗ[k] B) (hΨ : ∀ (d : ℕ) (a : Λ), G.IsHom d a → Ψ a ∈ P.F d ∧ (P.σ d) (Ψ a) = a) (h1 : Ψ 1 = 1) (a : Λ) : (splitOfLead Ψ hΨ h1).φ a = Ψ a

Lifting the matrix units

noncomputable def MultiplicativeBasisDeformations.PosFiltration.aL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (i : Fin M.n) : B

A lift of E_{i,rt i}.

noncomputable def MultiplicativeBasisDeformations.PosFiltration.aR {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (i : Fin M.n) : B

A lift of E_{rt i,i}.

theorem MultiplicativeBasisDeformations.PosFiltration.σ_aL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) (i : Fin M.n) : (P.σ 0) (P.aL M i) = M.E i (M.rt i)

theorem MultiplicativeBasisDeformations.PosFiltration.σ_aR {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) (i : Fin M.n) : (P.σ 0) (P.aR M i) = M.E (M.rt i) i

noncomputable def MultiplicativeBasisDeformations.PosFiltration.xL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (f : Fin M.n → B) (i : Fin M.n) : B

noncomputable def MultiplicativeBasisDeformations.PosFiltration.yL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (f : Fin M.n → B) (i : Fin M.n) : B

theorem MultiplicativeBasisDeformations.PosFiltration.f_xL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : f i * P.xL M f i = P.xL M f i

theorem MultiplicativeBasisDeformations.PosFiltration.xL_f {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : P.xL M f i * f (M.rt i) = P.xL M f i

theorem MultiplicativeBasisDeformations.PosFiltration.f_yL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : f (M.rt i) * P.yL M f i = P.yL M f i

theorem MultiplicativeBasisDeformations.PosFiltration.yL_f {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : P.yL M f i * f i = P.yL M f i

theorem MultiplicativeBasisDeformations.PosFiltration.σ_xL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : (P.σ0 M.diag) (P.xL M f i) = M.E i (M.rt i)

theorem MultiplicativeBasisDeformations.PosFiltration.σ_yL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : (P.σ0 M.diag) (P.yL M f i) = M.E (M.rt i) i

noncomputable def MultiplicativeBasisDeformations.PosFiltration.nL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (f : Fin M.n → B) (i : Fin M.n) : B

f_i − x_i y_i ∈ F¹.

theorem MultiplicativeBasisDeformations.PosFiltration.σ_nL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : (P.σ0 M.diag) (P.nL M f i) = 0

theorem MultiplicativeBasisDeformations.PosFiltration.nL_mem {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : P.nL M f i ∈ P.F 1

theorem MultiplicativeBasisDeformations.PosFiltration.f_nL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : f i * P.nL M f i = P.nL M f i

theorem MultiplicativeBasisDeformations.PosFiltration.nL_f {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : P.nL M f i * f i = P.nL M f i

theorem MultiplicativeBasisDeformations.PosFiltration.nL_pow {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : P.nL M f i ^ (P.M + 1) = 0

noncomputable def MultiplicativeBasisDeformations.PosFiltration.sL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (f : Fin M.n → B) (i : Fin M.n) : B

The geometric series Σ_{t ≤ M} n_i^t, an inverse of 1 − n_i.

theorem MultiplicativeBasisDeformations.PosFiltration.one_sub_mul_sL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : (1 - P.nL M f i) * P.sL M f i = 1

theorem MultiplicativeBasisDeformations.PosFiltration.sL_mul_one_sub {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : P.sL M f i * (1 - P.nL M f i) = 1

theorem MultiplicativeBasisDeformations.PosFiltration.commute_f_sL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : Commute (f i) (P.sL M f i)

noncomputable def MultiplicativeBasisDeformations.PosFiltration.vL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (f : Fin M.n → B) (i : Fin M.n) : B

v_i = f_i s_i, the inverse of x_i y_i in the corner f_iBf_i.

theorem MultiplicativeBasisDeformations.PosFiltration.xy_vL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : P.xL M f i * P.yL M f i * P.vL M f i = f i

theorem MultiplicativeBasisDeformations.PosFiltration.vL_f {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : P.vL M f i * f i = P.vL M f i

theorem MultiplicativeBasisDeformations.PosFiltration.σ_vL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : (P.σ0 M.diag) (P.vL M f i) = M.E i i

noncomputable def MultiplicativeBasisDeformations.PosFiltration.yL' {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (f : Fin M.n → B) (i : Fin M.n) : B

y'_i = y_i v_i, with x_i y'_i = f_i.

theorem MultiplicativeBasisDeformations.PosFiltration.xL_yL' {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : P.xL M f i * P.yL' M f i = f i

theorem MultiplicativeBasisDeformations.PosFiltration.yL'_f {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : P.yL' M f i * f i = P.yL' M f i

theorem MultiplicativeBasisDeformations.PosFiltration.f_yL' {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (i : Fin M.n) : f (M.rt i) * P.yL' M f i = P.yL' M f i

theorem MultiplicativeBasisDeformations.PosFiltration.σ_yL' {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : (P.σ0 M.diag) (P.yL' M f i) = M.E (M.rt i) i

theorem MultiplicativeBasisDeformations.PosFiltration.yL'_xL {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : P.yL' M f i * P.xL M f i = f (M.rt i)

y'_i x_i = f_{rt i}: an idempotent of the corner f_{rt i}Bf_{rt i} congruent to f_{rt i} modulo the nilpotent ideal F¹.

noncomputable def MultiplicativeBasisDeformations.PosFiltration.L {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (f : Fin M.n → B) (i j : Fin M.n) : B

The lifted matrix units L_{ij} = x_i y'_j.

theorem MultiplicativeBasisDeformations.PosFiltration.L_mul {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) {i j l m : Fin M.n} (hij : M.rt i = M.rt j) (hlm : M.rt l = M.rt m) : P.L M f i j * P.L M f l m = if j = l then P.L M f i m else 0

theorem MultiplicativeBasisDeformations.PosFiltration.L_diag {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i : Fin M.n) : P.L M f i i = f i

theorem MultiplicativeBasisDeformations.PosFiltration.σ_L {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (i j : Fin M.n) : (P.σ0 M.diag) (P.L M f i j) = M.E i j

The transported splitting

noncomputable def MultiplicativeBasisDeformations.PosFiltration.Φ {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) (f : Fin M.n → B) (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) : Λ →ₗ[k] B

The splitting transported from the root corners: Φ(a) = Σ_{i,j} L_{i,rt i} φ0(E_{rt i,i} a E_{j,rt j}) L_{rt j,j}.

theorem MultiplicativeBasisDeformations.PosFiltration.Φ_apply {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (a : Λ) : (P.Φ M f hf hσf) a = ∑ i : Fin M.n, ∑ j : Fin M.n, P.L M f i (M.rt i) * (φ0 hf hσf) (M.E (M.rt i) i * a * M.E j (M.rt j)) * P.L M f (M.rt j) j

theorem MultiplicativeBasisDeformations.PosFiltration.E_rt_isHom {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (M : G.MatUnits) {d : ℕ} {a : Λ} (ha : G.IsHom d a) (i j : Fin M.n) : G.IsHom d (M.E (M.rt i) i * a * M.E j (M.rt j))

theorem MultiplicativeBasisDeformations.PosFiltration.Φ_lead {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (d : ℕ) (a : Λ) (ha : G.IsHom d a) : (P.Φ M f hf hσf) a ∈ P.F d ∧ (P.σ d) ((P.Φ M f hf hσf) a) = a

Leading term the identity.

theorem MultiplicativeBasisDeformations.PosFiltration.Φ_left {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) {l m : Fin M.n} (hlm : M.rt l = M.rt m) (a : Λ) : (P.Φ M f hf hσf) (M.E l m * a) = P.L M f l m * (P.Φ M f hf hσf) a

Φ is left S-linear.

theorem MultiplicativeBasisDeformations.PosFiltration.Φ_right {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) {l m : Fin M.n} (hlm : M.rt l = M.rt m) (a : Λ) : (P.Φ M f hf hσf) (a * M.E l m) = (P.Φ M f hf hσf) a * P.L M f l m

Φ is right S-linear.

theorem MultiplicativeBasisDeformations.PosFiltration.Φ_one {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) : (P.Φ M f hf hσf) 1 = 1

Φ is unital.

theorem MultiplicativeBasisDeformations.PosFiltration.Φ_E {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) (l m : Fin M.n) : (P.Φ M f hf hσf) (M.E l m) = P.L M f l m

theorem MultiplicativeBasisDeformations.PosFiltration.Φ_mul_left {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) {s : Λ} (hs : G.IsHom 0 s) (a : Λ) : (P.Φ M f hf hσf) (s * a) = (P.Φ M f hf hσf) s * (P.Φ M f hf hσf) a

theorem MultiplicativeBasisDeformations.PosFiltration.Φ_mul_right {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] {P : PosFiltration G B} (M : G.MatUnits) {f : Fin M.n → B} (hf : CompleteOrthogonalIdempotents f) (hσf : ∀ (i : Fin M.n), (P.σ 0) (f i) = M.diag.e i) {s : Λ} (hs : G.IsHom 0 s) (a : Λ) : (P.Φ M f hf hσf) (a * s) = (P.Φ M f hf hσf) a * (P.Φ M f hf hσf) s

theorem MultiplicativeBasisDeformations.PosFiltration.splitPositiveDeformation_ss {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) : ∃ (S : P.Split), (∀ (s a : Λ), G.IsHom 0 s → S.φ (s * a) = S.φ s * S.φ a) ∧ (∀ (s a : Λ), G.IsHom 0 s → S.φ (a * s) = S.φ a * S.φ s) ∧ (∀ (d : ℕ) (a : Λ), G.IsHom d a → (P.σ d) (S.φ a) = a) ∧ (∀ (d : ℕ), Submodule.map (↑S.φ) (G.geSub d) = P.F d) ∧ (∀ (a b : Λ), S.φ a * S.φ b = S.φ (∑ q ∈ Finset.range G.N, ((S.μ q) a) b)) ∧ (∀ (a b : Λ), ((S.μ 0) a) b = a * b) ∧ (∀ (q d e : ℕ) (a b : Λ), G.IsHom d a → G.IsHom e b → G.IsHom (d + e + q) (((S.μ q) a) b)) ∧ ∀ (q : ℕ), 0 < q → IsRelS G (S.μ q)

Lemma 6.4 (lem:split-positive-deformation) for a split semisimple S = Λ₀ (given by matrix units MatUnits): there is a splitting φ : Λ ≅ B (a filtered linear isomorphism, φ 1 = 1, inducing the identification gr B = Λ) which is multiplicative on S (so S lifts to the unital subalgebra φ(S)) and S-bilinear on both sides; the transported multiplication is μ₀ + Σ_{q>0} μ_q with μ₀ the multiplication of Λ, each μ_q raising the degree by q, S-relative and vanishing when an input belongs to S.

theorem MultiplicativeBasisDeformations.PosFiltration.nonempty_split_ss {k : Type u_1} [Field k] {Λ : Type u_2} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type u_3} [Ring B] [Algebra k B] (P : PosFiltration G B) (M : G.MatUnits) : Nonempty P.Split

A splitting exists for a split semisimple Λ₀, so Proposition 6.5 (exists_fLift_of_split, fLift_unique_of_split, fLift_map_of_split, fLift_leading_of_split, fLift_gr_hom_of_split, fLift_orderGe_zero_of_split, isRad_iff, mem_radPow_iff) applies; the splitting is multiplicative on the left by every e ∈ Λ₀, so Split.regularLift gives the regular lifts eB of eΛ for every idempotent e of Λ₀.