Corners of the ray linearization

For A₀ = kP in Setting 8.4: the corners e_x (kP) e_y are spanned by the rays from x to y; the rays of positive degree span a nilpotent subspace; a local corner element with nonzero identity coefficient is a unit, and the only idempotents of a local corner are 0 and e_x. Every nonzero corner element is u b_r w with endpoint units u, w and a ray r (the top of its support in the endpoint chain), and R_x b_s R_y is spanned by the rays of U(s). These are the facts behind "the basis vectors represent exactly the same endpoint-unit orbits" in the proof of Proposition 11.3(3) (binary-families.tex).

def MultiplicativeBasisDeformations.RaySys.Tab.corSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] (x y : V) : Submodule K ↥(P.Lin K)

The corner e_x (kP) e_y, spanned by the rays from x to y.

def MultiplicativeBasisDeformations.RaySys.Tab.degSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] (d : ℤ) : Submodule K ↥(P.Lin K)

The span of the rays of degree at least d.

theorem MultiplicativeBasisDeformations.RaySys.Tab.mem_corSp_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {x y : V} {a : ↥(P.Lin K)} : a ∈ P.corSp K x y ↔ ∀ (r : R), ((P.basis K).repr a) r ≠ 0 → P.src r = x ∧ P.tgt r = y

theorem MultiplicativeBasisDeformations.RaySys.Tab.mem_degSp_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {d : ℤ} {a : ↥(P.Lin K)} : a ∈ P.degSp K d ↔ ∀ (r : R), ((P.basis K).repr a) r ≠ 0 → d ≤ P.deg (P.wt r)

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_mem_corSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] (r : R) : P.b K r ∈ P.corSp K (P.src r) (P.tgt r)

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_mem_corSp' {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {r : R} {x y : V} (h1 : P.src r = x) (h2 : P.tgt r = y) : P.b K r ∈ P.corSp K x y

theorem MultiplicativeBasisDeformations.RaySys.Tab.b_mem_degSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {r : R} {d : ℤ} (h : d ≤ P.deg (P.wt r)) : P.b K r ∈ P.degSp K d

