Corollary 8.13: active zero pairs

cor:active-zero-pairs (local-ray-geometry.tex): for rays r : x → y, s : y → z with rs = 0 and r * s ≠ 0, both are generating, r * s = r q_y s, and this ray is annihilated by both endpoint radicals.

theorem MultiplicativeBasisDeformations.RaySys.Sys.tgt_action_of_cycL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f r : R} (hf : S.CycL f) (h1 : S.P.src r = S.P.src f) (h2 : S.P.tgt r = S.P.tgt f) : S.rr r * S.q (S.P.tgt r) = 0 ∨ ∃ (a : ℕ), 1 ≤ a ∧ S.rr r * S.q (S.P.tgt r) = S.q (S.P.src r) ^ a * S.rr r

In a Hom cyclic at its source, the target action is a power of the source action.

theorem MultiplicativeBasisDeformations.RaySys.Sys.src_action_of_cycR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {g s : R} (hg : S.CycR g) (h1 : S.P.src s = S.P.src g) (h2 : S.P.tgt s = S.P.tgt g) : S.q (S.P.src s) * S.rr s = 0 ∨ ∃ (a : ℕ), 1 ≤ a ∧ S.q (S.P.src s) * S.rr s = S.rr s * S.q (S.P.tgt s) ^ a

In a Hom cyclic at its target, the source action is a power of the target action.

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

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

theorem MultiplicativeBasisDeformations.RaySys.Sys.active_zero {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)) {r s : R} (hrs0 : S.rr r * S.rr s = 0) (hst : S.stem r s ≠ 0) : S.IsGen r ∧ S.IsGen s ∧ S.stem r s = S.rr r * S.q (S.P.tgt r) * S.rr s ∧ S.q (S.P.src r) * (S.rr r * S.q (S.P.tgt r) * S.rr s) = 0 ∧ S.rr r * S.q (S.P.tgt r) * S.rr s * S.q (S.P.tgt s) = 0

Corollary 8.13 (cor:active-zero-pairs).