Lemma 8.11, Case 2 and the statement

Case 2 of lem:opposite-controls (local-ray-geometry.tex): fg = 0 with f q², q² g ≠ 0 is excluded by the seven-object category with arrows u → c → d, u → u', l → c → r, l_d → d and the relation l → c → r = 0 (dimensions 3 at c, 2 at u, d, 1 elsewhere: N = 22, D = 21, F = 1). Indices 0..6 are u' u c d l r l_d.

def MultiplicativeBasisDeformations.RaySys.Sys.t7 : Fin 7 → Fin 7 → Bool

The table of the seven-object category.

instance MultiplicativeBasisDeformations.RaySys.Sys.instFactAxT7 : Fact (PosetRep.Ax t7)

theorem MultiplicativeBasisDeformations.RaySys.Sys.t7_uniq : PosetRep.UniqOK t7

theorem MultiplicativeBasisDeformations.RaySys.Sys.t7_count : ∑ i : Fin (Nat.succ 6), ![1, 2, 3, 2, 1, 1, 1] i ^ 2 + ![1, 2, 3, 2, 1, 1, 1] 5 * ![1, 2, 3, 2, 1, 1, 1] 4 ≤ ∑ i : Fin 7, ∑ j : Fin 7, if PosetRep.covB t7 i j = true then ![1, 2, 3, 2, 1, 1, 1] i * ![1, 2, 3, 2, 1, 1, 1] j else 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.t7_cov42 : PosetRep.covB t7 4 2 = true

theorem MultiplicativeBasisDeformations.RaySys.Sys.t7_cov25 : PosetRep.covB t7 2 5 = true

def MultiplicativeBasisDeformations.RaySys.Sys.c2V {V : Type} (b c a : V) : Fin 7 → V

The objects.

def MultiplicativeBasisDeformations.RaySys.Sys.c2G {V R L : Type} [AddCommGroup L] (S : Sys V R L) (f g q0 : R) : Fin 7 → L

The weights.

def MultiplicativeBasisDeformations.RaySys.Sys.c2ρ {V R L : Type} [AddCommGroup L] (S : Sys V R L) (b c a : V) (f g q0 fq q2 qg : R) : Fin 7 → Fin 7 → R

