Lemma 9.2 as stated: B_χ = C_χ/𝔞_χ ≅ kQ_χ

integral-partial-lifts.tex (lem:centralizer-ray-algebra). Put q̂ = ∑_x q̂_x, C_χ = Cent_{A₀}(q̂), 𝔞_χ = {c ∈ C_χ : q̂c = 0} and B_χ = C_χ/𝔞_χ. "The algebra B_χ is basic and representation-finite. Its basis consists of the supporting identities and the two-sided rays of A₀, and its products define a weighted multiplication table Q_χ ... Thus B_χ = kQ_χ. If B_χ ≠ 0, it has strictly fewer nonzero basis labels than P."

CentralizerTable.lean builds the tables Tc and Q_χ and proves the representation finiteness and the count. Here the algebras themselves: q̂ b_r = b_{r⁺} or 0, and likewise on the right (qhat_mul_b_cases, b_mul_qhat_cases), so the commutator of q̂ with a ray is ±b_{r⁺} exactly for one-sided rays (comm_b); successors of distinct rays are distinct (succ_inj). Hence C_χ is spanned by the identities, two-sided and unshiftable rays (mem_Cχ_iff, Cχ_eq_range), 𝔞_χ by the unshiftable nonidentity rays and the identities at q̂_x = 0 (mem_aχ_iff), and the quotient map C_χ → kQ_χ induces B_χ ≅ kQ_χ (Bχ_equiv, centralizerRayAlgebra).

theorem MultiplicativeBasisDeformations.IsBasicAlgebra.of_ringEquiv {A : Type u_1} {B : Type u_2} [Ring A] [Ring B] (f : A ≃+* B) (h : IsBasicAlgebra A) : IsBasicAlgebra B

Basic algebras are invariant under ring isomorphisms.

Successors

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

A ray with the endpoints of r and weight ℓ(r) + χ exists.

theorem MultiplicativeBasisDeformations.RaySys.Sys.succ_spec' {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.HasSucc χ r) : S.P.src (S.succ χ r) = S.P.src r ∧ S.P.tgt (S.succ χ r) = S.P.tgt r ∧ S.P.wt (S.succ χ r) = S.P.wt r + χ

theorem MultiplicativeBasisDeformations.RaySys.Sys.succ_inj {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r r' : R} (h : S.HasSucc χ r) (h' : S.HasSucc χ r') (e : S.succ χ r = S.succ χ r') : r = r'

Distinct rays have distinct successors.

