Ordinary arrows and one-sided generating contours

def:generating-rays(3), the path part of lem:generating-paths, and prop:controlled-contours (primitive-ray-equations.tex, Appendix C.1 in local-ray-restrictions.tex).

An ordinary path for a ray f starts with an ordinary left divisor of f, and every ordinary left divisor starts such a path. We prove prop:controlled-contours in the form used by lem:one-sided-path-coefficients: a generating ray of type L has exactly one ordinary left divisor (all its ordinary paths start with the same arrow), and dually for type R. The proof is that of Appendix C.1 applied to two paths with distinct first (respectively last) arrows: the crown and the six-point tree fix their types, and the six-lift and eight-lift trees exclude the remaining case.

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

An ordinary arrow (def:generating-rays(3)).

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

An ordinary left divisor: the first arrow of an ordinary path of f.

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

An ordinary right divisor: the last arrow of an ordinary path of f.

theorem MultiplicativeBasisDeformations.RaySys.Sys.ne_e_of_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 : 0 < S.P.deg (S.P.wt r)) : r ≠ S.P.e (S.P.src r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_pos_of_ne_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r : R} (h : r ≠ S.P.e (S.P.src r)) : 0 < S.P.deg (S.P.wt r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.exists_OL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (f : R) (hf : f ≠ S.P.e (S.P.src f)) : ∃ (a : R), S.OL f a

Every nonidentity ray has an ordinary left divisor.

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

Right multiplication by a local power keeps the endpoints of a ray.

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

Left multiplication by a local power keeps the endpoints of a ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_loop_e {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {m : R} (hm : S.IsGen m) (hl : S.P.src m = S.P.tgt m) : m = S.P.e (S.P.src m)

A generating local ray is an identity.

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

Lemma 8.14, path part (lem:generating-paths): every factor of a generating ray in a Hom of dimension at least two is generating.

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

Lemma 8.14, vertex-simplicity: a generating ray in a Hom of dimension at least two has no local nonidentity factor.

theorem MultiplicativeBasisDeformations.RaySys.Sys.no_below_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 χ) {g r : R} (hg : S.IsGen g) (h1 : S.P.src r = S.P.src g) (h2 : S.P.tgt r = S.P.tgt g) (n : ℕ) (hn : 1 ≤ n) (hw : S.P.wt g = S.P.wt r + n • χ) : False

No ray lies n χ below a generating ray (start of Appendix C.1).

First arrows of a left-sided generating ray

theorem MultiplicativeBasisDeformations.RaySys.Sys.ord_not_rf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {a1 a2 : R} (h1 : a1 ≠ S.P.e (S.P.src a1)) (h2 : S.Ord a2) (hne : a1 ≠ a2) : ¬S.P.RF a1 a2

Distinct ordinary arrows are incomparable.

theorem MultiplicativeBasisDeformations.RaySys.Sys.ol_cofactor_ne {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f a1 a2 w1 : R} (h1 : S.Ord a1) (h2 : S.OL f a2) (hne : a1 ≠ a2) (hw1 : S.rr a1 * S.rr w1 = S.rr f) : w1 ≠ S.P.e (S.P.src w1)

The cofactor of an ordinary left divisor is not an identity when another one exists.

theorem MultiplicativeBasisDeformations.RaySys.Sys.supp_of_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} {r : R} (h : S.qh χ x * S.rr r ≠ 0) : S.Supp χ x

A supporting source gives q̂_x = q_x and ℓ(q_x) = χ.

theorem MultiplicativeBasisDeformations.RaySys.Sys.supp_of_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} {r : R} (h : S.rr r * S.qh χ x ≠ 0) : S.Supp χ x

theorem MultiplicativeBasisDeformations.RaySys.Sys.local_eq_q {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 χ) {v : R} (hl : S.P.src v = S.P.tgt v) (hw : S.P.wt v = χ) : S.rr v = S.q (S.P.src v) ∧ S.Supp χ (S.P.src v)

A local ray of character χ (primitive, positive) is the local generator.

theorem MultiplicativeBasisDeformations.RaySys.Sys.no_hidden_target {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 χ) {f v : R} (hT : S.TL χ f) (hv : S.rr f * S.rr v = S.qh χ (S.P.src f) * S.rr f) : False

A left-sided ray has no target action of character χ hidden in its projective support: f v = q̂_x f is impossible.

theorem MultiplicativeBasisDeformations.RaySys.Sys.no_return_one {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 χ) {a v : R} (hT : S.TL χ a) (hv : S.rr a * S.rr v = S.q (S.P.src a)) : False

