Tables for the dimension induction

Support for the strong induction of Proposition 8.3 (main-theorems.tex: "disconnected algebras reduce to their connected factors"; Lemma 9.2: "W(Q_χ) is free by the dimension induction … applied to each connected factor"):

• a ray table splits along a union of components into two tables with fewer rays, each with representation-finite linearization (a quotient of kT), and weight lifting holds for T when it holds for both pieces (lift2_of_split);
• a representation-finite ray table presents its own linearization (self_rayPres), which is basic.

structure MultiplicativeBasisDeformations.RaySys.Tab.Closed {V R L : Type} [AddCommGroup L] (P : Tab V R L) (C : V → Prop) : Prop

A set of vertices closed under rays (a union of components).

• fwd (r : R) : C (P.src r) → C (P.tgt r)
• bwd (r : R) : C (P.tgt r) → C (P.src r)

def MultiplicativeBasisDeformations.RaySys.Tab.compData {V R L : Type} [AddCommGroup L] {P : Tab V R L} {C : V → Prop} (hC : P.Closed C) : P.SubData

The sub-table on a union of components.

theorem MultiplicativeBasisDeformations.RaySys.Tab.compMul_eq_some {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {C : V → Prop} (hC : P.Closed C) {r s t : { r : R // C (P.src r) }} : (sub (compData hC)).mul r s = some t ↔ P.mul ↑r ↑s = some ↑t

theorem MultiplicativeBasisDeformations.RaySys.Tab.Closed.compl {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {C : V → Prop} (hC : P.Closed C) : P.Closed fun (x : V) => ¬C x

The complement of a union of components is one.

theorem MultiplicativeBasisDeformations.RaySys.Tab.lift2_of_split {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {C : V → Prop} (hC : P.Closed C) (h1 : (sub (compData hC)).Lift2) (h2 : (sub (compData ⋯)).Lift2) : P.Lift2

Weight lifting for a table split into two unions of components.

noncomputable def MultiplicativeBasisDeformations.RaySys.Tab.compMor {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {C : V → Prop} (hC : P.Closed C) : Mor P.toMult (sub (compData hC)).toMult

The quotient morphism kT → kT_C onto a union of components.

theorem MultiplicativeBasisDeformations.RaySys.Tab.comp_isRepresentationFinite {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {C : V → Prop} (hC : P.Closed C) (k : Type u) [Field k] (h : IsRepresentationFinite k ↥(P.Lin k)) : IsRepresentationFinite k ↥((sub (compData hC)).Lin k)

def MultiplicativeBasisDeformations.RaySys.Tab.Conn {V R L : Type} [AddCommGroup L] (P : Tab V R L) : Prop

A connected table: every two vertices are joined by a zigzag of rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.exists_split {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} (hnc : ¬P.Conn) : ∃ (C : V → Prop), P.Closed C ∧ (∃ (x : V), C x) ∧ ∃ (x : V), ¬C x

A disconnected table splits along a component.

theorem MultiplicativeBasisDeformations.RaySys.Tab.card_comp_lt {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] {P : Tab V R L} {C : V → Prop} (hx : ∃ (x : V), ¬C x) : Fintype.card { r : R // C (P.src r) } < Fintype.card R

A proper union of components has fewer rays.

The linearization of a representation-finite table

theorem MultiplicativeBasisDeformations.RaySys.Tab.isBasic_lin {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] : IsBasicAlgebra ↥(P.Lin k)

The linearization of a ray table is basic.

theorem MultiplicativeBasisDeformations.RaySys.Sys.coch_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] [IsAlgClosed k] : S.coch k 0 = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.self_hΨ {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] [IsAlgClosed k] (a z : ↥(S.P.Lin k)) : (LinearEquiv.refl k ↥(S.P.Lin k)) (a * z + ((S.coch k 0) a) z) = (LinearEquiv.refl k ↥(S.P.Lin k)) a * (LinearEquiv.refl k ↥(S.P.Lin k)) z

theorem MultiplicativeBasisDeformations.RaySys.Sys.self_rayPres {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] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) : (S.fibreIdem k hfin 0 (LinearEquiv.refl k ↥(S.P.Lin k)) ⋯).IsRayPres S.P.toMult (S.fibreIdx k hfin 0 (LinearEquiv.refl k ↥(S.P.Lin k)) ⋯) (S.P.b k)

A representation-finite ray table presents its own linearization (Definition 3.9(3)).