Lemma 9.3: two-sided factor paths

integral-partial-lifts.tex (lem:two-sided-factor-paths): "let b be a two-sided ray. If s has type L and bs is nonzero and shiftable, then every ordinary path representing b consists of two-sided arrows. Dually, the same conclusion holds if r has type R and rb is nonzero and shiftable."

The proof of the first-arrow form (first_TB) uses only that the left factor is not an identity, so every nonidentity left factor of b is two-sided (leftFactor_TB). For an ordinary path a₁ ⋯ aₙ of b (IsOrdPath), all prefix products are therefore two-sided; an arrow aᵢ between two two-sided prefixes has both endpoint actions nonzero, since a two-sided ray commutes with q̂, so it is two-sided (ordPath_TB). The dual statement follows by passing to Sys.op (ordPath_TB').

theorem MultiplicativeBasisDeformations.RaySys.Sys.leftFactor_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 w : R} (hb : S.TB χ b) (hs : S.TL χ s) (hbs : S.rr b * S.rr s = S.rr t) (ht : S.Shift χ t) (ha0 : a ≠ S.P.e (S.P.src a)) (hw : S.rr a * S.rr w = S.rr b) : S.TB χ a

Every nonidentity left factor of b is two-sided (the proof of first_TB).

Ordinary paths

def MultiplicativeBasisDeformations.RaySys.Sys.pathM {V R L : Type} [AddCommGroup L] (S : Sys V R L) : List R → M S.P.toMult

The product of a sequence of rays.

theorem MultiplicativeBasisDeformations.RaySys.Sys.pathM_append {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (l l' : List R) : S.pathM (l ++ l') = S.pathM l * S.pathM l'

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

An ordinary path of b: a nonempty sequence of ordinary arrows with product b.

theorem MultiplicativeBasisDeformations.RaySys.Sys.pathM_ray {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {l : List R} (hl : l ≠ []) (ho : ∀ a ∈ l, a ≠ S.P.e (S.P.src a)) (h0 : S.pathM l ≠ 0) : ∃ (c : R), S.pathM l = S.rr c ∧ c ≠ S.P.e (S.P.src c)

A nonzero product of a nonempty sequence of nonidentity rays is a nonidentity ray.

theorem MultiplicativeBasisDeformations.RaySys.Sys.ordPath_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 : R} (hb : S.TB χ b) (hs : S.TL χ s) (hbs : S.rr b * S.rr s = S.rr t) (ht : S.Shift χ t) {l : List R} (hl : S.IsOrdPath b l) (a : R) : a ∈ l → S.TB χ a

Lemma 9.3 (lem:two-sided-factor-paths): if b is two-sided and bs is nonzero and shiftable with s left-sided, every ordinary path of b consists of two-sided arrows.

theorem MultiplicativeBasisDeformations.RaySys.Sys.rightFactor_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 w : R} (hb : S.TB χ b) (hr : S.TR χ r) (hrb : S.rr r * S.rr b = S.rr t) (ht : S.Shift χ t) (ha0 : a ≠ S.P.e (S.P.src a)) (hw : S.rr w * S.rr a = S.rr b) : S.TB χ a

Every nonidentity right factor of b is two-sided (dual of leftFactor_TB).

theorem MultiplicativeBasisDeformations.RaySys.Sys.ordPath_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 : R} (hb : S.TB χ b) (hr : S.TR χ r) (hrb : S.rr r * S.rr b = S.rr t) (ht : S.Shift χ t) {l : List R} (hl : S.IsOrdPath b l) (a : R) : a ∈ l → S.TB χ a

Lemma 9.3, the dual: if b is two-sided and rb is nonzero and shiftable with r right-sided, every ordinary path of b consists of two-sided arrows.