Multiplicative bases

MultiplicativeBasisDeformations.Foundations.PositiveDeformation

Positive filtered deformations #

Definition 6.2 (def:positive-deformation, positive-deformations.tex): "A positive filtered deformation of a finite-dimensional nonnegatively graded algebra Λ is an algebra B with a finite decreasing multiplicative filtration and an identification gr B = Λ." The identification is recorded by the leading-term maps σ_d : F^d → Λ_d (PosFiltration), surjective with kernel F^{d+1} and multiplicative.

Lemma 6.4 (lem:split-positive-deformation, lines 189–233): the vertex idempotents lift (through the nilpotent ideal F¹), and the filtration splits as S-bimodules, giving a linear isomorphism φ : Λ ≅ B that is an S-bimodule map, sends Λ_{≥d} onto F^d and has leading term the identity (exists_split). In the transported multiplication a ⋆ b = φ⁻¹(φa φb) the S-actions are those of Λ and a ⋆ b - ab raises degree (star_sub_mul_ge).

Here the splitting is built from diagonal idempotents whose degree-0 corners are lines (Diag, exists_splitD); for S = Λ₀ ≅ kⁿ (Vertices) this is exists_split. A split semisimple S with matrix blocks is handled in Refinements/SplitSemisimple.lean by lifting matrix units and transporting the splitting of the root corners.