A left-sided ray has no return a v = q_x.

theorem MultiplicativeBasisDeformations.RaySys.Sys.no_cross {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 χ) {f ai wi aj wj h : R} (hT : S.TL χ f) (hai : S.TL χ ai) (hai0 : ai ≠ S.P.e (S.P.src ai)) (hwi0 : wi ≠ S.P.e (S.P.src wi)) (hwi : S.rr ai * S.rr wi = S.rr f) (hwj : S.rr aj * S.rr wj = S.rr f) (hsj : S.P.src aj = S.P.src f) (hh : S.rr ai * S.rr h = S.qh χ (S.P.src f) * S.rr aj) : False

A cross comparison a_i h = q̂_x a_j between first arrows of a left-sided ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.first_arrow_types {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] {χ : L} (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {f a1 a2 : R} (hf : S.IsGen f) (hT : S.TL χ f) (h1 : S.OL f a1) (h2 : S.OL f a2) (hne : a1 ≠ a2) : S.TL χ a1 ∧ S.TB χ a2 ∨ S.TB χ a1 ∧ S.TL χ a2

Two distinct first arrows of a left-sided generating ray (Appendix C.1, first step): one is left-sided and the other two-sided.

The opposite system

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_ord {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (a : R) : S.op.Ord a ↔ S.Ord a

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_OL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (f a : R) : S.op.OL f a ↔ S.OR f a

theorem MultiplicativeBasisDeformations.RaySys.Sys.last_arrow_types {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] {χ : L} (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {f b1 b2 : R} (hf : S.IsGen f) (hT : S.TR χ f) (h1 : S.OR f b1) (h2 : S.OR f b2) (hne : b1 ≠ b2) : S.TR χ b1 ∧ S.TB χ b2 ∨ S.TB χ b1 ∧ S.TR χ b2

Two distinct last arrows of a right-sided generating ray: one is right-sided and the other two-sided (the dual of first_arrow_types).

Right-sided rays with two last arrows

theorem MultiplicativeBasisDeformations.RaySys.Sys.ord_not_lf {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {a b : R} (ha : a ≠ S.P.e (S.P.src a)) (hb : S.Ord b) (hne : a ≠ b) : ¬S.P.LF b a

An ordinary arrow is not a proper left multiple of another ray.

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.no_hidden_source {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 χ) {f v : R} (hT : S.TR χ f) (hv : S.rr v * S.rr f = S.rr f * S.qh χ (S.P.tgt f)) : False

eq:absent-source-action: a right-sided ray has no hidden source action.

theorem MultiplicativeBasisDeformations.RaySys.Sys.or_cofactor_ne {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f b1 b2 w1 : R} (h1 : S.Ord b1) (h2 : S.OR f b2) (hne : b1 ≠ b2) (hw1 : S.rr w1 * S.rr b1 = S.rr f) : w1 ≠ S.P.e (S.P.src w1)

The cofactor of an ordinary right divisor is not an identity when another one exists.

theorem MultiplicativeBasisDeformations.RaySys.Sys.right_two_last {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] {χ : L} (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {f α β : R} (hf : S.IsGen f) (hT : S.TR χ f) (hα : S.OR f α) (hβ : S.OR f β) (hne : α ≠ β) (hαB : S.TB χ α) (hβR : S.TR χ β) : False

The right-sided case of Appendix C.1: a right-sided generating ray has no two last arrows of types B and R. With a primitive reverse of the two-sided arrow the six-lift tree occurs; otherwise the eight-lift tree occurs.

theorem MultiplicativeBasisDeformations.RaySys.Sys.unique_last {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] {χ : L} (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {f b1 b2 : R} (hf : S.IsGen f) (hT : S.TR χ f) (h1 : S.OR f b1) (h2 : S.OR f b2) : b1 = b2

Proposition 9.10 (prop:controlled-contours), right-sided form: all ordinary paths of a right-sided generating ray end with the same arrow.

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_OR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (f a : R) : S.op.OR f a ↔ S.OL f a

theorem MultiplicativeBasisDeformations.RaySys.Sys.unique_first {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] {χ : L} (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {f a1 a2 : R} (hf : S.IsGen f) (hT : S.TL χ f) (h1 : S.OL f a1) (h2 : S.OL f a2) : a1 = a2

Proposition 9.10, left-sided form: all ordinary paths of a left-sided generating ray start with the same arrow.