Setting 8.4 from a representation-finite ray table

Setting 8.4 (local-ray-geometry.tex) for a finite ray table P with representation-finite linearization: "Write R_x = k[q_x]/(q_x^{N_x}) when R_x ≠ k, choosing q_x as its homogeneous radical generator", with the endpoint chains of Lemma 3.1(3). The identity vectors of kP are a complete set of primitive orthogonal idempotents; the corners are spanned by rays, and the corner radicals by the local rays of positive degree. By Lemma 3.1(3) (exists_rad_gen) at most one positive local ray at x is not a product of two positive local rays; it generates all local rays (q_x). Every Hom is cyclic over one endpoint (endpointSpan_one_sided) and its endpoint subbimodules form a chain (isChain_subbimodules), which gives the fields cyc and chain of Sys.

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_e_complete {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] : CompleteOrthogonalIdempotents fun (x : V) => P.b k (P.e x)

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_e_primitive {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (x : V) : IsPrimitiveIdempotent (P.b k (P.e x))

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.linIdem {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] : PrimitiveIdempotents ↥(P.Lin k)

The identity vectors of kP as primitive idempotents.

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.linIdx {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] : V ≃ Fin (P.linIdem k).m

Vertices as indices of the identity vectors.

theorem MultiplicativeBasisDeformations.RaySys.Tab.linIdem_e {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (x : V) : (P.linIdem k).e ((P.linIdx k) x) = P.b k (P.e x)

theorem MultiplicativeBasisDeformations.RaySys.Tab.linIdem_e' {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (i : Fin (P.linIdem k).m) : (P.linIdem k).e i = P.b k (P.e ((P.linIdx k).symm i))

theorem MultiplicativeBasisDeformations.RaySys.Tab.corner_eq {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (x y : V) : (P.linIdem k).corner ((P.linIdx k) x) ((P.linIdx k) y) = P.corSp k x y

theorem MultiplicativeBasisDeformations.RaySys.Tab.degSp_le_radical {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] : P.degSp k 1 ≤ algebraRadical k ↥(P.Lin k)

Rays of positive degree span a two-sided ideal contained in the radical.

theorem MultiplicativeBasisDeformations.RaySys.Tab.cornerRadical_eq {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (x : V) : (P.linIdem k).cornerRadical ((P.linIdx k) x) = P.corSp k x x ⊓ P.degSp k 1

Elements of the ray monoid as vectors

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.vecT {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] (a : M P.toMult) : ↥(P.Lin k)

The vector of a ray, and zero.

theorem MultiplicativeBasisDeformations.RaySys.Tab.vecT_rr {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (r : R) : P.vecT k (P.rr r) = P.b k r

theorem MultiplicativeBasisDeformations.RaySys.Tab.vecT_zero {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] : P.vecT k 0 = 0

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_mul_b' {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (u v : R) : P.b k u * P.b k v = P.vecT k (P.rr u * P.rr v)

theorem MultiplicativeBasisDeformations.RaySys.Tab.vecT_mul_b {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (w : R) {a : M P.toMult} (ha : a = 0 ∨ ∃ (u : R), a = P.rr u) : P.vecT k a * P.b k w = P.vecT k (a * P.rr w)

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_mul_vecT {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (u : R) {a : M P.toMult} (ha : a = 0 ∨ ∃ (w : R), a = P.rr w) : P.b k u * P.vecT k a = P.vecT k (P.rr u * a)

theorem MultiplicativeBasisDeformations.RaySys.Tab.rr_mul_rr_cases' {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (u v : R) : P.rr u * P.rr v = 0 ∨ ∃ (t : R), P.rr u * P.rr v = P.rr t

theorem MultiplicativeBasisDeformations.RaySys.Tab.mul_rr_cases {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {a : M P.toMult} (ha : a = 0 ∨ ∃ (u : R), a = P.rr u) (v : R) : a * P.rr v = 0 ∨ ∃ (t : R), a * P.rr v = P.rr t

theorem MultiplicativeBasisDeformations.RaySys.Tab.rr_mul_cases {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (u : R) {a : M P.toMult} (ha : a = 0 ∨ ∃ (v : R), a = P.rr v) : P.rr u * a = 0 ∨ ∃ (t : R), P.rr u * a = P.rr t

The local generator

def MultiplicativeBasisDeformations.RaySys.Tab.PosL {V R L : Type} [AddCommGroup L] (P : Tab V R L) (x : V) : Set R

Local rays of positive degree at x.

def MultiplicativeBasisDeformations.RaySys.Tab.ProdL {V R L : Type} [AddCommGroup L] (P : Tab V R L) (x : V) : Set R

Positive local rays which are products of two positive local rays.

def MultiplicativeBasisDeformations.RaySys.Tab.GenL {V R L : Type} [AddCommGroup L] (P : Tab V R L) (x : V) : Set R

Positive local rays which are not such products.

theorem MultiplicativeBasisDeformations.RaySys.Tab.posL_deg {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x : V} {l : R} (hl : l ∈ P.PosL x) : 1 ≤ P.deg (P.wt l)

theorem MultiplicativeBasisDeformations.RaySys.Tab.corRad_span {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (x : V) : P.corSp k x x ⊓ P.degSp k 1 = Submodule.span k (⇑(P.basis k) '' P.PosL x)

theorem MultiplicativeBasisDeformations.RaySys.Tab.corRad_sq_le {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (x : V) : (P.corSp k x x ⊓ P.degSp k 1) * (P.corSp k x x ⊓ P.degSp k 1) ≤ Submodule.span k (⇑(P.basis k) '' P.ProdL x)

theorem MultiplicativeBasisDeformations.RaySys.Tab.repr_eq_zero_of_mem_span {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] {T : Set R} {a : ↥(P.Lin k)} (ha : a ∈ Submodule.span k (⇑(P.basis k) '' T)) {r : R} (hr : r ∉ T) : ((P.basis k).repr a) r = 0

theorem MultiplicativeBasisDeformations.RaySys.Tab.genL_unique {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) {x : V} {g g' : R} (hg : g ∈ P.GenL x) (hg' : g' ∈ P.GenL x) : g = g'

At most one positive local ray is not a product (dim rad/rad² ≤ 1, Lemma 3.1(3)).

theorem MultiplicativeBasisDeformations.RaySys.Tab.genL_exists {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {x : V} (h : (P.PosL x).Nonempty) : ∃ (g : R), g ∈ P.GenL x

theorem MultiplicativeBasisDeformations.RaySys.Tab.posL_eq_pow {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) {x : V} {g : R} (hg : g ∈ P.GenL x) (l : R) : l ∈ P.PosL x → ∃ (j : ℕ), 1 ≤ j ∧ P.rr l = P.rr g ^ j

Every positive local ray is a power of the generator.

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.qT {V R L : Type} [AddCommGroup L] [Fintype R] (P : Tab V R L) (x : V) : M P.toMult

The local generator q_x (zero when R_x = k).

theorem MultiplicativeBasisDeformations.RaySys.Tab.qT_cases {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (x : V) : P.qT x = 0 ∨ ∃ (g : R), P.qT x = P.rr g ∧ P.src g = x ∧ P.tgt g = x ∧ g ≠ P.e x

theorem MultiplicativeBasisDeformations.RaySys.Tab.qT_mul_e {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (x : V) : P.qT x * P.rr (P.e x) = P.qT x

theorem MultiplicativeBasisDeformations.RaySys.Tab.e_mul_qT {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (x : V) : P.rr (P.e x) * P.qT x = P.qT x

theorem MultiplicativeBasisDeformations.RaySys.Tab.qTpow_comm_e {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (x : V) (j : ℕ) : P.qT x ^ j * P.rr (P.e x) = P.rr (P.e x) * P.qT x ^ j

theorem MultiplicativeBasisDeformations.RaySys.Tab.qT_pow {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) (r : R) (h : P.src r = P.tgt r) : ∃ (j : ℕ), P.qT (P.src r) ^ j * P.rr (P.e (P.src r)) = P.rr r

theorem MultiplicativeBasisDeformations.RaySys.Tab.qTpow_e_cases {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (x : V) (j : ℕ) : P.qT x ^ j * P.rr (P.e x) = 0 ∨ ∃ (l : R), P.qT x ^ j * P.rr (P.e x) = P.rr l ∧ P.src l = x ∧ P.tgt l = x

Local powers of the generator are local rays or zero.

theorem MultiplicativeBasisDeformations.RaySys.Tab.zero_ne_one_M {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) : 0 ≠ 1

theorem MultiplicativeBasisDeformations.RaySys.Tab.mul_rr_mul_ne_one {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (a b : M P.toMult) (r : R) : a * P.rr r * b ≠ 1

theorem MultiplicativeBasisDeformations.RaySys.Tab.eq_rr_of_ne_zero {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) {a b : M P.toMult} {r : R} (h : a * P.rr r * b ≠ 0) : ∃ (t : R), a * P.rr r * b = P.rr t

theorem MultiplicativeBasisDeformations.RaySys.Tab.local_eq_qTpow {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) {l : R} {x : V} (h1 : P.src l = x) (h2 : P.tgt l = x) : ∃ (j : ℕ), P.rr l = P.qT x ^ j * P.rr (P.e x)

A local ray is a local power of the generator times the identity.

theorem MultiplicativeBasisDeformations.RaySys.Tab.both_span {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) (r : R) {a c : ↥(P.Lin k)} (ha : a ∈ P.corSp k (P.src r) (P.src r)) (hc : c ∈ P.corSp k (P.tgt r) (P.tgt r)) : a * P.b k r * c ∈ Submodule.span k (⇑(P.basis k) '' {s : R | ∃ (i : ℕ) (j : ℕ), P.rr s = P.qT (P.src r) ^ i * P.rr r * P.qT (P.tgt r) ^ j})

theorem MultiplicativeBasisDeformations.RaySys.Tab.mem_of_b_mem_span {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] {T : Set R} {r : R} (h : P.b k r ∈ Submodule.span k (⇑(P.basis k) '' T)) : r ∈ T

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_mem_corner {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (r : R) : P.b k r ∈ (P.linIdem k).corner ((P.linIdx k) (P.src r)) ((P.linIdx k) (P.tgt r))

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_mem_endpointSpan {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) {r t : R} {i j : ℕ} (ht : P.rr t = P.qT (P.src r) ^ i * P.rr r * P.qT (P.tgt r) ^ j) : P.b k t ∈ (P.linIdem k).endpointSpan ((P.linIdx k) (P.src r)) ((P.linIdx k) (P.tgt r)) (P.b k r)

theorem MultiplicativeBasisDeformations.RaySys.Tab.left_span {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) (r : R) {a : ↥(P.Lin k)} (ha : a ∈ P.corSp k (P.src r) (P.src r)) : a * P.b k r ∈ Submodule.span k (⇑(P.basis k) '' {s : R | ∃ (i : ℕ), P.rr s = P.qT (P.src r) ^ i * P.rr r})

theorem MultiplicativeBasisDeformations.RaySys.Tab.right_span {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) (r : R) {c : ↥(P.Lin k)} (hc : c ∈ P.corSp k (P.tgt r) (P.tgt r)) : P.b k r * c ∈ Submodule.span k (⇑(P.basis k) '' {s : R | ∃ (j : ℕ), P.rr s = P.rr r * P.qT (P.tgt r) ^ j})

theorem MultiplicativeBasisDeformations.RaySys.Tab.cycT {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) (r : R) : (∀ (i j : ℕ), P.qT (P.src r) ^ i * P.rr r * P.qT (P.tgt r) ^ j ≠ 0 → ∃ (i' : ℕ), P.qT (P.src r) ^ i * P.rr r * P.qT (P.tgt r) ^ j = P.qT (P.src r) ^ i' * P.rr r) ∨ ∀ (i j : ℕ), P.qT (P.src r) ^ i * P.rr r * P.qT (P.tgt r) ^ j ≠ 0 → ∃ (j' : ℕ), P.qT (P.src r) ^ i * P.rr r * P.qT (P.tgt r) ^ j = P.rr r * P.qT (P.tgt r) ^ j'

theorem MultiplicativeBasisDeformations.RaySys.Tab.endpointSpan_le_both {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) (s : R) : (P.linIdem k).endpointSpan ((P.linIdx k) (P.src s)) ((P.linIdx k) (P.tgt s)) (P.b k s) ≤ Submodule.span k (⇑(P.basis k) '' {t : R | ∃ (i : ℕ) (j : ℕ), P.rr t = P.qT (P.src s) ^ i * P.rr s * P.qT (P.tgt s) ^ j})

theorem MultiplicativeBasisDeformations.RaySys.Tab.chainT {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) (r s : R) (h1 : P.src r = P.src s) (h2 : P.tgt r = P.tgt s) : (∃ (i : ℕ) (j : ℕ), P.rr r = P.qT (P.src r) ^ i * P.rr s * P.qT (P.tgt r) ^ j) ∨ ∃ (i : ℕ) (j : ℕ), P.rr s = P.qT (P.src r) ^ i * P.rr r * P.qT (P.tgt r) ^ j

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.toSys {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) : Sys V R L

Setting 8.4 for a representation-finite ray table.

theorem MultiplicativeBasisDeformations.RaySys.Tab.toSys_P {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(P.Lin k)) : (P.toSys k hfin).P = P