def MultiplicativeBasisDeformations.LenGrading.geSub {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (m : ℕ) :

Submodule k Λ

Λ_{≥ m}.

Instances For

theorem MultiplicativeBasisDeformations.LenGrading.mem_geSub {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) {m : ℕ} {a : Λ} :

a ∈ G.geSub m ↔ G.Ge m a

theorem MultiplicativeBasisDeformations.LenGrading.isHom_sum {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) {d : ℕ} {ι : Type u_1} (s : Finset ι) (f : ι → Λ) (h : ∀ i ∈ s, G.IsHom d (f i)) :

G.IsHom d (∑ i ∈ s, f i)

theorem MultiplicativeBasisDeformations.LenGrading.ge_sub_proj {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) {m : ℕ} {a : Λ} (ha : G.Ge m a) :

G.Ge (m + 1) (a - (G.proj m) a)

theorem MultiplicativeBasisDeformations.LenGrading.eq_zero_of_ge {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) {m : ℕ} {a : Λ} (ha : G.Ge m a) (hm : G.N ≤ m) :

a = 0

theorem MultiplicativeBasisDeformations.LenGrading.ge_sum_proj {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (m : ℕ) (a : Λ) :

G.Ge m (∑ e ∈ Finset.Ico m G.N, (G.proj e) a)

theorem MultiplicativeBasisDeformations.LenGrading.eq_sum_proj_of_ge {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) {m : ℕ} {a : Λ} (ha : G.Ge m a) :

a = ∑ e ∈ Finset.Ico m G.N, (G.proj e) a

theorem MultiplicativeBasisDeformations.LenGrading.corner_corner {R : Type u_1} [Ring R] {ι : Type u_2} [DecidableEq ι] {e : ι → R} (he : OrthogonalIdempotents e) (i j i' j' : ι) (y : R) :

e i' * (e i * y * e j) * e j' = if i' = i ∧ j' = j then e i * y * e j else 0

structure MultiplicativeBasisDeformations.LenGrading.Vertices {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) :

Vertex idempotents: a complete set of orthogonal idempotents of degree 0 spanning Λ₀ (S = Λ₀ ≅ kⁿ).

n : ℕ
e : Fin self.n → Λ
complete : CompleteOrthogonalIdempotents self.e
deg0 (i : Fin self.n) : G.IsHom 0 (self.e i)
span0 (a : Λ) : G.IsHom 0 a → ∃ (c : Fin self.n → k), a = ∑ i : Fin self.n, c i • self.e i

Instances For

theorem MultiplicativeBasisDeformations.LenGrading.Vertices.isHom_one {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) :

G.IsHom 0 1

structure MultiplicativeBasisDeformations.LenGrading.Diag {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) :

Diagonal idempotents: a complete set of orthogonal idempotents of degree 0 whose degree-0 diagonal corners are lines (e_i Λ₀ e_i = k e_i). The vertex idempotents of Λ₀ ≅ kⁿ (Vertices) and the diagonal matrix units of a split semisimple Λ₀ are examples.

n : ℕ
e : Fin self.n → Λ
complete : CompleteOrthogonalIdempotents self.e
deg0 (i : Fin self.n) : G.IsHom 0 (self.e i)
corner0 (i : Fin self.n) (a : Λ) : G.IsHom 0 a → ∃ (c : k), self.e i * a * self.e i = c • self.e i

Instances For

theorem MultiplicativeBasisDeformations.LenGrading.Diag.isHom_one {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Diag) :

G.IsHom 0 1

def MultiplicativeBasisDeformations.LenGrading.Vertices.toDiag {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Vertices) :

Vertex idempotents are diagonal idempotents.

Instances For

structure MultiplicativeBasisDeformations.PosFiltration {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] (G : LenGrading k Λ) (B : Type w) [Ring B] [Algebra k B] :

Type (max v w)

Definition 6.2: a positive filtered deformation B of Λ: a finite decreasing multiplicative filtration F with F⁰ = B, and leading-term maps σ_d identifying F^d/F^{d+1} with Λ_d multiplicatively.

F : ℕ → Submodule k B
F_zero : self.F 0 = ⊤
F_succ_le (d : ℕ) : self.F (d + 1) ≤ self.F d
F_mul (d e : ℕ) (a b : B) : a ∈ self.F d → b ∈ self.F e → a * b ∈ self.F (d + e)
M : ℕ
F_M : self.F self.M = ⊥
σ : ℕ → B →ₗ[k] Λ
σ_hom (d : ℕ) (a : B) : G.IsHom d ((self.σ d) a)
σ_ker (d : ℕ) (a : B) : a ∈ self.F d → ((self.σ d) a = 0 ↔ a ∈ self.F (d + 1))
σ_surj (d : ℕ) (x : Λ) : G.IsHom d x → ∃ a ∈ self.F d, (self.σ d) a = x
σ_mul (d e : ℕ) (a b : B) : a ∈ self.F d → b ∈ self.F e → (self.σ (d + e)) (a * b) = (self.σ d) a * (self.σ e) b

Instances For

theorem MultiplicativeBasisDeformations.PosFiltration.mem_zero {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (a : B) :

a ∈ P.F 0

theorem MultiplicativeBasisDeformations.PosFiltration.F_anti {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) {d d' : ℕ} (h : d ≤ d') :

P.F d' ≤ P.F d

theorem MultiplicativeBasisDeformations.PosFiltration.mul_mem_left {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) {d : ℕ} (a : B) {b : B} (hb : b ∈ P.F d) :

a * b ∈ P.F d

theorem MultiplicativeBasisDeformations.PosFiltration.mul_mem_right {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) {d : ℕ} {a : B} (b : B) (ha : a ∈ P.F d) :

a * b ∈ P.F d

theorem MultiplicativeBasisDeformations.PosFiltration.eq_bot_of_le {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) {d : ℕ} (h : P.M ≤ d) :

P.F d = ⊥

theorem MultiplicativeBasisDeformations.PosFiltration.σ_mul_left {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (d : ℕ) (a b : B) (hb : b ∈ P.F d) :

(P.σ d) (a * b) = (P.σ 0) a * (P.σ d) b

theorem MultiplicativeBasisDeformations.PosFiltration.σ_mul_right {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (d : ℕ) (a b : B) (ha : a ∈ P.F d) :

(P.σ d) (a * b) = (P.σ d) a * (P.σ 0) b

theorem MultiplicativeBasisDeformations.PosFiltration.pow_mem {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) {x : B} (hx : x ∈ P.F 1) (n : ℕ) :

x ^ (n + 1) ∈ P.F (n + 1)

def MultiplicativeBasisDeformations.PosFiltration.σ0 {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Diag) :

B →+* Λ

The leading term in degree 0, as a ring homomorphism B → Λ.

Instances For

theorem MultiplicativeBasisDeformations.PosFiltration.σ0_apply {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Diag) (a : B) :

(P.σ0 V) a = (P.σ 0) a

theorem MultiplicativeBasisDeformations.PosFiltration.ker_σ0_nilpotent {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Diag) (x : B) :

x ∈ RingHom.ker (P.σ0 V) → IsNilpotent x

theorem MultiplicativeBasisDeformations.PosFiltration.exists_lift {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Diag) :

∃ (eL : Fin V.n → B), CompleteOrthogonalIdempotents eL ∧ ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i

Lifted vertex idempotents.

Splitting the filtration as `S`-bimodules #

def MultiplicativeBasisDeformations.PosFiltration.cornerMap {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (V : G.Diag) (eL : Fin V.n → B) (i j : Fin V.n) :

B →ₗ[k] B

x ↦ ẽ_i x ẽ_j.

Instances For

theorem MultiplicativeBasisDeformations.PosFiltration.cornerMap_apply {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (V : G.Diag) (eL : Fin V.n → B) (i j : Fin V.n) (x : B) :

(cornerMap V eL i j) x = eL i * x * eL j

def MultiplicativeBasisDeformations.PosFiltration.C {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Diag) (eL : Fin V.n → B) (i j : Fin V.n) (d : ℕ) :

Submodule k B

The corner ẽ_i F^d ẽ_j.

Instances For

noncomputable def MultiplicativeBasisDeformations.PosFiltration.W {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Diag) (eL : Fin V.n → B) (i j : Fin V.n) (d : ℕ) :

Submodule k B

A complement of ẽ_i F^{d+1} ẽ_j in ẽ_i F^d ẽ_j (the line of ẽ_i in the degree-0 diagonal corners).

Instances For

theorem MultiplicativeBasisDeformations.PosFiltration.mem_C {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) {i j : Fin V.n} {d : ℕ} {x : B} :

x ∈ P.C V eL i j d ↔ x ∈ P.F d ∧ eL i * x * eL j = x

theorem MultiplicativeBasisDeformations.PosFiltration.C_succ_le {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (i j : Fin V.n) (d : ℕ) :

P.C V eL i j (d + 1) ≤ P.C V eL i j d

theorem MultiplicativeBasisDeformations.PosFiltration.idem_eq_zero {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {x : B} (hx : IsIdempotentElem x) (h1 : x ∈ P.F 1) :

x = 0

theorem MultiplicativeBasisDeformations.PosFiltration.eL_mem_C {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (i : Fin V.n) :

eL i ∈ P.C V eL i i 0

theorem MultiplicativeBasisDeformations.PosFiltration.W_le {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (i j : Fin V.n) (d : ℕ) :

P.W V eL i j d ≤ P.C V eL i j d

theorem MultiplicativeBasisDeformations.PosFiltration.σ0_corner_eq {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) {i : Fin V.n} {x : B} (hx : eL i * x * eL i = x) (heL : CompleteOrthogonalIdempotents eL) :

∃ (c : k), (P.σ 0) x = c • V.e i

theorem MultiplicativeBasisDeformations.PosFiltration.sup_W {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i j : Fin V.n) (d : ℕ) :

P.C V eL i j (d + 1) ⊔ P.W V eL i j d = P.C V eL i j d

theorem MultiplicativeBasisDeformations.PosFiltration.W_inf {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) {i j : Fin V.n} {d : ℕ} {x : B} (hx : x ∈ P.W V eL i j d) (hx' : x ∈ P.C V eL i j (d + 1)) (heL : CompleteOrthogonalIdempotents eL) :

x = 0

def MultiplicativeBasisDeformations.PosFiltration.Lc {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Diag) (i j : Fin V.n) (d : ℕ) :

Submodule k Λ

The corner e_i Λ_d e_j of Λ.

Instances For

def MultiplicativeBasisDeformations.PosFiltration.πc {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} (V : G.Diag) (i j : Fin V.n) (d : ℕ) :

Λ →ₗ[k] Λ

a ↦ e_i (proj_d a) e_j.

Instances For

theorem MultiplicativeBasisDeformations.PosFiltration.πc_apply {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {V : G.Diag} (i j : Fin V.n) (d : ℕ) (a : Λ) :

(πc V i j d) a = V.e i * (G.proj d) a * V.e j

theorem MultiplicativeBasisDeformations.PosFiltration.πc_mem {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {V : G.Diag} (i j : Fin V.n) (d : ℕ) (a : Λ) :

(πc V i j d) a ∈ Lc V i j d

theorem MultiplicativeBasisDeformations.PosFiltration.πc_of_mem {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {V : G.Diag} {i j : Fin V.n} {d : ℕ} {x : Λ} (hx : x ∈ Lc V i j d) (i' j' : Fin V.n) (d' : ℕ) :

(πc V i' j' d') x = if i' = i ∧ j' = j ∧ d' = d then x else 0

theorem MultiplicativeBasisDeformations.PosFiltration.σ_corner {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) {d : ℕ} {x : B} (hx : x ∈ P.F d) (i j : Fin V.n) :

(P.σ d) (eL i * x * eL j) = V.e i * (P.σ d) x * V.e j

noncomputable def MultiplicativeBasisDeformations.PosFiltration.τ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Diag) (eL : Fin V.n → B) (i j : Fin V.n) (d : ℕ) :

↥(P.W V eL i j d) →ₗ[k] Λ

σ_d on the complement.

Instances For

theorem MultiplicativeBasisDeformations.PosFiltration.τ_injective {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i j : Fin V.n) (d : ℕ) :

Function.Injective ⇑(P.τ V eL i j d)

theorem MultiplicativeBasisDeformations.PosFiltration.range_τ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i j : Fin V.n) (d : ℕ) :

(P.τ V eL i j d).range = Lc V i j d

noncomputable def MultiplicativeBasisDeformations.PosFiltration.ψ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i j : Fin V.n) (d : ℕ) :

Λ →ₗ[k] B

The inverse of σ_d on the corner e_i Λ_d e_j, extended by the corner projection.

Instances For

theorem MultiplicativeBasisDeformations.PosFiltration.ψ_mem {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i j : Fin V.n) (d : ℕ) (a : Λ) :

(ψ heL hσe i j d) a ∈ P.W V eL i j d

theorem MultiplicativeBasisDeformations.PosFiltration.σ_ψ {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i j : Fin V.n) (d : ℕ) (a : Λ) :

(P.σ d) ((ψ heL hσe i j d) a) = (πc V i j d) a

theorem MultiplicativeBasisDeformations.PosFiltration.ψ_eq_zero {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) {i j : Fin V.n} {d : ℕ} {a : Λ} (h : (πc V i j d) a = 0) :

(ψ heL hσe i j d) a = 0

theorem MultiplicativeBasisDeformations.PosFiltration.ψ_mem_F {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i j : Fin V.n) (d : ℕ) (a : Λ) :

(ψ heL hσe i j d) a ∈ P.F d

theorem MultiplicativeBasisDeformations.PosFiltration.ψ_corner {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i j : Fin V.n) (d : ℕ) (a : Λ) :

eL i * (ψ heL hσe i j d) a * eL j = (ψ heL hσe i j d) a

noncomputable def MultiplicativeBasisDeformations.PosFiltration.φ0 {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) :

Λ →ₗ[k] B

The splitting map φ = Σ ψ_{ijd}.

Instances For

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_apply {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (a : Λ) :

(φ0 heL hσe) a = ∑ i : Fin V.n, ∑ j : Fin V.n, ∑ d ∈ Finset.range G.N, (ψ heL hσe i j d) a

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_of_mem {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) {i j : Fin V.n} {d : ℕ} {x : Λ} (hx : x ∈ Lc V i j d) :

(φ0 heL hσe) x = (ψ heL hσe i j d) x

theorem MultiplicativeBasisDeformations.PosFiltration.eq_sum_corners {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {V : G.Diag} (a : Λ) :

a = ∑ i : Fin V.n, ∑ j : Fin V.n, V.e i * a * V.e j

theorem MultiplicativeBasisDeformations.PosFiltration.mem_Lc_of_hom {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {V : G.Diag} {d : ℕ} {a : Λ} (ha : G.IsHom d a) (i j : Fin V.n) :

V.e i * a * V.e j ∈ Lc V i j d

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_hom {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) {d : ℕ} {a : Λ} (ha : G.IsHom d a) :

(φ0 heL hσe) a ∈ P.F d ∧ (P.σ d) ((φ0 heL hσe) a) = a

Leading terms: φ maps Λ_d into F^d with leading term the identity.

theorem MultiplicativeBasisDeformations.PosFiltration.eq_sum_πc {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {V : G.Diag} (a : Λ) :

a = ∑ i : Fin V.n, ∑ j : Fin V.n, ∑ d ∈ Finset.range G.N, (πc V i j d) a

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_left {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (l : Fin V.n) (a : Λ) :

(φ0 heL hσe) (V.e l * a) = eL l * (φ0 heL hσe) a

φ is an S-bimodule map.

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_right {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (l : Fin V.n) (a : Λ) :

(φ0 heL hσe) (a * V.e l) = (φ0 heL hσe) a * eL l

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_ge {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) {d : ℕ} {a : Λ} (ha : G.Ge d a) :

(φ0 heL hσe) a ∈ P.F d

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_surj_aux {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (n d : ℕ) :

P.M ≤ d + n → ∀ x ∈ P.F d, ∃ (a : Λ), G.Ge d a ∧ (φ0 heL hσe) a = x

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_injective {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) :

Function.Injective ⇑(φ0 heL hσe)

theorem MultiplicativeBasisDeformations.PosFiltration.φ0_e {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} {V : G.Diag} {eL : Fin V.n → B} (heL : CompleteOrthogonalIdempotents eL) (hσe : ∀ (i : Fin V.n), (P.σ 0) (eL i) = V.e i) (i : Fin V.n) :

(φ0 heL hσe) (V.e i) = eL i

theorem MultiplicativeBasisDeformations.PosFiltration.exists_splitD {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] (P : PosFiltration G B) (V : G.Diag) :

∃ (φ : Λ ≃ₗ[k] B), (CompleteOrthogonalIdempotents fun (i : Fin V.n) => φ (V.e i)) ∧ (∀ (i : Fin V.n) (a : Λ), φ (V.e i * a) = φ (V.e i) * φ a) ∧ (∀ (i : Fin V.n) (a : Λ), φ (a * V.e i) = φ a * φ (V.e i)) ∧ (∀ (d : ℕ) (a : Λ), G.IsHom d a → (P.σ d) (φ a) = a) ∧ ∀ (d : ℕ), Submodule.map (↑φ) (G.geSub d) = P.F d

The diagonal idempotents lift, and the filtration splits compatibly: a linear isomorphism φ : Λ ≅ B sending e_i to the lifted idempotents, linear for them on both sides, mapping Λ_{≥d} onto F^d, with leading term the identity.

theorem MultiplicativeBasisDeformations.PosFiltration.exists_split {k : Type u} [Field k] {Λ : Type v} [Ring Λ] [Algebra k Λ] {G : LenGrading k Λ} {B : Type w} [Ring B] [Algebra k B] {P : PosFiltration G B} (V : G.Vertices) :

∃ (φ : Λ ≃ₗ[k] B), (CompleteOrthogonalIdempotents fun (i : Fin V.n) => φ (V.e i)) ∧ (∀ (i : Fin V.n) (a : Λ), φ (V.e i * a) = φ (V.e i) * φ a) ∧ (∀ (i : Fin V.n) (a : Λ), φ (a * V.e i) = φ a * φ (V.e i)) ∧ (∀ (d : ℕ) (a : Λ), G.IsHom d a → (P.σ d) (φ a) = a) ∧ ∀ (d : ℕ), Submodule.map (↑φ) (G.geSub d) = P.F d

Lemma 6.4 for S = Λ₀ ≅ kⁿ: the vertex idempotents lift, and the filtration splits as S-bimodules: a linear isomorphism φ : Λ ≅ B sending e_i to the lifted idempotents, S-bilinear, mapping Λ_{≥d} onto F^d, with leading term the identity. For a split semisimple S see PosFiltration.splitPositiveDeformation_ss.