Lemma 8.11(2)

lem:opposite-controls(2): "The product space f R_c g has dimension at most one and is annihilated by rad R_b on the left and rad R_a on the right." The source's proof: a radical action at an outside endpoint moves at least two powers of q to the middle (eq:opposite-control-inclusions: rad_src_mul_of_cycR, rad_tgt_pow_mul_of_cycL), and every term f q^n g with n ≥ 2 vanishes by (1) (opposite_controls); the endpoint Hom is uniserial with a one-dimensional socle (socle_unique, from the endpoint chain), so the nonzero products f q^j g all coincide (opposite_controls_two).

theorem MultiplicativeBasisDeformations.RaySys.Sys.socle_unique {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r s : R} (h1 : S.P.src r = S.P.src s) (h2 : S.P.tgt r = S.P.tgt s) (hrL : S.q (S.P.src r) * S.rr r = 0) (hrR : S.rr r * S.q (S.P.tgt r) = 0) (hsL : S.q (S.P.src s) * S.rr s = 0) (hsR : S.rr s * S.q (S.P.tgt s) = 0) : r = s

The endpoint socle is one-dimensional: two rays with the same endpoints killed by both endpoint radicals are equal.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fqg_ray {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f g : R} (hfg : S.P.tgt f = S.P.src g) (i : ℕ) (h0 : S.rr f * S.q (S.P.tgt f) ^ i * S.rr g ≠ 0) : ∃ (w : R), S.rr f * S.q (S.P.tgt f) ^ i * S.rr g = S.rr w ∧ S.P.src w = S.P.src f ∧ S.P.tgt w = S.P.tgt g

A nonzero f q^i g is a ray from the source of f to the target of g.

theorem MultiplicativeBasisDeformations.RaySys.Sys.opposite_controls_two {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) : (∀ (j : ℕ), S.q (S.P.src f) * (S.rr f * S.q (S.P.tgt f) ^ j * S.rr g) = 0) ∧ (∀ (j : ℕ), S.rr f * S.q (S.P.tgt f) ^ j * S.rr g * S.q (S.P.tgt g) = 0) ∧ ∀ (i j : ℕ), S.rr f * S.q (S.P.tgt f) ^ i * S.rr g ≠ 0 → S.rr f * S.q (S.P.tgt f) ^ j * S.rr g ≠ 0 → S.rr f * S.q (S.P.tgt f) ^ i * S.rr g = S.rr f * S.q (S.P.tgt f) ^ j * S.rr g

Lemma 8.11(2) (lem:opposite-controls): for generating f : b → c, g : c → a whose Homs are cyclic at c but not at the other endpoints, the products f q^j g spanning f R_c g are killed by rad R_b = q_b R_b on the left and by rad R_a = R_a q_a on the right, and any two nonzero ones coincide, so f R_c g has dimension at most one.