Lemma 8.14: generating rays have no radical factorization

lem:generating-paths (local-ray-geometry.tex), first assertion: a generating ray in a Hom of dimension at least two does not factor as a q_y b through a nonidentity local radical.

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_not_inU_strict {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f g : R} (hf : S.IsGen f) (h1 : S.P.src g = S.P.src f) (h2 : S.P.tgt g = S.P.tgt f) (hU : S.InU f g) : f = g

A generating ray is not of the form q^i g q^j with (i, j) ≠ (0, 0) for a ray g of its Hom.

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

A Hom of dimension at least two: its generating ray is moved by an endpoint radical.

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_ne_q_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f b : R} (hf : S.IsGen f) (hb1 : S.P.src b = S.P.src f) (hb2 : S.P.tgt b = S.P.tgt f) (i : ℕ) (hi : 1 ≤ i) : S.rr f ≠ S.q (S.P.src f) ^ i * S.rr b

Left factorization through a radical of the source.

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_ne_mul_q {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f b : R} (hf : S.IsGen f) (hb1 : S.P.src b = S.P.src f) (hb2 : S.P.tgt b = S.P.tgt f) (j : ℕ) (hj : 1 ≤ j) : S.rr f ≠ S.rr b * S.q (S.P.tgt f) ^ j

Right factorization through a radical of the target.

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_no_rad {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 a b : R} (hf : S.IsGen f) (hd : S.Dim2 f) (h : S.rr a * S.q (S.P.tgt a) * S.rr b = S.rr f) : False

Lemma 8.14, first assertion (lem:generating-paths): a generating ray of a Hom of dimension at least two has no factorization a q_y b through a nonidentity local radical.