Two-sided segments, crown rows and nondeep boundary arrows

lem:two-sided-factor-paths, lem:crown-output-comparison and lem:nondeep-boundary-arrows (integral-partial-lifts.tex), in path-free form: an ordinary path is recorded by its first (last) arrow, an ordinary left (right) divisor.

theorem MultiplicativeBasisDeformations.RaySys.Sys.out_BL {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 χ) {r s t : R} (hr : S.TB χ r) (hs : S.TL χ s) (hrs : S.rr r * S.rr s = S.rr t) (ht : S.Shift χ t) : S.TL χ t

The output type of a product of a two-sided and a left-sided ray is left-sided.

theorem MultiplicativeBasisDeformations.RaySys.Sys.first_TB {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 χ) {b s t a : R} (hb : S.TB χ b) (hs : S.TL χ s) (hbs : S.rr b * S.rr s = S.rr t) (ht : S.Shift χ t) (ha : S.OL b a) : S.TB χ a

Lemma 9.3, first-arrow form (lem:two-sided-factor-paths): if b is two-sided and bs is shiftable with s left-sided, every ordinary path of b starts with a two-sided arrow.

theorem MultiplicativeBasisDeformations.RaySys.Sys.last_TB {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 χ) {r b t a : R} (hb : S.TB χ b) (hr : S.TR χ r) (hrb : S.rr r * S.rr b = S.rr t) (ht : S.Shift χ t) (ha : S.OR b a) : S.TB χ a

Lemma 9.3, last-arrow form (the dual).

theorem MultiplicativeBasisDeformations.RaySys.Sys.nondeep_first_TL {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 χ) {x : V} {e l a : R} (hN : S.NondeepRet χ x e l) (ha : S.OL e a) : S.TL χ a

Lemma 9.6 (lem:nondeep-boundary-arrows): the first arrow of the outgoing ray of a nondeep return is left-sided.

theorem MultiplicativeBasisDeformations.RaySys.Sys.nondeep_last_TR {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 χ) {x : V} {e l b : R} (hN : S.NondeepRet χ x e l) (hb : S.OR l b) : S.TR χ b

Lemma 9.6, dual: the last arrow of the incoming ray of a nondeep return is right-sided.

theorem MultiplicativeBasisDeformations.RaySys.Sys.exists_OR {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)) : ∃ (b : R), S.OR f b

Every nonidentity ray has an ordinary right divisor.

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

A row X_a + Y_b = [f] with generating two-sided output (eq:generating-crown-row): f = a v = w b with v right-sided and w left-sided generating, b the last arrow of v and a the first arrow of w.

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

A row X_a + Y_b = 2[q̂_x] of a nondeep return (eq:nondeep-coefficient-row).

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_crownRow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {a b f : R} : S.op.CrownRow χ b a f ↔ S.CrownRow χ a b f

theorem MultiplicativeBasisDeformations.RaySys.Sys.crown_compare {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 χ) {a f t v w : R} (ha : S.TL χ a) (hoa : S.Ord a) (hf : S.TB χ f) (ht : S.TB χ t) (hfa : S.rr a * S.rr v = S.rr f) (hta : S.rr a * S.rr w = S.rr t) : S.P.RF f t ∨ S.P.RF t f

Lemma 9.5, first part (lem:crown-output-comparison): two two-sided rays whose paths start with the same ordinary left-sided arrow are comparable by right factorization.

theorem MultiplicativeBasisDeformations.RaySys.Sys.crown_row_step {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 χ) {a b b' f t h : R} (hf : S.CrownRow χ a b f) (ht : S.CrownRow χ a b' t) (hh : S.rr f * S.rr h = S.rr t) : f = t

One direction of the uniqueness: f h = t forces f = t.

theorem MultiplicativeBasisDeformations.RaySys.Sys.crown_row_unique_a {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 χ) {a b b' f t : R} (hf : S.CrownRow χ a b f) (ht : S.CrownRow χ a b' t) : f = t

Lemma 9.5 (lem:crown-output-comparison, last assertion): crown rows sharing the variable X_a have the same output ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.crown_row_unique_b {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 χ) {a a' b f t : R} (hf : S.CrownRow χ a b f) (ht : S.CrownRow χ a' b t) : f = t

Lemma 9.5, dual: crown rows sharing Y_b have the same output ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_ndRow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} {a b : R} {x : V} (hprim : Prim χ) (h : S.NdRow χ a b x) : S.op.NdRow χ b a x

theorem MultiplicativeBasisDeformations.RaySys.Sys.prim_rev_of_TB {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)) (hprim : Prim χ) {f w : R} (hf : S.IsGen f) (hB : S.TB χ f) (w1 : S.P.src w = S.P.tgt f) (w2 : S.P.tgt w = S.P.src f) (hw : S.rr f * S.rr w ≠ 0) : ∃ (g : R), S.PrimRev f g

A generating two-sided ray with a nonzero reverse product has a primitive reverse.

theorem MultiplicativeBasisDeformations.RaySys.Sys.crown_nd_disjoint_a {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 χ) {a b b' f : R} {x : V} (hf : S.CrownRow χ a b f) (hn : S.NdRow χ a b' x) : False

The variable X_a of a nondeep row occurs in no crown row (integral-partial-lifts.tex).

theorem MultiplicativeBasisDeformations.RaySys.Sys.crown_nd_disjoint_b {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 χ) {a a' b f : R} {x : V} (hf : S.CrownRow χ a b f) (hn : S.NdRow χ a' b x) : False

The variable Y_b of a nondeep row occurs in no crown row (the dual).