Primitive cyclic corners (Lemma 8.21)

def:primitive-return-corner and lem:primitive-cyclic-corners (primitive-ray-equations.tex). Part (1): a generating ray f : x → y, x ≠ y, cyclic at both endpoints with q_x f = f q_y ≠ 0 and ℓ(q_x) primitive, has a primitive reverse whenever f A₀(y, x) ≠ 0: the generating ray h of A₀(y, x) satisfies fh = q_x, hf = q_y. A higher least return exponent gives a four-point crown in the faithful projective support at x.

def MultiplicativeBasisDeformations.RaySys.Sys.PrimRev {V R L : Type} [AddCommGroup L] (S : Sys V R L) (f h : R) : Prop

A primitive reverse of f (def:primitive-return-corner(1)).

theorem MultiplicativeBasisDeformations.RaySys.Sys.comm_pow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (h : S.q (S.P.src f) * S.rr f = S.rr f * S.q (S.P.tgt f)) (n : ℕ) : S.q (S.P.src f) ^ n * S.rr f = S.rr f * S.q (S.P.tgt f) ^ n

Iterating q_x f = f q_y.

theorem MultiplicativeBasisDeformations.RaySys.Sys.prim_reverse {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 h0 : R} (hf : S.IsGen f) (hxy : S.P.src f ≠ S.P.tgt f) (hL : S.CycL f) (hR : S.CycR f) (hqf : S.q (S.P.src f) * S.rr f = S.rr f * S.q (S.P.tgt f)) (hqf0 : S.q (S.P.src f) * S.rr f ≠ 0) (hprim : Prim (S.χ (S.P.src f))) (h01 : S.P.src h0 = S.P.tgt f) (h02 : S.P.tgt h0 = S.P.src f) (hfh0 : S.rr f * S.rr h0 ≠ 0) {h : R} (hh : S.IsGen h) (hh1 : S.P.src h = S.P.tgt f) (hh2 : S.P.tgt h = S.P.src f) : S.PrimRev f h

Lemma 8.21(1) (lem:primitive-cyclic-corners): the generating reverse is primitive.

Return partners and the corner S_x

def MultiplicativeBasisDeformations.RaySys.Sys.Partner {V R L : Type} [AddCommGroup L] (S : Sys V R L) (x y : V) : Prop

A return partner y of x (def:primitive-return-corner(2)).

def MultiplicativeBasisDeformations.RaySys.Sys.InS {V R L : Type} [AddCommGroup L] (S : Sys V R L) (x y : V) : Prop

Membership in the primitive return corner S_x.

theorem MultiplicativeBasisDeformations.RaySys.Sys.partner_of_factor {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x y : V} {u v : R} (hu1 : S.P.src u = x) (hu2 : S.P.tgt u = y) (hxy : y ≠ x) (huv : S.rr u * S.rr v = S.q x) (hq2 : S.q x ^ 2 ≠ 0) (hprim : Prim (S.χ x)) : S.IsGen u ∧ S.PrimRev u v ∧ S.q x * S.rr u = S.rr u * S.q y ∧ S.q x * S.rr u ≠ 0 ∧ S.Partner x y

A factorization uv = q_x through y ≠ x (lem:primitive-cyclic-corners(3), last paragraph): u is generating with primitive reverse v, and y is a return partner.

Primitive pairs

