Section 9: successors and endpoint types

def:primitive-characters, set:fixed-character, def:successor-types (primitive-ray-equations.tex): for a positive primitive character χ ∈ L, q̂_x = q_x if q_x ≠ 0 and ℓ(q_x) = χ, and 0 otherwise. A nonidentity ray is shiftable if a ray with the same endpoints has weight ℓ(r) + χ (its successor r⁺). The successor is obtained by one local generator of character χ (succ_by_gen), which gives the three endpoint types L, R, B. Also lem:primitive-action-generation (primitive-ray-equations.tex).

def MultiplicativeBasisDeformations.RaySys.Sys.Prim {L : Type} [AddCommGroup L] (χ : L) : Prop

A primitive character: not a proper integer multiple.

Lemma 9.4: primitive action generation

theorem MultiplicativeBasisDeformations.RaySys.Sys.prim_action_gen {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) (hprim : Prim (S.χ (S.P.src f))) (hqf : S.q (S.P.src f) * S.rr f ≠ 0) : S.CycL f ∧ (S.CycR f → S.χ (S.P.tgt f) = S.χ (S.P.src f) ∧ S.q (S.P.src f) * S.rr f = S.rr f * S.q (S.P.tgt f))

Lemma 9.4 (lem:primitive-action-generation): for f generating with ℓ(q_x) primitive and q_x f ≠ 0, the Hom is cyclic at x; if it is also cyclic at y, then ℓ(q_y) = ℓ(q_x) and q_x f = f q_y.

The fixed character

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