The rays.

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_src {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (f1 : S.P.src f = b) (g1 : S.P.src g = c) (q01 : S.P.src q0 = c) (hfq : S.P.mul f q0 = some fq) (hq2 : S.P.mul q0 q0 = some q2) (hqg : S.P.mul q0 g = some qg) (i j : Fin 7) : t7 i j = true → ¬Tab.ZT t7 4 5 i j → S.P.src (S.c2ρ b c a f g q0 fq q2 qg i j) = c2V b c a i

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_tgt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (f2 : S.P.tgt f = c) (g2 : S.P.tgt g = a) (q02 : S.P.tgt q0 = c) (hfq : S.P.mul f q0 = some fq) (hq2 : S.P.mul q0 q0 = some q2) (hqg : S.P.mul q0 g = some qg) (i j : Fin 7) : t7 i j = true → ¬Tab.ZT t7 4 5 i j → S.P.tgt (S.c2ρ b c a f g q0 fq q2 qg i j) = c2V b c a j

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_wt {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (hfq : S.P.mul f q0 = some fq) (hq2 : S.P.mul q0 q0 = some q2) (hqg : S.P.mul q0 g = some qg) (i j : Fin 7) : t7 i j = true → ¬Tab.ZT t7 4 5 i j → S.P.wt (S.c2ρ b c a f g q0 fq q2 qg i j) = S.c2G f g q0 j - S.c2G f g q0 i

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (i : Fin 7) : S.c2ρ b c a f g q0 fq q2 qg i i = S.P.e (c2V b c a i)

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (hfq : S.P.mul f q0 = some fq) (hq2 : S.P.mul q0 q0 = some q2) (hqg : S.P.mul q0 g = some qg) (i j l : Fin 7) : t7 i j = true → t7 j l = true → i ≠ j → j ≠ l → ¬Tab.ZT t7 4 5 i l → S.P.mul (S.c2ρ b c a f g q0 fq q2 qg i j) (S.c2ρ b c a f g q0 fq q2 qg j l) = some (S.c2ρ b c a f g q0 fq q2 qg i l)

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_mulZ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (hfg : S.P.mul f g = none) (i j l : Fin 7) : t7 i j = true → t7 j l = true → ¬Tab.ZT t7 4 5 i j → ¬Tab.ZT t7 4 5 j l → Tab.ZT t7 4 5 i l → S.P.mul (S.c2ρ b c a f g q0 fq q2 qg i j) (S.c2ρ b c a f g q0 fq q2 qg j l) = none

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_retL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (hdf : 0 < S.P.deg (S.P.wt f)) (hdg : 0 < S.P.deg (S.P.wt g)) (hdq : 0 < S.P.deg (S.P.wt q0)) (X1 : ∀ (h : R), S.P.src h = a → S.P.tgt h = c → S.P.mul g h ≠ some q0) (X2 : ∀ (h : R), S.P.src h = a → S.P.tgt h = c → S.P.mul g h ≠ some q2) (X3 : ∀ (h : R), S.P.src h = a → S.P.tgt h = a → S.P.mul g h ≠ some qg) (X4 : ∀ (h : R), S.P.src h = c → S.P.tgt h = a → S.P.mul q0 h ≠ some g) (X5 : ∀ (h : R), S.P.src h = c → S.P.tgt h = b → S.P.mul h f ≠ some q0) (X6 : ∀ (h : R), S.P.src h = c → S.P.tgt h = b → S.P.mul h f ≠ some q2) (X7 : ∀ (h : R), S.P.src h = b → S.P.tgt h = b → S.P.mul h f ≠ some fq) (X8 : ∀ (h : R), S.P.src h = b → S.P.tgt h = c → S.P.mul h q0 ≠ some f) (i j l : Fin 7) (h : R) : PosetRep.covB t7 i j = true → t7 i l = true → ¬Tab.ZT t7 4 5 i l → S.P.src h = c2V b c a j → S.P.tgt h = c2V b c a l → S.P.wt h = S.c2G f g q0 l - S.c2G f g q0 j → S.P.mul (S.c2ρ b c a f g q0 fq q2 qg i j) h = some (S.c2ρ b c a f g q0 fq q2 qg i l) → t7 j l = true

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_retR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (hdf : 0 < S.P.deg (S.P.wt f)) (hdg : 0 < S.P.deg (S.P.wt g)) (hdq : 0 < S.P.deg (S.P.wt q0)) (X1 : ∀ (h : R), S.P.src h = a → S.P.tgt h = c → S.P.mul g h ≠ some q0) (X2 : ∀ (h : R), S.P.src h = a → S.P.tgt h = c → S.P.mul g h ≠ some q2) (X3 : ∀ (h : R), S.P.src h = a → S.P.tgt h = a → S.P.mul g h ≠ some qg) (X4 : ∀ (h : R), S.P.src h = c → S.P.tgt h = a → S.P.mul q0 h ≠ some g) (X5 : ∀ (h : R), S.P.src h = c → S.P.tgt h = b → S.P.mul h f ≠ some q0) (X6 : ∀ (h : R), S.P.src h = c → S.P.tgt h = b → S.P.mul h f ≠ some q2) (X7 : ∀ (h : R), S.P.src h = b → S.P.tgt h = b → S.P.mul h f ≠ some fq) (X8 : ∀ (h : R), S.P.src h = b → S.P.tgt h = c → S.P.mul h q0 ≠ some f) (i j l : Fin 7) (h : R) : PosetRep.covB t7 i j = true → t7 l j = true → ¬Tab.ZT t7 4 5 l j → S.P.src h = c2V b c a l → S.P.tgt h = c2V b c a i → S.P.wt h = S.c2G f g q0 i - S.c2G f g q0 l → S.P.mul h (S.c2ρ b c a f g q0 fq q2 qg i j) = some (S.c2ρ b c a f g q0 fq q2 qg l j) → t7 l i = true

theorem MultiplicativeBasisDeformations.RaySys.Sys.c2_false {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {b c a : V} {f g q0 fq q2 qg : R} (f1 : S.P.src f = b) (f2 : S.P.tgt f = c) (g1 : S.P.src g = c) (g2 : S.P.tgt g = a) (q01 : S.P.src q0 = c) (q02 : S.P.tgt q0 = c) (hfq : S.P.mul f q0 = some fq) (hq2 : S.P.mul q0 q0 = some q2) (hqg : S.P.mul q0 g = some qg) (hfg : S.P.mul f g = none) (hdf : 0 < S.P.deg (S.P.wt f)) (hdg : 0 < S.P.deg (S.P.wt g)) (hdq : 0 < S.P.deg (S.P.wt q0)) (X1 : ∀ (h : R), S.P.src h = a → S.P.tgt h = c → S.P.mul g h ≠ some q0) (X2 : ∀ (h : R), S.P.src h = a → S.P.tgt h = c → S.P.mul g h ≠ some q2) (X3 : ∀ (h : R), S.P.src h = a → S.P.tgt h = a → S.P.mul g h ≠ some qg) (X4 : ∀ (h : R), S.P.src h = c → S.P.tgt h = a → S.P.mul q0 h ≠ some g) (X5 : ∀ (h : R), S.P.src h = c → S.P.tgt h = b → S.P.mul h f ≠ some q0) (X6 : ∀ (h : R), S.P.src h = c → S.P.tgt h = b → S.P.mul h f ≠ some q2) (X7 : ∀ (h : R), S.P.src h = b → S.P.tgt h = b → S.P.mul h f ≠ some fq) (X8 : ∀ (h : R), S.P.src h = b → S.P.tgt h = c → S.P.mul h q0 ≠ some f) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) : False

The seven-object category of Case 2 is excluded.

theorem MultiplicativeBasisDeformations.RaySys.Sys.rad_tgt_pow_mul_of_cycL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {g : R} (hgL : S.CycL g) (hgR : ¬S.CycR g) (j : ℕ) (hj : 1 ≤ j) : S.rr g * S.q (S.P.tgt g) ^ j = 0 ∨ ∃ (m : ℕ), 2 ≤ m ∧ S.rr g * S.q (S.P.tgt g) ^ j = S.q (S.P.src g) ^ m * S.rr g

g q_a^j ∈ R_c q² g for j ≥ 1.

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_one_of_qpow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {q0 : R} (hq0 : S.q x = S.rr q0) (hdq : 0 < S.P.deg (S.P.wt q0)) {m : ℕ} {t : R} (ht : S.rr t = S.q x ^ m * S.rr (S.P.e x)) (ht' : S.P.wt t = S.P.wt q0) : m = 1

A loop equal to q^m e and to q forces m = 1.

theorem MultiplicativeBasisDeformations.RaySys.Sys.opposite_controls {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)) {f g : R} (hfR : S.CycR f) (hfL : ¬S.CycL f) (hgL : S.CycL g) (hgR : ¬S.CycR g) (hfg : S.P.tgt f = S.P.src g) : S.rr f * S.q (S.P.tgt f) ^ 2 = 0 ∨ S.q (S.P.tgt f) ^ 2 * S.rr g = 0

Lemma 8.11(1) (lem:opposite-controls): for generating f : b → c, g : c → a whose Homs are cyclic at c but not at the other endpoints, f q² = 0 or q² g = 0.

theorem MultiplicativeBasisDeformations.RaySys.Sys.opposite_controls_high {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)) {f g : R} (hfR : S.CycR f) (hfL : ¬S.CycL f) (hgL : S.CycL g) (hgR : ¬S.CycR g) (hfg : S.P.tgt f = S.P.src g) (n : ℕ) (hn : 2 ≤ n) : S.rr f * S.q (S.P.tgt f) ^ n * S.rr g = 0

Lemma 8.11(2), first part: f q^n g = 0 for n ≥ 2.

theorem MultiplicativeBasisDeformations.RaySys.Sys.opposite_controls_src {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)) {f g : R} (hfR : S.CycR f) (hfL : ¬S.CycL f) (hgL : S.CycL g) (hgR : ¬S.CycR g) (hfg : S.P.tgt f = S.P.src g) (n : ℕ) : S.q (S.P.src f) * (S.rr f * S.q (S.P.tgt f) ^ n * S.rr g) = 0

Lemma 8.11(2), socle part: the source radical kills f q^n g.

theorem MultiplicativeBasisDeformations.RaySys.Sys.opposite_controls_tgt {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)) {f g : R} (hfR : S.CycR f) (hfL : ¬S.CycL f) (hgL : S.CycL g) (hgR : ¬S.CycR g) (hfg : S.P.tgt f = S.P.src g) (n : ℕ) : S.rr f * S.q (S.P.tgt f) ^ n * S.rr g * S.q (S.P.tgt g) = 0

Lemma 8.11(2), socle part: the target radical kills f q^n g.