theorem MultiplicativeBasisDeformations.RaySys.Tab.degSp_mono {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {d d' : ℤ} (h : d ≤ d') : P.degSp K d' ≤ P.degSp K d

theorem MultiplicativeBasisDeformations.RaySys.Tab.mul_mem_degSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {d d' : ℤ} {a c : ↥(P.Lin K)} (ha : a ∈ P.degSp K d) (hc : c ∈ P.degSp K d') : a * c ∈ P.degSp K (d + d')

Degrees add under products.

theorem MultiplicativeBasisDeformations.RaySys.Tab.exists_deg_bound {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) : ∃ (D : ℕ), ∀ (r : R), P.deg (P.wt r) ≤ ↑D

A bound for the degrees of the rays.

theorem MultiplicativeBasisDeformations.RaySys.Tab.nilpotent_degSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] : ∃ (N : ℕ), ∀ n ∈ P.degSp K 1, n ^ N = 0

Rays of positive degree span a nilpotent subspace.

theorem MultiplicativeBasisDeformations.RaySys.Tab.e_mul_of_mem_corSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {x y : V} {a : ↥(P.Lin K)} (ha : a ∈ P.corSp K x y) : P.b K (P.e x) * a = a

theorem MultiplicativeBasisDeformations.RaySys.Tab.mul_e_of_mem_corSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {x y : V} {a : ↥(P.Lin K)} (ha : a ∈ P.corSp K x y) : a * P.b K (P.e y) = a

theorem MultiplicativeBasisDeformations.RaySys.Tab.e_mul_mul_e_mem {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] (x y : V) (a : ↥(P.Lin K)) : P.b K (P.e x) * a * P.b K (P.e y) ∈ P.corSp K x y

The corner of an element.

theorem MultiplicativeBasisDeformations.RaySys.Tab.local_decomp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {x : V} {a : ↥(P.Lin K)} (ha : a ∈ P.corSp K x x) : a - ((P.basis K).repr a) (P.e x) • P.b K (P.e x) ∈ P.corSp K x x ⊓ P.degSp K 1

A local corner element is its identity coefficient plus a positive part.

theorem MultiplicativeBasisDeformations.RaySys.Tab.repr_e_of_mem_degSp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {x : V} {n : ↥(P.Lin K)} (hn : n ∈ P.degSp K 1) : ((P.basis K).repr n) (P.e x) = 0

theorem MultiplicativeBasisDeformations.RaySys.Tab.idem_local {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {x : V} {a : ↥(P.Lin K)} (ha : a ∈ P.corSp K x x) (hidem : a * a = a) : a = 0 ∨ a = P.b K (P.e x)

The only idempotents of a local corner are 0 and e_x.

def MultiplicativeBasisDeformations.RaySys.Tab.IsLocUnit {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] (x : V) (u : ↥(P.Lin K)) : Prop

A unit of the local corner at x.

theorem MultiplicativeBasisDeformations.RaySys.Tab.isLocUnit_e {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] (x : V) : P.IsLocUnit K x (P.b K (P.e x))

theorem MultiplicativeBasisDeformations.RaySys.Tab.isLocUnit_of {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] {x : V} {c : K} (hc : c ≠ 0) {n : ↥(P.Lin K)} (hn : n ∈ P.corSp K x x ⊓ P.degSp K 1) : P.IsLocUnit K x (c • P.b K (P.e x) + n)

A local element with nonzero identity coefficient is a unit.

theorem MultiplicativeBasisDeformations.RaySys.Tab.sum_repr_b {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (P : Tab V R L) (K : Type u) [Field K] (a : ↥(P.Lin K)) : ∑ s : R, ((P.basis K).repr a) s • P.b K s = a

def MultiplicativeBasisDeformations.RaySys.Sys.USp {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (K : Type u) [Field K] (s : R) : Submodule K ↥(S.P.Lin K)

The span of the rays of U(s).

theorem MultiplicativeBasisDeformations.RaySys.Sys.vecM_mem_degSp {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] {d : ℤ} {x : M S.P.toMult} (hx : x = 0 ∨ ∃ (r : R), x = S.rr r) (h : ∀ (r : R), x = S.rr r → d ≤ S.P.deg (S.P.wt r)) : S.vecM K x ∈ S.P.degSp K d

theorem MultiplicativeBasisDeformations.RaySys.Sys.qpow_e_mem {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] {x : V} (j : ℕ) (hne : S.q x ^ j * S.rr (S.P.e x) ≠ S.rr (S.P.e x)) : S.vecM K (S.q x ^ j * S.rr (S.P.e x)) ∈ S.P.corSp K x x ⊓ S.P.degSp K 1

A local power times the identity is a positive local ray unless it is the identity.

theorem MultiplicativeBasisDeformations.RaySys.Sys.exists_unit_ray {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] {x y : V} {a : ↥(S.P.Lin K)} (ha : a ∈ S.P.corSp K x y) (ha0 : a ≠ 0) : ∃ (r : R), S.P.src r = x ∧ S.P.tgt r = y ∧ ∃ (u : ↥(S.P.Lin K)) (w : ↥(S.P.Lin K)), S.P.IsLocUnit K x u ∧ S.P.IsLocUnit K y w ∧ a = u * S.P.b K r * w

Every nonzero corner element is u b_r w with endpoint units (the top ray r of its support in the endpoint chain).

theorem MultiplicativeBasisDeformations.RaySys.Sys.inU_of_mem_USp {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] {r s : R} (h : S.P.b K r ∈ S.USp K s) : S.InU r s

theorem MultiplicativeBasisDeformations.RaySys.Sys.local_eq_qpow {V R L : Type} [AddCommGroup L] [DecidableEq L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {l : R} {x : V} (h1 : S.P.src l = x) (h2 : S.P.tgt l = x) : ∃ (j : ℕ), S.rr l = S.q x ^ j * S.rr (S.P.e x)

A local ray at x is a power of q_x times e_x.

theorem MultiplicativeBasisDeformations.RaySys.Sys.mul_mem_USp {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] {x y : V} {s : R} (hs1 : S.P.src s = x) (hs2 : S.P.tgt s = y) {u w : ↥(S.P.Lin K)} (hu : u ∈ S.P.corSp K x x) (hw : w ∈ S.P.corSp K y y) : u * S.P.b K s * w ∈ S.USp K s

R_x b_s R_y is spanned by the rays of U(s).