theorem MultiplicativeBasisDeformations.RaySys.Sys.qh_loop {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.qh χ x = 0 ∨ ∃ (g : R), S.qh χ x = S.rr g ∧ S.P.src g = x ∧ S.P.tgt g = x ∧ S.P.wt g = χ

theorem MultiplicativeBasisDeformations.RaySys.Sys.qh_mul_of_ne {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {x : V} {r : R} (h : x ≠ S.P.src r) : S.qh χ x * S.rr r = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.mul_qh_of_ne {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {x : V} {r : R} (h : x ≠ S.P.tgt r) : S.rr r * S.qh χ x = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.qh_mul_eq {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (r : R) : S.qh χ (S.P.src r) * S.rr r = 0 ∨ S.HasSucc χ r ∧ S.qh χ (S.P.src r) * S.rr r = S.rr (S.succ χ r)

q̂_x r is zero or the successor of r.

theorem MultiplicativeBasisDeformations.RaySys.Sys.mul_qh_eq {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (r : R) : S.rr r * S.qh χ (S.P.tgt r) = 0 ∨ S.HasSucc χ r ∧ S.rr r * S.qh χ (S.P.tgt r) = S.rr (S.succ χ r)

r q̂_y is zero or the successor of r.

The actions of q̂ on rays

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

The left action of q̂ survives on r.

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

The right action of q̂ survives on r.

theorem MultiplicativeBasisDeformations.RaySys.Sys.e_mul_qh {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.rr (S.P.e x) * S.qh χ x = S.qh χ x

theorem MultiplicativeBasisDeformations.RaySys.Sys.qh_mul_e {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.qh χ x * S.rr (S.P.e x) = S.qh χ x

theorem MultiplicativeBasisDeformations.RaySys.Sys.lq_iff_rq {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 : R) : S.InC χ r ↔ (S.Lq χ r ↔ S.Rq χ r)

Both actions agree on the centralizer rays, and differ on the others.

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

On the centralizer rays, the left action survives exactly on the rays of Q_χ.

Elements of kP

def MultiplicativeBasisDeformations.RaySys.Sys.toLin {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] : M S.P.toMult → ↥(S.P.Lin k)

Elements of the monoid with zero as elements of kP.

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Sys.toLin_one {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] : S.toLin k 1 = 1

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Sys.toLin_zero {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] : S.toLin k 0 = 0

@[simp]

theorem MultiplicativeBasisDeformations.RaySys.Sys.toLin_rr {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (r : R) : S.toLin k (S.rr r) = S.P.b k r

theorem MultiplicativeBasisDeformations.RaySys.Sys.toLin_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (a b : M S.P.toMult) : S.toLin k (a * b) = S.toLin k a * S.toLin k b

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.qhat {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (χ : L) : ↥(S.P.Lin k)

q̂ = ∑_x q̂_x.

theorem MultiplicativeBasisDeformations.RaySys.Sys.qhat_mul_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (r : R) : S.qhat k χ * S.P.b k r = S.toLin k (S.qh χ (S.P.src r) * S.rr r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.b_mul_qhat {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (r : R) : S.P.b k r * S.qhat k χ = S.toLin k (S.rr r * S.qh χ (S.P.tgt r))

theorem MultiplicativeBasisDeformations.RaySys.Sys.qhat_mul_b' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (r : R) : S.qhat k χ * S.P.b k r = if S.Lq χ r then S.P.b k (S.succ χ r) else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.b_mul_qhat' {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (r : R) : S.P.b k r * S.qhat k χ = if S.Rq χ r then S.P.b k (S.succ χ r) else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.hasSucc_of_lq {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.Lq χ r) : S.HasSucc χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.hasSucc_of_rq {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.Rq χ r) : S.HasSucc χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.sum_succ_eq_zero_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (p : R → Prop) [DecidablePred p] (hp : ∀ (r : R), p r → S.HasSucc χ r) (a : R → k) : (∑ r : R, if p r then a r • S.P.b k (S.succ χ r) else 0) = 0 ↔ ∀ (r : R), p r → a r = 0

Coefficients of a combination of successors.

The centralizer and the ideal

def MultiplicativeBasisDeformations.RaySys.Sys.Cχ {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (χ : L) : Subalgebra k ↥(S.P.Lin k)

C_χ = Cent_{A₀}(q̂).

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.Sys.instRingSubtypeMatrixMemSubalgebraLinPCχ {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (χ : L) : Ring ↥(S.Cχ k χ)

A shortcut: instance search through the matrix algebra is slow.

theorem MultiplicativeBasisDeformations.RaySys.Sys.mem_Cχ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (c : ↥(S.P.Lin k)) : c ∈ S.Cχ k χ ↔ S.qhat k χ * c = c * S.qhat k χ

theorem MultiplicativeBasisDeformations.RaySys.Sys.sum_repr {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (c : ↥(S.P.Lin k)) : ∑ r : R, ((S.P.basis k).repr c) r • S.P.b k r = c

theorem MultiplicativeBasisDeformations.RaySys.Sys.mem_Cχ_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (c : ↥(S.P.Lin k)) : c ∈ S.Cχ k χ ↔ ∀ (r : R), ¬S.InC χ r → ((S.P.basis k).repr c) r = 0

C_χ is spanned by the identities, the two-sided rays and the unshiftable rays.

theorem MultiplicativeBasisDeformations.RaySys.Sys.repr_incl {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (x : ↥((S.Tc hχ hprim).Lin k)) (r : R) : ((S.P.basis k).repr (((S.incl hχ hprim).alg k) x)) r = if h : S.InC χ r then (((S.Tc hχ hprim).basis k).repr x) ⟨r, h⟩ else 0

The coefficients of an element of the centralizer table.

theorem MultiplicativeBasisDeformations.RaySys.Sys.mem_range_incl {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (c : ↥(S.P.Lin k)) : c ∈ ((S.incl hχ hprim).alg k).range ↔ ∀ (r : R), ¬S.InC χ r → ((S.P.basis k).repr c) r = 0

The image of the centralizer table: coefficients vanish off the centralizer rays.

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

C_χ is the image of the centralizer table.

def MultiplicativeBasisDeformations.RaySys.Sys.aχ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (χ : L) : Ideal ↥(S.Cχ k χ)

𝔞_χ = {c ∈ C_χ : q̂c = 0}.

instance MultiplicativeBasisDeformations.RaySys.Sys.instIsTwoSidedSubtypeMatrixMemSubalgebraLinPCχAχ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (χ : L) : (S.aχ k χ).IsTwoSided

theorem MultiplicativeBasisDeformations.RaySys.Sys.mem_aχ_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (c : ↥(S.Cχ k χ)) : c ∈ S.aχ k χ ↔ ∀ (r : R), S.InQ χ r → ((S.P.basis k).repr ↑c) r = 0

𝔞_χ is spanned by the unshiftable nonidentity rays and the identities at q̂_x = 0: an element of C_χ lies in 𝔞_χ exactly when its coefficients at the rays of Q_χ vanish.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.eC {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) : ↥(S.Cχ k χ) ≃ₐ[k] ↥((S.Tc hχ hprim).Lin k)

The identification C_χ ≃ kT_c.

theorem MultiplicativeBasisDeformations.RaySys.Sys.incl_eC {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (c : ↥(S.Cχ k χ)) : ((S.incl hχ hprim).alg k) ((S.eC k hχ hprim) c) = ↑c

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

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

The quotient map C_χ → kQ_χ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.φχ_apply {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (c : ↥(S.Cχ k χ)) : (S.φχ k hχ hprim) c = (S.proj hχ hprim k) ↑c

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

theorem MultiplicativeBasisDeformations.RaySys.Sys.proj_eq_zero_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (c : ↥(S.P.Lin k)) : (S.proj hχ hprim k) c = 0 ↔ ∀ (r : R), S.InQ χ r → ((S.P.basis k).repr c) r = 0

π(c) = 0 exactly when the coefficients of c at the rays of Q_χ vanish.

theorem MultiplicativeBasisDeformations.RaySys.Sys.aχ_eq_ker {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) : S.aχ k χ = RingHom.ker (S.φχ k hχ hprim)

𝔞_χ is the kernel of C_χ → kQ_χ.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Sys.Bχ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (χ : L) : Type u

B_χ = C_χ/𝔞_χ.

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

B_χ ≅ kQ_χ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.Bχ_equiv_mk {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (c : ↥(S.Cχ k χ)) : (S.Bχ_equiv k hχ hprim) ((Ideal.Quotient.mk (S.aχ k χ)) c) = (S.proj hχ hprim k) ↑c

theorem MultiplicativeBasisDeformations.RaySys.Sys.b_mem_Cχ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r : R} (h : S.InC χ r) : S.P.b k r ∈ S.Cχ k χ

theorem MultiplicativeBasisDeformations.RaySys.Sys.Bχ_equiv_b {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r : R} (h : S.InQ χ r) : (S.Bχ_equiv k hχ hprim) ((Ideal.Quotient.mk (S.aχ k χ)) ⟨S.P.b k r, ⋯⟩) = (S.Qχ hχ hprim).b k ⟨r, h⟩

The class in B_χ of a ray of Q_χ is its basis vector of kQ_χ.

instance MultiplicativeBasisDeformations.RaySys.Sys.instFiniteDimensionalSubtypeMatrixMemSubalgebraLinPCχ {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (χ : L) : FiniteDimensional k ↥(S.Cχ k χ)

instance MultiplicativeBasisDeformations.RaySys.Sys.instFiniteDimensionalBχ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (k : Type u) [Field k] (χ : L) : FiniteDimensional k (S.Bχ k χ)

theorem MultiplicativeBasisDeformations.RaySys.Sys.centralizerRayAlgebra {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] (hχ : 0 < S.P.deg χ) (hprim : Prim χ) [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) : IsBasicAlgebra (S.Bχ k χ) ∧ IsRepresentationFinite k (S.Bχ k χ) ∧ (∃ (e : S.Bχ k χ ≃ₐ[k] ↥((S.Qχ hχ hprim).Lin k)), ∀ (r : R) (h : S.InQ χ r), e ((Ideal.Quotient.mk (S.aχ k χ)) ⟨S.P.b k r, ⋯⟩) = (S.Qχ hχ hprim).b k ⟨r, h⟩) ∧ (Nontrivial (S.Bχ k χ) → Fintype.card { r : R // (S.qData hχ hprim).pR r } < Fintype.card R)

Lemma 9.2 (lem:centralizer-ray-algebra), as stated: B_χ = C_χ/𝔞_χ is basic and representation-finite; the classes of the supporting identities and the two-sided rays form a basis, whose products are those of the table Q_χ (B_χ ≅ kQ_χ, the class of a ray going to its basis vector); Q_χ has fewer rays than P when B_χ ≠ 0. Here C_χ = Cent_{A₀}(q̂) and 𝔞_χ = {c ∈ C_χ : q̂c = 0}.