theorem MultiplicativeBasisDeformations.RaySys.Sys.χ_pair {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t h : R} (hth : S.rr t * S.rr h = S.q (S.P.src t)) (hht : S.rr h * S.rr t = S.q (S.P.tgt t)) (hq : S.q (S.P.src t) ≠ 0) (hq' : S.q (S.P.tgt t) ≠ 0) : S.χ (S.P.src t) = S.P.wt t + S.P.wt h ∧ S.χ (S.P.tgt t) = S.P.wt h + S.P.wt t

Weights of a primitive pair: χ_b = ℓ(t) + ℓ(h) = χ_c.

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_of_pair {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t h : R} (hbc : S.P.src t ≠ S.P.tgt t) (hth : S.rr t * S.rr h = S.q (S.P.src t)) (hht : S.rr h * S.rr t = S.q (S.P.tgt t)) (hq : S.q (S.P.src t) ≠ 0) (hq' : S.q (S.P.tgt t) ≠ 0) : S.IsGen t

The first ray of a primitive pair between distinct vertices is generating.

theorem MultiplicativeBasisDeformations.RaySys.Sys.partner_of_pair {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t h : R} (hbc : S.P.src t ≠ S.P.tgt t) (hth : S.rr t * S.rr h = S.q (S.P.src t)) (hht : S.rr h * S.rr t = S.q (S.P.tgt t)) (hq : S.q (S.P.src t) ≠ 0) (hq' : S.q (S.P.tgt t) ≠ 0) (h3 : S.q (S.P.src t) ^ 2 ≠ 0 ∨ S.q (S.P.tgt t) ^ 2 ≠ 0) : S.Partner (S.P.src t) (S.P.tgt t)

A primitive pair gives a return partner when one local length is at least three (lem:primitive-cyclic-corners(3): "both displayed actions are nonzero: use q_b² = t q_c h or q_c² = h q_b t").

theorem MultiplicativeBasisDeformations.RaySys.Sys.ext_chain {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)) {x : V} (hprim : Prim (S.χ x)) (hq2 : S.q x ^ 2 ≠ 0) {f h : R} (hf : S.IsGen f) (hh : S.IsGen h) (f1 : S.P.src f = x) (h1 : S.P.src h = x) (hqf : S.q x * S.rr f ≠ 0) (hqh : S.q x * S.rr h ≠ 0) (hfS : ¬S.InS x (S.P.tgt f)) (hhS : ¬S.InS x (S.P.tgt h)) : S.P.RF f h ∨ S.P.RF h f

Lemma 9.8 (lem:external-hom-chain): generating rays out of x with surviving q_x-action and targets outside S_x are comparable.

theorem MultiplicativeBasisDeformations.RaySys.Sys.partner_chain {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)) {x : V} {f f' h h' : R} (hf : S.IsGen f) (hf' : S.IsGen f') (f1 : S.P.src f = x) (f1' : S.P.src f' = x) (hfh : S.PrimRev f h) (hfh' : S.PrimRev f' h') (hq : S.q x * S.rr f = S.rr f * S.q (S.P.tgt f)) (hq0 : S.q x * S.rr f ≠ 0) (hq' : S.q x * S.rr f' = S.rr f' * S.q (S.P.tgt f')) (hq0' : S.q x * S.rr f' ≠ 0) : S.P.RF f f' ∨ S.P.RF f' f

Lemma 8.21(2), the chain (lem:primitive-cyclic-corners(2)): the generating outgoing rays of x with primitive reverses and surviving equal actions q_x f = f q_y ≠ 0 are comparable under factorization ("incomparability would be a crown").

theorem MultiplicativeBasisDeformations.RaySys.Sys.pair_of_rf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {a : V} {u u' v v' t : R} (u1 : S.P.src u = a) (v1 : S.P.src v = a) (hu : S.PrimRev u u') (hv : S.PrimRev v v') (hqu : S.q a * S.rr u = S.rr u * S.q (S.P.tgt u)) (hqu0 : S.q a * S.rr u ≠ 0) (hqv : S.q a * S.rr v = S.rr v * S.q (S.P.tgt v)) (hqv0 : S.q a * S.rr v ≠ 0) (hut : S.rr u * S.rr t = S.rr v) : ∃ (h : R), S.P.src t = S.P.tgt u ∧ S.P.tgt t = S.P.tgt v ∧ S.rr t * S.rr h = S.q (S.P.tgt u) ∧ S.rr h * S.rr t = S.q (S.P.tgt v)

The comparison pair (lem:primitive-cyclic-corners(3)): for partners b, c of a with v = ut, the rays t : b → c and h = v̄u : c → b satisfy th = q_b, ht = q_c.

theorem MultiplicativeBasisDeformations.RaySys.Sys.partners_of_rf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {a b c : V} (hbc : b ≠ c) (h3 : S.q b ^ 2 ≠ 0 ∨ S.q c ^ 2 ≠ 0) {u v : R} (u1 : S.P.src u = a) (u2 : S.P.tgt u = b) (v1 : S.P.src v = a) (v2 : S.P.tgt v = c) {u' v' : R} (hu : S.PrimRev u u') (hv : S.PrimRev v v') (hqu : S.q a * S.rr u = S.rr u * S.q b) (hqu0 : S.q a * S.rr u ≠ 0) (hqv : S.q a * S.rr v = S.rr v * S.q c) (hqv0 : S.q a * S.rr v ≠ 0) (hr : S.P.RF u v) : S.Partner b c ∧ S.Partner c b

theorem MultiplicativeBasisDeformations.RaySys.Sys.partner_comparison {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)) {a b c : V} (hb : S.Partner a b) (hc : S.Partner a c) (hbc : b ≠ c) (h3 : S.q b ^ 2 ≠ 0 ∨ S.q c ^ 2 ≠ 0) : S.Partner b c ∧ S.Partner c b

Two partners of a are mutual partners when one has local length at least three (lem:primitive-cyclic-corners(3), first paragraph).

theorem MultiplicativeBasisDeformations.RaySys.Sys.partner_symm {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {a b : V} (hb : S.Partner a b) (h3 : S.q a ^ 2 ≠ 0) : S.Partner b a

a is a partner of its partner b when N_a ≥ 3 (q_b ū = ū q_a ≠ 0).

theorem MultiplicativeBasisDeformations.RaySys.Sys.inS_subset {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)) {a b : V} (hb : S.Partner a b) (ha3 : S.q a ^ 2 ≠ 0) (hb3 : S.q b ^ 2 ≠ 0) {c : V} (hc : S.InS a c) : S.InS b c

V_a ⊆ V_b for a partner b of a with N_a, N_b ≥ 3.

theorem MultiplicativeBasisDeformations.RaySys.Sys.inS_eq {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)) {a b : V} (hb : S.Partner a b) (ha3 : S.q a ^ 2 ≠ 0) (hb3 : S.q b ^ 2 ≠ 0) (c : V) : S.InS a c ↔ S.InS b c

V_a = V_b for a partner b of a with N_a, N_b ≥ 3.

theorem MultiplicativeBasisDeformations.RaySys.Sys.inS_disjoint_or_eq {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)) {x x' : V} (hx3 : S.q x ^ 2 ≠ 0) (hx3' : S.q x' ^ 2 ≠ 0) {v : V} (hv : S.InS x v) (hv' : S.InS x' v) (y : V) : S.InS x y ↔ S.InS x' y

Lemma 8.21(3) (lem:primitive-cyclic-corners(3)): for vertices x, x' with N_x, N_{x'} ≥ 3, the vertex sets V_x, V_{x'} of the primitive return corners are disjoint or equal. (Primitivity is not needed for this part; with it, every nontrivial factorization of q_x passes through S_x, partner_of_factor.)

theorem MultiplicativeBasisDeformations.RaySys.Sys.loop_of_eq_q {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {t : R} (ht : S.rr t = S.q x) : S.P.src t = x ∧ S.P.tgt t = x

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_partner_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x y : V} (hq2 : S.q x ^ 2 ≠ 0) (hprim : Prim (S.χ x)) : S.op.Partner x y ↔ S.Partner x y

Return partners agree for A₀ and A₀ᵒᵖ when q_x² ≠ 0.

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_inS_iff {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x y : V} (hq2 : S.q x ^ 2 ≠ 0) (hprim : Prim (S.χ x)) : S.op.InS x y ↔ S.InS x y

theorem MultiplicativeBasisDeformations.RaySys.Sys.ext_chain_in {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)) {x : V} (hprim : Prim (S.χ x)) (hq2 : S.q x ^ 2 ≠ 0) {f h : R} (hf : S.IsGen f) (hh : S.IsGen h) (f2 : S.P.tgt f = x) (h2 : S.P.tgt h = x) (hqf : S.rr f * S.q x ≠ 0) (hqh : S.rr h * S.q x ≠ 0) (hfS : ¬S.InS x (S.P.src f)) (hhS : ¬S.InS x (S.P.src h)) : S.P.LF f h ∨ S.P.LF h f

Lemma 9.8, incoming form.