Lemma 8.11: opposite controls

lem:opposite-controls (local-ray-geometry.tex): generating rays f : b → c and g : c → a whose Homs are cyclic at c but not at their other endpoints. Here: the setting, the inclusions (eq:opposite-control-inclusions)

(rad R_b) f ⊆ f q² R_c, A₀(c, b) f ⊆ (q²), and their duals for g,

and the four-leaf star of Case 1, which gives the strong star vanishing (eq:strong-star-vanishing, local-ray-restrictions.tex): if fq, qg, q² ≠ 0 then fg = 0.

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

A loop Hom is cyclic at its source, generated by the identity.

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_loop {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (hf : S.IsGen f) (h : S.P.src f = S.P.tgt f) : f = S.P.e (S.P.src f)

A generating loop is the identity.

theorem MultiplicativeBasisDeformations.RaySys.Sys.src_ne_tgt_of_cycR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (hfR : S.CycR f) (hfL : ¬S.CycL f) : S.P.src f ≠ S.P.tgt f

The two endpoints of a ray generated only at its target differ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.mul_q_ne_of_cycR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (hfR : S.CycR f) (hfL : ¬S.CycL f) : S.rr f * S.q (S.P.tgt f) ≠ 0

A ray generated only at its target has f q ≠ 0.

theorem MultiplicativeBasisDeformations.RaySys.Sys.rad_src_mul_of_cycR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (hfR : S.CycR f) (hfL : ¬S.CycL f) : S.q (S.P.src f) * S.rr f = 0 ∨ ∃ (m : ℕ), 2 ≤ m ∧ S.q (S.P.src f) * S.rr f = S.rr f * S.q (S.P.tgt f) ^ m

(rad R_b) f ⊆ f q² R_c (first inclusion of eq:opposite-control-inclusions).

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

Powers of the source radical: q_b^j f ∈ f q² R_c for j ≥ 1.

theorem MultiplicativeBasisDeformations.RaySys.Sys.rev_mul_of_cycR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (hfR : S.CycR f) (hfL : ¬S.CycL f) (h : R) (hh : S.rr h * S.rr f ≠ 0) (hsrc : S.P.src h = S.P.tgt f) : ∃ (m : ℕ), 2 ≤ m ∧ S.rr h * S.rr f = S.q (S.P.tgt f) ^ m * S.rr (S.P.e (S.P.tgt f))

A₀(c, b) f ⊆ (q²) (second inclusion of eq:opposite-control-inclusions).

The dual statements for g

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_hyp_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) : S.op.CycR g ∧ ¬S.op.CycL g

theorem MultiplicativeBasisDeformations.RaySys.Sys.src_ne_tgt_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) : S.P.src g ≠ S.P.tgt g

theorem MultiplicativeBasisDeformations.RaySys.Sys.q_mul_ne_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) : S.q (S.P.src g) * S.rr g ≠ 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.rad_tgt_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) : S.rr g * S.q (S.P.tgt g) = 0 ∨ ∃ (m : ℕ), 2 ≤ m ∧ S.rr g * S.q (S.P.tgt g) = S.q (S.P.src g) ^ m * S.rr g

g rad R_a ⊆ R_c q² g.

theorem MultiplicativeBasisDeformations.RaySys.Sys.rev_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) (h : R) (hh : S.rr g * S.rr h ≠ 0) (htgt : S.P.tgt h = S.P.src g) : ∃ (m : ℕ), 2 ≤ m ∧ S.rr g * S.rr h = S.q (S.P.src g) ^ m * S.rr (S.P.e (S.P.src g))

g A₀(a, c) ⊆ (q²).

The four-leaf star

def MultiplicativeBasisDeformations.RaySys.Sys.tStar : Fin 5 → Fin 5 → Bool

The table of the four-leaf star l, u → c → r, d (indices 0..4 are l u c r d).

instance MultiplicativeBasisDeformations.RaySys.Sys.instFactAxTStar : Fact (PosetRep.Ax tStar)

theorem MultiplicativeBasisDeformations.RaySys.Sys.tStar_uniq : PosetRep.UniqOK tStar

theorem MultiplicativeBasisDeformations.RaySys.Sys.tStar_count : PosetRep.CountOK tStar ![1, 1, 2, 1, 1]

theorem MultiplicativeBasisDeformations.RaySys.Sys.no_neg {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {h : R} {X : L} (hw : S.P.wt h = -X) (hX : 0 < S.P.deg X) : False

A ray of negative degree does not exist.

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

The objects of the star.

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

The weights of the star.

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

The rays of the star.

theorem MultiplicativeBasisDeformations.RaySys.Sys.star_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 fg fq qg q2 : R} (f1 : S.P.src f = b) (g1 : S.P.src g = c) (q01 : S.P.src q0 = c) (hfg : S.P.mul f g = some fg) (hfq : S.P.mul f q0 = some fq) (hqg : S.P.mul q0 g = some qg) (hq2 : S.P.mul q0 q0 = some q2) (i j : Fin 5) : tStar i j = true → S.P.src (S.starρ b c a f g q0 fg fq qg q2 i j) = starV b c a i