A supporting vertex: its local generator has character χ.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.qh {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (x : V) : M S.P.toMult

q̂_x (set:fixed-character).

def MultiplicativeBasisDeformations.RaySys.Sys.Shift {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (r : R) : Prop

A shiftable ray (def:successor-types(2)).

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.succ {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (r : R) : R

The successor r⁺.

theorem MultiplicativeBasisDeformations.RaySys.Sys.succ_spec {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {r : R} (h : S.Shift χ r) : S.P.src (S.succ χ r) = S.P.src r ∧ S.P.tgt (S.succ χ r) = S.P.tgt r ∧ S.P.wt (S.succ χ r) = S.P.wt r + χ

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_succ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {r t : R} (h : S.Shift χ r) (h1 : S.P.src t = S.P.src r) (h2 : S.P.tgt t = S.P.tgt r) (h3 : S.P.wt t = S.P.wt r + χ) : t = S.succ χ r

The successor is the only ray with its endpoints and weight.

theorem MultiplicativeBasisDeformations.RaySys.Sys.qh_of_supp {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {x : V} (h : S.Supp χ x) : S.qh χ x = S.q x

theorem MultiplicativeBasisDeformations.RaySys.Sys.qh_of_not_supp {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {x : V} (h : ¬S.Supp χ x) : S.qh χ x = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.qh_mul_cases {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {r : R} (h : S.Shift χ r) : S.qh χ (S.P.src r) * S.rr r = 0 ∨ S.qh χ (S.P.src r) * S.rr r = S.rr (S.succ χ r)

q̂_x r is zero or the successor.

theorem MultiplicativeBasisDeformations.RaySys.Sys.mul_qh_cases {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) {r : R} (h : S.Shift χ r) : S.rr r * S.qh χ (S.P.tgt r) = 0 ∨ S.rr r * S.qh χ (S.P.tgt r) = S.rr (S.succ χ r)

r q̂_y is zero or the successor.

theorem MultiplicativeBasisDeformations.RaySys.Sys.succ_by_gen {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r : R} (h : S.Shift χ r) : S.qh χ (S.P.src r) * S.rr r = S.rr (S.succ χ r) ∨ S.rr r * S.qh χ (S.P.tgt r) = S.rr (S.succ χ r)

The successor is obtained by one local generator of character χ.

def MultiplicativeBasisDeformations.RaySys.Sys.TL {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (r : R) : Prop

Type L: a surviving source action only.

def MultiplicativeBasisDeformations.RaySys.Sys.TR {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (r : R) : Prop

Type R: a surviving target action only.

def MultiplicativeBasisDeformations.RaySys.Sys.TB {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (r : R) : Prop

Type B: both actions survive (and agree).

def MultiplicativeBasisDeformations.RaySys.Sys.EL {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (r s t : R) : Prop

Left successor substitution r⁺ s = t⁺.

def MultiplicativeBasisDeformations.RaySys.Sys.ER {V R L : Type} [AddCommGroup L] [DecidableEq L] [DecidableEq V] [Fintype R] (S : Sys V R L) (χ : L) (r s t : R) : Prop

Right successor substitution r s⁺ = t⁺.

theorem MultiplicativeBasisDeformations.RaySys.Sys.types_of_shift {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r : R} (h : S.Shift χ r) : S.TL χ r ∨ S.TR χ r ∨ S.TB χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.shift_of_qh_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r : R} (hr : r ≠ S.P.e (S.P.src r)) (h : S.qh χ (S.P.src r) * S.rr r ≠ 0) : S.Shift χ r ∧ S.qh χ (S.P.src r) * S.rr r = S.rr (S.succ χ r)

A nonzero source action makes a nonidentity ray shiftable, with the action its successor.

theorem MultiplicativeBasisDeformations.RaySys.Sys.shift_of_mul_qh {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r : R} (hr : r ≠ S.P.e (S.P.src r)) (h : S.rr r * S.qh χ (S.P.tgt r) ≠ 0) : S.Shift χ r ∧ S.rr r * S.qh χ (S.P.tgt r) = S.rr (S.succ χ r)

A nonzero target action makes a nonidentity ray shiftable, with the action its successor.

theorem MultiplicativeBasisDeformations.RaySys.Sys.prod_ne_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r s t : R} (hr : r ≠ S.P.e (S.P.src r)) (hrs : S.rr r * S.rr s = S.rr t) : t ≠ S.P.e (S.P.src t)

A nonzero product of nonidentity rays is not an identity.

theorem MultiplicativeBasisDeformations.RaySys.Sys.subst_left {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r s t : R} (hr : S.Shift χ r) (hrs : S.rr r * S.rr s = S.rr t) : S.rr (S.succ χ r) * S.rr s = 0 ∨ S.Shift χ t ∧ S.rr (S.succ χ r) * S.rr s = S.rr (S.succ χ t)

Substitutions in a product are zero or the successor of the output.

theorem MultiplicativeBasisDeformations.RaySys.Sys.subst_right {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r s t : R} (hr : r ≠ S.P.e (S.P.src r)) (hs : S.Shift χ s) (hrs : S.rr r * S.rr s = S.rr t) : S.rr r * S.rr (S.succ χ s) = 0 ∨ S.Shift χ t ∧ S.rr r * S.rr (S.succ χ s) = S.rr (S.succ χ t)

theorem MultiplicativeBasisDeformations.RaySys.Sys.table_L {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r s t : R} (hr : r ≠ S.P.e (S.P.src r)) (hs : s ≠ S.P.e (S.P.src s)) (hrs : S.rr r * S.rr s = S.rr t) (ht : S.TL χ t) : S.TL χ r ∧ S.EL χ r s t ∧ ¬S.ER χ r s t ∨ S.TB χ r ∧ S.TL χ s ∧ S.EL χ r s t ∧ S.ER χ r s t

Lemma 9.5, rows with output of type L (lem:successor-substitutions).

Translation to the opposite system

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_supp {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (x : V) : S.op.Supp χ x ↔ S.Supp χ x

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_qh {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (x : V) : S.op.qh χ x = S.P.toOp (S.qh χ x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.ne_e_iff_op {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : r ≠ S.P.e (S.P.tgt r) ↔ r ≠ S.P.e (S.P.src r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_shift {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (r : R) : S.op.Shift χ r ↔ S.Shift χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_succ {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r : R} (h : S.Shift χ r) : S.op.succ χ r = S.succ χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_TL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (r : R) : S.op.TL χ r ↔ S.TR χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_TR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (r : R) : S.op.TR χ r ↔ S.TL χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_TB {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (r : R) : S.op.TB χ r ↔ S.TB χ r

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_EL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r s t : R} (ht : S.Shift χ t) : S.op.EL χ s r t ↔ S.ER χ r s t

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_ER {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r s t : R} (ht : S.Shift χ t) : S.op.ER χ s r t ↔ S.EL χ r s t

theorem MultiplicativeBasisDeformations.RaySys.Sys.table_R {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r s t : R} (hr : r ≠ S.P.e (S.P.src r)) (hs : s ≠ S.P.e (S.P.src s)) (hrs : S.rr r * S.rr s = S.rr t) (ht : S.TR χ t) : S.TR χ s ∧ S.ER χ r s t ∧ ¬S.EL χ r s t ∨ S.TB χ s ∧ S.TR χ r ∧ S.EL χ r s t ∧ S.ER χ r s t

Lemma 9.5, rows with output of type R (by passing to the opposite system).

theorem MultiplicativeBasisDeformations.RaySys.Sys.table_B {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r s t : R} (hr : r ≠ S.P.e (S.P.src r)) (hs : s ≠ S.P.e (S.P.src s)) (hrs : S.rr r * S.rr s = S.rr t) (ht : S.TB χ t) : (S.TB χ r ∧ S.TB χ s ∨ S.TL χ r ∧ S.TR χ s) ∧ S.EL χ r s t ∧ S.ER χ r s t

Lemma 9.5, rows with output of type B.

theorem MultiplicativeBasisDeformations.RaySys.Sys.table_unshift {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {r s t : R} (hr : r ≠ S.P.e (S.P.src r)) (hrs : S.rr r * S.rr s = S.rr t) (ht : ¬S.Shift χ t) : (S.Shift χ r → S.rr (S.succ χ r) * S.rr s = 0) ∧ (S.Shift χ s → S.rr r * S.rr (S.succ χ s) = 0)

Lemma 9.5, unshiftable outputs: no successor substitution survives.