Lemma 8.10: unequal endpoint actions

lem:unequal-endpoint-action (local-ray-geometry.tex): "suppose A₀(x,y) = R_x f has dimension l, where f is generating. If f q_y = q_x^a f ≠ 0 with a ≥ 2, then l = a+1, and f q_y lies in the endpoint socle of A₀(x,y)."

Deviation: the paper's seven-point support poset has one commuting relation (F = 1 in Lemma 8.8); we use its full subposet without v₀ = f, the Euclidean tree D̃₅ with two adjacent trivalent vertices (N = D = 12), which needs no relation.

def MultiplicativeBasisDeformations.RaySys.Sys.tD5 : Fin 6 → Fin 6 → Bool

The table of D̃₅: u₀ < u₁ < u₂ < u₃, u₁ < v₁, u₂ < v₂ (indices 0..5 are u₀ u₁ u₂ u₃ v₁ v₂).

theorem MultiplicativeBasisDeformations.RaySys.Sys.tD5_uniq : PosetRep.UniqOK tD5

theorem MultiplicativeBasisDeformations.RaySys.Sys.tD5_count : PosetRep.CountOK tD5 ![1, 2, 2, 1, 1, 1]

theorem MultiplicativeBasisDeformations.RaySys.Sys.wt_of_eq_qpow_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {v f : R} {c : ℕ} (h : S.rr v = S.q (S.P.src f) ^ c * S.rr f) : S.P.wt v = c • S.χ (S.P.src f) + S.P.wt f

theorem MultiplicativeBasisDeformations.RaySys.Sys.wt_of_eq_qpow_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {v : R} {x : V} {c : ℕ} (h : S.rr v = S.q x ^ c * S.rr (S.P.e x)) : S.P.wt v = c • S.χ x

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_wt_qpow_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {v : R} {x : V} {c : ℕ} (h : S.rr v = S.q x ^ c * S.rr (S.P.e x)) : S.P.deg (S.P.wt v) = ↑c * S.P.deg (S.χ x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_wt_qpow_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {v f : R} {c : ℕ} (h : S.rr v = S.q (S.P.src f) ^ c * S.rr f) : S.P.deg (S.P.wt v) = ↑c * S.P.deg (S.χ (S.P.src f)) + S.P.deg (S.P.wt f)

theorem MultiplicativeBasisDeformations.RaySys.Sys.local_deg {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) (h : S.P.src r = S.P.tgt r) : ∃ (c : ℕ), S.rr r = S.q (S.P.src r) ^ c * S.rr (S.P.e (S.P.src r)) ∧ S.P.deg (S.P.wt r) = ↑c * S.P.deg (S.χ (S.P.src r))

A loop is a power of the local generator; its degree is a multiple of deg χ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_pos_of_ne {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.P.src f ≠ S.P.tgt f) : 0 < S.P.deg (S.P.wt f)

The identity is the only ray of degree zero; a generating ray of a loop Hom is e.

theorem MultiplicativeBasisDeformations.RaySys.Sys.d5_order {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {Xr Yr : ℕ → R} {a : ℕ} (ha : 2 ≤ a) (XX : ∀ (m m' : ℕ), m ≤ a + 1 → m' ≤ a + 1 → (S.P.RF (Xr m) (Xr m') ↔ m ≤ m')) (XY : ∀ (m m' : ℕ), m ≤ a + 1 → m' ≤ a + 1 → (S.P.RF (Xr m) (Yr m') ↔ m ≤ m')) (YX : ∀ (m m' : ℕ), 1 ≤ m → m ≤ a → m' ≤ a + 1 → ¬S.P.RF (Yr m) (Xr m')) (YY : ∀ (m m' : ℕ), m = 1 ∧ m' = a ∨ m = a ∧ m' = 1 → ¬S.P.RF (Yr m) (Yr m')) (i j : Fin 6) : tD5 i j = true ↔ S.P.RF (![Xr 0, Xr 1, Xr a, Xr (a + 1), Yr 1, Yr a] i) (![Xr 0, Xr 1, Xr a, Xr (a + 1), Yr 1, Yr a] j)

The order of the six support points of Lemma 8.10 is D̃₅.

theorem MultiplicativeBasisDeformations.RaySys.Sys.unequal_endpoint_action {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 : R} (hf : S.CycL f) {a : ℕ} (ha : 2 ≤ a) (h : S.rr f * S.q (S.P.tgt f) = S.q (S.P.src f) ^ a * S.rr f) (h0 : S.rr f * S.q (S.P.tgt f) ≠ 0) : S.q (S.P.src f) ^ (a + 1) * S.rr f = 0

Lemma 8.10 (lem:unequal-endpoint-action), length part: q_x^{a+1} f = 0, i.e. dim A₀(x, y) ≤ a + 1.

theorem MultiplicativeBasisDeformations.RaySys.Sys.unequal_endpoint_socle {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 : R} (hf : S.CycL f) {a : ℕ} (ha : 2 ≤ a) (h : S.rr f * S.q (S.P.tgt f) = S.q (S.P.src f) ^ a * S.rr f) (h0 : S.rr f * S.q (S.P.tgt f) ≠ 0) : S.q (S.P.src f) * (S.rr f * S.q (S.P.tgt f)) = 0 ∧ S.rr f * S.q (S.P.tgt f) * S.q (S.P.tgt f) = 0

Lemma 8.10, socle part: f q_y is annihilated by both endpoint radicals.