Lemma 9.2: the centralizer ray algebra B_χ

lem:centralizer-ray-algebra (integral-partial-lifts.tex). The centralizer C_χ = Cent_{A₀}(q̂) is spanned by the identities, the two-sided rays and the unshiftable rays; B_χ = C_χ/𝔞_χ has basis the supporting identities and the two-sided rays, with the products of A₀ (zero when the product leaves the basis). We record these as ray tables Tc (the centralizer) and Qχ (the two-sided table) with morphisms Tc → P (inclusion) and Tc → Qχ (quotient), and the projection π : kP → kQχ.

structure MultiplicativeBasisDeformations.RaySys.Tab.SubData {V R L : Type} [AddCommGroup L] (P : Tab V R L) : Type

Data for a sub-table: selected vertices and rays, closed enough for associativity.

• pV : V → Prop
• pR : R → Prop
• e_mem (x : V) : self.pV x → self.pR (P.e x)
• src_mem (r : R) : self.pR r → self.pV (P.src r)
• tgt_mem (r : R) : self.pR r → self.pV (P.tgt r)
• cc (r s u t v w : R) : self.pR r → self.pR s → self.pR u → P.mul r s = some t → P.mul t u = some w → P.mul s u = some v → self.pR w → (self.pR t ↔ self.pR v)

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.subMul {V R L : Type} [AddCommGroup L] {P : Tab V R L} (D : P.SubData) (r s : { r : R // D.pR r }) : Option { r : R // D.pR r }

The restricted product: zero when the product leaves the selected rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.subMul_eq_some {V R L : Type} [AddCommGroup L] {P : Tab V R L} (D : P.SubData) {r s t : { r : R // D.pR r }} : subMul D r s = some t ↔ P.mul ↑r ↑s = some ↑t

theorem MultiplicativeBasisDeformations.RaySys.Tab.subMul_assoc {V R L : Type} [AddCommGroup L] {P : Tab V R L} (D : P.SubData) (r s u : { r : R // D.pR r }) : ((subMul D r s).bind fun (t : { r : R // D.pR r }) => subMul D t u) = (subMul D s u).bind fun (t : { r : R // D.pR r }) => subMul D r t

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.sub {V R L : Type} [AddCommGroup L] {P : Tab V R L} (D : P.SubData) : Tab { x : V // D.pV x } { r : R // D.pR r } L

The sub-table.

def MultiplicativeBasisDeformations.RaySys.Sys.InC {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (r : R) : Prop

Rays of the centralizer: two-sided or unshiftable.

theorem MultiplicativeBasisDeformations.RaySys.Sys.e_inC {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (x : V) : S.InC χ (S.P.e x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.inC_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r s t : R} (hr : S.InC χ r) (hs : S.InC χ s) (h : S.rr r * S.rr s = S.rr t) : S.InC χ t

The centralizer is closed under products (integral-partial-lifts.tex).

def MultiplicativeBasisDeformations.RaySys.Sys.InQ {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (r : R) : Prop

Rays of B_χ: two-sided rays and supporting identities.

theorem MultiplicativeBasisDeformations.RaySys.Sys.inQ_src {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r : R} (h : S.InQ χ r) : S.Supp χ (S.P.src r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.inQ_tgt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r : R} (h : S.InQ χ r) : S.Supp χ (S.P.tgt r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.inQ_inC {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r : R} (h : S.InQ χ r) : S.InC χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.inQ_of_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r s t : R} (hrs : S.InC χ r ∨ S.InC χ s) (h : S.rr r * S.rr s = S.rr t) (ht : S.InQ χ t) : S.InQ χ r ∧ S.InQ χ s

A retained product has retained factors when one factor lies in the centralizer (integral-partial-lifts.tex).

def MultiplicativeBasisDeformations.RaySys.Sys.cData {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) : S.P.SubData

The centralizer sub-table data.

def MultiplicativeBasisDeformations.RaySys.Sys.qData {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) : S.P.SubData

The two-sided sub-table data (Q_χ).

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.Tc {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) : Tab { x : V // (S.cData hχ hprim).pV x } { r : R // (S.cData hχ hprim).pR r } L

The centralizer table Tc.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.Qχ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) : Tab { x : V // (S.qData hχ hprim).pV x } { r : R // (S.qData hχ hprim).pR r } L

The two-sided table Q_χ; B_χ = kQ_χ.

def MultiplicativeBasisDeformations.RaySys.Sys.incl {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) : Mor (S.Tc hχ hprim).toMult S.P.toMult

The inclusion Tc → P.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.quot {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) : Mor (S.Tc hχ hprim).toMult (S.Qχ hχ hprim).toMult

The quotient Tc → Q_χ.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.proj {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] : ↥(S.P.Lin k) →ₗ[k] ↥((S.Qχ hχ hprim).Lin k)

The projection π : kP → kQ_χ onto the retained rays.

theorem MultiplicativeBasisDeformations.RaySys.Sys.proj_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] (r : R) : (S.proj hχ hprim k) (S.P.b k r) = if h : S.InQ χ r then (S.Qχ hχ hprim).b k ⟨r, h⟩ else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.quot_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] (r : { r : R // (S.cData hχ hprim).pR r }) : ((S.quot hχ hprim).alg k) ((S.Tc hχ hprim).b k r) = if h : S.InQ χ ↑r then (S.Qχ hχ hprim).b k ⟨↑r, h⟩ else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.incl_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] (r : { r : R // (S.cData hχ hprim).pR r }) : ((S.incl hχ hprim).alg k) ((S.Tc hχ hprim).b k r) = S.P.b k ↑r

theorem MultiplicativeBasisDeformations.RaySys.Sys.Qb_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] {r s : R} (hr : S.InQ χ r) (hs : S.InQ χ s) : (S.Qχ hχ hprim).b k ⟨r, hr⟩ * (S.Qχ hχ hprim).b k ⟨s, hs⟩ = match S.P.mul r s with | some t => if h : S.InQ χ t then (S.Qχ hχ hprim).b k ⟨t, h⟩ else 0 | none => 0

The product of two retained basis vectors of kQ_χ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.proj_left {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] (x : ↥((S.Tc hχ hprim).Lin k)) (y : ↥(S.P.Lin k)) : (S.proj hχ hprim k) (((S.incl hχ hprim).alg k) x * y) = ((S.quot hχ hprim).alg k) x * (S.proj hχ hprim k) y

π(c b) = q(c) π(b) (the retained-product analysis).

theorem MultiplicativeBasisDeformations.RaySys.Sys.proj_right {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] (y : ↥(S.P.Lin k)) (x : ↥((S.Tc hχ hprim).Lin k)) : (S.proj hχ hprim k) (y * ((S.incl hχ hprim).alg k) x) = (S.proj hχ hprim k) y * ((S.quot hχ hprim).alg k) x

π(b c) = π(b) q(c).

theorem MultiplicativeBasisDeformations.RaySys.Sys.incl_injective {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] : Function.Injective ⇑((S.incl hχ hprim).alg k)

theorem MultiplicativeBasisDeformations.RaySys.Sys.Qχ_isRepresentationFinite {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (k : Type u) [Field k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) : IsRepresentationFinite k ↥((S.Qχ hχ hprim).Lin k)

Lemma 9.2 (lem:centralizer-ray-algebra), representation-finiteness: B_χ = kQ_χ is representation-finite (Lemma 4.6 applied to C_χ ⊆ A₀, the quotient C_χ → B_χ and π).

The weight group of Q_χ

def MultiplicativeBasisDeformations.RaySys.Tab.IsAdd {L : Type} [AddCommGroup L] {V' R' : Type} (T : Tab V' R' L) {N : Type u_1} [AddCommGroup N] (f : R' → N) : Prop

Additive functions on a ray table (homomorphisms out of W(P)).

theorem MultiplicativeBasisDeformations.RaySys.Sys.hW_of_Qχ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hQ : ∀ (w : { r : R // (S.qData hχ hprim).pR r } → ZMod 2), (S.Qχ hχ hprim).IsAdd w → ∃ (ω : { r : R // (S.qData hχ hprim).pR r } → ℤ), (S.Qχ hχ hprim).IsAdd ω ∧ ∀ (r : { r : R // (S.qData hχ hprim).pR r }), ↑(ω r) = w r) (w : R → ZMod 2) : (∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → w t = w r + w s) → ∃ (ω : R → ℤ), (∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) ∧ ∀ (r : R), S.TB χ r → ↑(ω r) = w r

Lemma 9.2, the weight group: the lifting property of W(Q_χ) gives the lifting property used in Theorem 9.1(3).

theorem MultiplicativeBasisDeformations.RaySys.Sys.q_nilpotent {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) : ∃ (n : ℕ), S.q x ^ (n + 1) = 0

The local generators are nilpotent.

theorem MultiplicativeBasisDeformations.RaySys.Sys.card_Qχ_lt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (hx : ∃ (x : V), S.Supp χ x) : Fintype.card { r : R // (S.qData hχ hprim).pR r } < Fintype.card R

Lemma 9.2, dimension: Q_χ has fewer rays than P, unless no vertex supports χ (dim B_χ < dim A).