Proposition 8.12: the stem product

def:stem-product and prop:intrinsic-stem-product (local-ray-geometry.tex): for rays r : x → y, s : y → z, r * s = r q_y^n s for the least n with r q_y^n s ≠ 0, and 0 if there is none. In ray terms the endpoint subbimodule U_r is the set of rays q^i r q^j, and the product of the sets U_r U_s is U_{r*s} (stem_U). Hence the stem product is associative (stem_assoc), and it is the ray product when the latter is nonzero (stem_of_mul_ne).

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.stem {V R L : Type} [AddCommGroup L] [DecidableEq R] (S : Sys V R L) (r s : R) : M S.P.toMult

The stem product (prop:intrinsic-stem-product).

theorem MultiplicativeBasisDeformations.RaySys.Sys.stem_of_mul_ne {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r s : R} (h : S.rr r * S.rr s ≠ 0) : S.stem r s = S.rr r * S.rr s

def MultiplicativeBasisDeformations.RaySys.Sys.InProd {V R L : Type} [AddCommGroup L] (S : Sys V R L) (t r s : R) : Prop

t is a product of rays of U_r and U_s.

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_χ_nonneg {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) : 0 ≤ S.P.deg (S.χ x)

The degree of a power of a local generator is a nonnegative multiple.

theorem MultiplicativeBasisDeformations.RaySys.Sys.inProd_expand {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {t r s : R} (h : S.InProd t r s) : ∃ (i : ℕ) (m : ℕ) (l : ℕ), S.rr t = S.q (S.P.src r) ^ i * (S.rr r * S.q (S.P.tgt r) ^ m * S.rr s) * S.q (S.P.tgt s) ^ l

Expanding a product of elements of U_r and U_s.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.RaySys.Sys.degM {V R L : Type} [AddCommGroup L] (S : Sys V R L) (a : M S.P.toMult) : ℤ

The degree of a nonzero element.

theorem MultiplicativeBasisDeformations.RaySys.Sys.degM_mul {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {a b : M S.P.toMult} (h : a * b ≠ 0) : S.degM (a * b) = S.degM a + S.degM b

theorem MultiplicativeBasisDeformations.RaySys.Sys.degM_qpow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {n : ℕ} (h : S.q x ^ n ≠ 0) : S.degM (S.q x ^ n) = ↑n * S.P.deg (S.χ x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.degM_qpow_nonneg {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {n : ℕ} (h : S.q x ^ n ≠ 0) : 0 ≤ S.degM (S.q x ^ n)

theorem MultiplicativeBasisDeformations.RaySys.Sys.degM_rr {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : S.degM (S.rr r) = S.P.deg (S.P.wt r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.stem_U {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s : R) : (S.stem r s = 0 ∧ ∀ (t : R), ¬S.InProd t r s) ∨ ∃ (w : R), S.stem r s = S.rr w ∧ ∀ (t : R), S.InProd t r s ↔ S.InU t w

U_r U_s = U_{r * s} (the key step of Proposition 8.12).

def MultiplicativeBasisDeformations.RaySys.Sys.UM {V R L : Type} [AddCommGroup L] (S : Sys V R L) (x : M S.P.toMult) (t : R) : Prop

Membership in the endpoint subbimodule of an element (zero or a ray).

theorem MultiplicativeBasisDeformations.RaySys.Sys.stem_cases {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s : R) : S.stem r s = 0 ∨ ∃ (w : R), S.stem r s = S.rr w

theorem MultiplicativeBasisDeformations.RaySys.Sys.UM_stem {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s t : R) : S.UM (S.stem r s) t ↔ S.InProd t r s

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_of_UM {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x y : M S.P.toMult} (hx : x = 0 ∨ ∃ (w : R), x = S.rr w) (hy : y = 0 ∨ ∃ (w : R), y = S.rr w) (h : ∀ (t : R), S.UM x t ↔ S.UM y t) : x = y

Elements with the same endpoint subbimodule are equal.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.stemL {V R L : Type} [AddCommGroup L] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : M S.P.toMult) (u : R) : M S.P.toMult

The stem product of an element with a ray.

noncomputable def MultiplicativeBasisDeformations.RaySys.Sys.stemR {V R L : Type} [AddCommGroup L] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) (y : M S.P.toMult) : M S.P.toMult

The stem product of a ray with an element.

theorem MultiplicativeBasisDeformations.RaySys.Sys.stemL_rr {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (w u : R) : S.stemL (S.rr w) u = S.stem w u

theorem MultiplicativeBasisDeformations.RaySys.Sys.stemR_rr {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r w : R) : S.stemR r (S.rr w) = S.stem r w

def MultiplicativeBasisDeformations.RaySys.Sys.InProd3 {V R L : Type} [AddCommGroup L] (S : Sys V R L) (t r s u : R) : Prop

Triple products of the endpoint subbimodules.

theorem MultiplicativeBasisDeformations.RaySys.Sys.UM_stemL {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s u t : R) : S.UM (S.stemL (S.stem r s) u) t ↔ S.InProd3 t r s u

theorem MultiplicativeBasisDeformations.RaySys.Sys.UM_stemR {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s u t : R) : S.UM (S.stemR r (S.stem s u)) t ↔ S.InProd3 t r s u

theorem MultiplicativeBasisDeformations.RaySys.Sys.stemL_cases {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : M S.P.toMult) (u : R) : S.stemL x u = 0 ∨ ∃ (w : R), S.stemL x u = S.rr w

theorem MultiplicativeBasisDeformations.RaySys.Sys.stemR_cases {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) (y : M S.P.toMult) : S.stemR r y = 0 ∨ ∃ (w : R), S.stemR r y = S.rr w

theorem MultiplicativeBasisDeformations.RaySys.Sys.stem_assoc {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s u : R) : S.stemL (S.stem r s) u = S.stemR r (S.stem s u)

The stem product is associative (Proposition 8.12).