Lemma 9.4 along arbitrary ordinary paths

lem:one-sided-path-coefficients (integral-partial-lifts.tex): for a generating left-sided ray r, an ordinary path of r with two-sided prefix p and first left-sided arrow a, the value d_r = [p] + X_a does not depend on the chosen path, and neither does a. Dually d_s = Y_b + [p'] for a generating right-sided ray s.

IntegralLifting.lean defines d_r (DL) by a recursion on unique first arrows. Here the manuscript's definition is given (dPath, dPathR: read along a chosen ordinary path, which exists, exists_ordPath) and shown equal to it (dPath_eq_DL, dPathR_eq_DR), so the product equations DL_prod, DR_prod hold for it. The value read along any ordinary path is DL r (dL_eq_pathCoef), the first arrow of the path which is not two-sided (fstNB) exists and is left-sided, and it is the same for all paths (fstNB_unique). The dual statements read the reversed path (dR_eq_pathCoef, lstNB_unique). The product equations with generating one-sided output are DL_prod and DR_prod.

def MultiplicativeBasisDeformations.RaySys.Sys.pathCoef {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) (ω X : R → ℤ) : List R → ℤ

[p] + X_a read along a path: two-sided arrows contribute ω; the first arrow a which is not two-sided contributes X_a and ends the reading.

def MultiplicativeBasisDeformations.RaySys.Sys.fstNB {V R L : Type} [AddCommGroup L] (S : Sys V R L) (χ : L) : List R → Option R

The first arrow of a path which is not two-sided.

theorem MultiplicativeBasisDeformations.RaySys.Sys.pathCoef_of_fstNB {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (X : R → ℤ) {a : R} (l : List R) (h : S.fstNB χ l = some a) : S.pathCoef χ 0 X l = X a

theorem MultiplicativeBasisDeformations.RaySys.Sys.exists_ordPath {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) (hr : r ≠ S.P.e (S.P.src r)) : ∃ (l : List R), S.IsOrdPath r l

Every nonidentity ray has an ordinary path: split it into nonidentity factors until all factors are ordinary (the degree drops at each split).

theorem MultiplicativeBasisDeformations.RaySys.Sys.dL_eq_pathCoef {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (ω X : R → ℤ) (l : List R) {r : R} (hr : S.IsGen r) (hT : S.TL χ r) (hl : S.IsOrdPath r l) : S.DL χ ω X r = S.pathCoef χ ω X l ∧ ∃ (a : R), S.fstNB χ l = some a ∧ S.TL χ a

Lemma 9.4, path form: along any ordinary path of a generating left-sided ray r, d_r = [p] + X_a, where p is the two-sided prefix and a the first arrow which is not two-sided; this arrow exists and is left-sided.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.dPath {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (ω X : R → ℤ) (r : R) : ℤ

d_r = [p] + X_a, defined as in the manuscript: read along a chosen ordinary path.

theorem MultiplicativeBasisDeformations.RaySys.Sys.dPath_eq_DL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (ω X : R → ℤ) {r : R} (hr : S.IsGen r) (hT : S.TL χ r) : S.dPath χ ω X r = S.DL χ ω X r

The path definition of d_r is the coefficient DL used in the integral lifting.

theorem MultiplicativeBasisDeformations.RaySys.Sys.dPath_prod {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (ω X : R → ℤ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r u v : R} (hr : S.IsGen r) (hT : S.TL χ r) (huv : S.rr u * S.rr v = S.rr r) (hu0 : u ≠ S.P.e (S.P.src u)) : (S.TL χ u → S.dPath χ ω X r = S.dPath χ ω X u) ∧ (S.TB χ u → S.dPath χ ω X r = ω u + S.dPath χ ω X v)

Lemma 9.4, product equations with generating left-sided output, for the path definition: d_t = d_u for a left-sided first factor, d_t = [u] + d_v for a two-sided one.

theorem MultiplicativeBasisDeformations.RaySys.Sys.pathCoef_unique {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (ω X : R → ℤ) {r : R} (hr : S.IsGen r) (hT : S.TL χ r) {l l' : List R} (hl : S.IsOrdPath r l) (hl' : S.IsOrdPath r l') : S.pathCoef χ ω X l = S.pathCoef χ ω X l'

Lemma 9.4: d_r = [p] + X_a does not depend on the chosen ordinary path.

theorem MultiplicativeBasisDeformations.RaySys.Sys.fstNB_unique {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {r : R} (hr : S.IsGen r) (hT : S.TL χ r) {l l' : List R} (hl : S.IsOrdPath r l) (hl' : S.IsOrdPath r l') : S.fstNB χ l = S.fstNB χ l'

Lemma 9.4: the first left-sided arrow of an ordinary path of a generating left-sided ray does not depend on the path.

The dual: right-sided rays

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_pathM {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (l : List R) : S.op.pathM l.reverse = S.P.toOp (S.pathM l)

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_isOrdPath {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {s : R} {l : List R} (h : S.IsOrdPath s l) : S.op.IsOrdPath s l.reverse

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_pathCoef {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (ω X : R → ℤ) (l : List R) : S.op.pathCoef χ ω X l = S.pathCoef χ ω X l

theorem MultiplicativeBasisDeformations.RaySys.Sys.op_fstNB {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.op.fstNB χ l = S.fstNB χ l

theorem MultiplicativeBasisDeformations.RaySys.Sys.dR_eq_pathCoef {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (ω Y : R → ℤ) (l : List R) {s : R} (hs : S.IsGen s) (hT : S.TR χ s) (hl : S.IsOrdPath s l) : S.DR χ ω Y s = S.pathCoef χ ω Y l.reverse ∧ ∃ (b : R), S.fstNB χ l.reverse = some b ∧ S.TR χ b

Lemma 9.4, dual path form: along any ordinary path of a generating right-sided ray s, read from its end, d_s = Y_b + [p'], where p' is the two-sided suffix and b the last arrow which is not two-sided; this arrow exists and is right-sided.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.dPathR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (χ : L) (ω Y : R → ℤ) (s : R) : ℤ

d_s = Y_b + [p'], defined as in the manuscript: read backwards along a chosen ordinary path.

theorem MultiplicativeBasisDeformations.RaySys.Sys.dPathR_eq_DR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (ω Y : R → ℤ) {s : R} (hs : S.IsGen s) (hT : S.TR χ s) : S.dPathR χ ω Y s = S.DR χ ω Y s

The path definition of d_s is the coefficient DR used in the integral lifting.

theorem MultiplicativeBasisDeformations.RaySys.Sys.dPathR_prod {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) (ω Y : R → ℤ) (hω : ∀ (r s t : R), S.TB χ r → S.TB χ s → S.TB χ t → S.rr r * S.rr s = S.rr t → ω t = ω r + ω s) {r u v : R} (hr : S.IsGen r) (hT : S.TR χ r) (huv : S.rr u * S.rr v = S.rr r) (hv0 : v ≠ S.P.e (S.P.src v)) : (S.TR χ v → S.dPathR χ ω Y r = S.dPathR χ ω Y v) ∧ (S.TB χ v → S.dPathR χ ω Y r = S.dPathR χ ω Y u + ω v)

Lemma 9.4, product equations with generating right-sided output, for the path definition: d_t = d_v for a right-sided last factor, d_t = d_u + [v] for a two-sided one.

theorem MultiplicativeBasisDeformations.RaySys.Sys.lstNB_unique {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {χ : L} (k : Type u) [Field k] [IsAlgClosed k] (hfin : IsRepresentationFinite k ↥(S.P.Lin k)) (hχ : 0 < S.P.deg χ) (hprim : Prim χ) {s : R} (hs : S.IsGen s) (hT : S.TR χ s) {l l' : List R} (hl : S.IsOrdPath s l) (hl' : S.IsOrdPath s l') : S.fstNB χ l.reverse = S.fstNB χ l'.reverse

Lemma 9.4, dual: the last right-sided arrow of an ordinary path of a generating right-sided ray does not depend on the path.