theorem MultiplicativeBasisDeformations.RaySys.Sys.star_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 fg fq qg q2 : R} (f2 : S.P.tgt f = c) (g2 : S.P.tgt g = a) (q02 : S.P.tgt q0 = c) (hfg : S.P.mul f g = some fg) (hfq : S.P.mul f q0 = some fq) (hqg : S.P.mul q0 g = some qg) (hq2 : S.P.mul q0 q0 = some q2) (i j : Fin 5) : tStar i j = true → S.P.tgt (S.starρ b c a f g q0 fg fq qg q2 i j) = starV b c a j

theorem MultiplicativeBasisDeformations.RaySys.Sys.star_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 fg fq qg q2 : R} (hfg : S.P.mul f g = some fg) (hfq : S.P.mul f q0 = some fq) (hqg : S.P.mul q0 g = some qg) (hq2 : S.P.mul q0 q0 = some q2) (i j : Fin 5) : tStar i j = true → S.P.wt (S.starρ b c a f g q0 fg fq qg q2 i j) = S.starG f g q0 j - S.starG f g q0 i

theorem MultiplicativeBasisDeformations.RaySys.Sys.star_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 fg fq qg q2 : R} (i : Fin 5) : S.starρ b c a f g q0 fg fq qg q2 i i = S.P.e (starV b c a i)

theorem MultiplicativeBasisDeformations.RaySys.Sys.star_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 fg fq qg q2 : R} (hfg : S.P.mul f g = some fg) (hfq : S.P.mul f q0 = some fq) (hqg : S.P.mul q0 g = some qg) (hq2 : S.P.mul q0 q0 = some q2) (i j l : Fin 5) : tStar i j = true → tStar j l = true → i ≠ j → j ≠ l → S.P.mul (S.starρ b c a f g q0 fg fq qg q2 i j) (S.starρ b c a f g q0 fg fq qg q2 j l) = some (S.starρ b c a f g q0 fg fq qg q2 i l)

theorem MultiplicativeBasisDeformations.RaySys.Sys.star_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 fg fq qg q2 : 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)) (R1 : ∀ (h : R), S.P.src h = a → S.P.tgt h = c → S.P.wt h = S.P.wt q0 - S.P.wt g → S.P.mul g h ≠ some q0) (R2 : ∀ (h : R), S.P.src h = c → S.P.tgt h = a → S.P.wt h = S.P.wt g - S.P.wt q0 → S.P.mul q0 h ≠ some g) (i j l : Fin 5) (h : R) : PosetRep.covB tStar i j = true → tStar i l = true → S.P.src h = starV b c a j → S.P.tgt h = starV b c a l → S.P.wt h = S.starG f g q0 l - S.starG f g q0 j → S.P.mul (S.starρ b c a f g q0 fg fq qg q2 i j) h = some (S.starρ b c a f g q0 fg fq qg q2 i l) → tStar j l = true

theorem MultiplicativeBasisDeformations.RaySys.Sys.star_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 fg fq qg q2 : 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)) (R3 : ∀ (h : R), S.P.src h = c → S.P.tgt h = b → S.P.wt h = -S.P.wt f + S.P.wt q0 → S.P.mul h f ≠ some q0) (R4 : ∀ (h : R), S.P.src h = b → S.P.tgt h = c → S.P.wt h = -S.P.wt q0 + S.P.wt f → S.P.mul h q0 ≠ some f) (i j l : Fin 5) (h : R) : PosetRep.covB tStar i j = true → tStar l j = true → S.P.src h = starV b c a l → S.P.tgt h = starV b c a i → S.P.wt h = S.starG f g q0 i - S.starG f g q0 l → S.P.mul h (S.starρ b c a f g q0 fg fq qg q2 i j) = some (S.starρ b c a f g q0 fg fq qg q2 l j) → tStar l i = true

theorem MultiplicativeBasisDeformations.RaySys.Sys.star_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 fg fq qg q2 : 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) (hfg : S.P.mul f g = some fg) (hfq : S.P.mul f q0 = some fq) (hqg : S.P.mul q0 g = some qg) (hq2 : S.P.mul q0 q0 = some q2) (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)) (R1 : ∀ (h : R), S.P.src h = a → S.P.tgt h = c → S.P.wt h = S.P.wt q0 - S.P.wt g → S.P.mul g h ≠ some q0) (R2 : ∀ (h : R), S.P.src h = c → S.P.tgt h = a → S.P.wt h = S.P.wt g - S.P.wt q0 → S.P.mul q0 h ≠ some g) (R3 : ∀ (h : R), S.P.src h = c → S.P.tgt h = b → S.P.wt h = -S.P.wt f + S.P.wt q0 → S.P.mul h f ≠ some q0) (R4 : ∀ (h : R), S.P.src h = b → S.P.tgt h = c → S.P.wt h = -S.P.wt q0 + S.P.wt f → S.P.mul h q0 ≠ some f) (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) : False

The four-leaf star is excluded.

theorem MultiplicativeBasisDeformations.RaySys.Sys.strong_star {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) (hq2 : S.q (S.P.tgt f) * S.q (S.P.tgt f) ≠ 0) : S.rr f * S.rr g = 0

Strong star vanishing (eq:strong-star-vanishing; Case 1 of Lemma 8.11): for f generated only at its target and g generated only at its source, with q² ≠ 0 at the middle vertex, fg = 0.