Setting 8.4: local generators and endpoint chains of a ray table

set:projective-companion: A₀ = kP with its normed homogeneous ray basis; each local ring is R_x = k[q_x]/(q_x^{N_x}) with q_x a ray (or q_x = 0 when R_x = k), and by Lemma 3.1(3) the endpoint subbimodules of each Hom form a chain, each generated over one endpoint ring (lem:endpoint-chains). In ray terms:

• q x is 0 or a nonidentity loop at x, and every loop at x is q x ^ j e_x;
• for each ray r, every ray q^i r q^j equals q^i' r for all such, or r q^j' for all such (one-sided generation);
• the rays of each Hom form a chain under s ∈ U(r).

Sys bundles a ray table with this structure. Products are computed in the monoid with zero M P; we write ⌜r⌝ for a ray in it.

structure MultiplicativeBasisDeformations.RaySys.Sys (V R L : Type) [AddCommGroup L] : Type

Setting 8.4 for a ray table.

• P : Tab V R L
• q : V → M self.P.toMult
• q_cases (x : V) : self.q x = 0 ∨ ∃ (g : R), self.q x = self.P.rr g ∧ self.P.src g = x ∧ self.P.tgt g = x ∧ g ≠ self.P.e x
• q_pow (r : R) : self.P.src r = self.P.tgt r → ∃ (j : ℕ), self.q (self.P.src r) ^ j * self.P.rr (self.P.e (self.P.src r)) = self.P.rr r
• cyc (r : R) : (∀ (i j : ℕ), self.q (self.P.src r) ^ i * self.P.rr r * self.q (self.P.tgt r) ^ j ≠ 0 → ∃ (i' : ℕ), self.q (self.P.src r) ^ i * self.P.rr r * self.q (self.P.tgt r) ^ j = self.q (self.P.src r) ^ i' * self.P.rr r) ∨ ∀ (i j : ℕ), self.q (self.P.src r) ^ i * self.P.rr r * self.q (self.P.tgt r) ^ j ≠ 0 → ∃ (j' : ℕ), self.q (self.P.src r) ^ i * self.P.rr r * self.q (self.P.tgt r) ^ j = self.P.rr r * self.q (self.P.tgt r) ^ j'
• chain (r s : R) : self.P.src r = self.P.src s → self.P.tgt r = self.P.tgt s → (∃ (i : ℕ) (j : ℕ), self.P.rr r = self.q (self.P.src r) ^ i * self.P.rr s * self.q (self.P.tgt r) ^ j) ∨ ∃ (i : ℕ) (j : ℕ), self.P.rr s = self.q (self.P.src r) ^ i * self.P.rr r * self.q (self.P.tgt r) ^ j

@[reducible, inline]

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

A ray as an element of the monoid with zero.

Elements of the monoid with zero

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

The weight of an element (zero on 0 and 1).

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

theorem MultiplicativeBasisDeformations.RaySys.Sys.wtM_one {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) : S.wtM 1 = 0

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

theorem MultiplicativeBasisDeformations.RaySys.Sys.rr_ne {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : S.rr r ≠ 0

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

theorem MultiplicativeBasisDeformations.RaySys.Sys.ray_of_mul_ne {V R L : Type} [AddCommGroup 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) : ∃ (t : R), S.rr r * S.rr s = S.rr t

theorem MultiplicativeBasisDeformations.RaySys.Sys.mul_left_ray {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r : R} {a : M S.P.toMult} (h : S.rr r * a ≠ 0) : ∃ (t : R), S.rr r * a = S.rr t

theorem MultiplicativeBasisDeformations.RaySys.Sys.mul_right_ray {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r : R} {a : M S.P.toMult} (h : a * S.rr r ≠ 0) : ∃ (t : R), a * S.rr r = S.rr t

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

theorem MultiplicativeBasisDeformations.RaySys.Sys.e_mul_rr {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : S.rr (S.P.e (S.P.src r)) * S.rr r = S.rr r

theorem MultiplicativeBasisDeformations.RaySys.Sys.rr_mul_e {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : S.rr r * S.rr (S.P.e (S.P.tgt r)) = S.rr r

theorem MultiplicativeBasisDeformations.RaySys.Sys.e_mul_rr' {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) {x : V} (h : S.P.src r = x) : S.rr (S.P.e x) * S.rr r = S.rr r

theorem MultiplicativeBasisDeformations.RaySys.Sys.e_mul_rr_of_ne {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {r : R} (h : x ≠ S.P.src r) : S.rr (S.P.e x) * S.rr r = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.rr_mul_e_of_ne {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {x : V} {r : R} (h : x ≠ S.P.tgt r) : S.rr r * S.rr (S.P.e x) = 0

theorem MultiplicativeBasisDeformations.RaySys.Sys.prod_of {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r s t : R} (h : S.rr r * S.rr s = S.rr t) : S.P.src t = S.P.src r ∧ S.P.tgt t = S.P.tgt s ∧ S.P.tgt r = S.P.src s ∧ S.P.wt t = S.P.wt r + S.P.wt s

A nonzero product of rays: endpoints and weight.

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

Left cancellation of nonzero products.

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

Right cancellation of nonzero products.

Local generators

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

The weight of the local generator (0 when R_x = k).

theorem MultiplicativeBasisDeformations.RaySys.Sys.q_mul_e {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) : S.q x * S.rr (S.P.e x) = S.q x

theorem MultiplicativeBasisDeformations.RaySys.Sys.e_mul_q {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) : S.rr (S.P.e x) * S.q x = S.q x

theorem MultiplicativeBasisDeformations.RaySys.Sys.e_mul_qpow {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) (j : ℕ) : S.rr (S.P.e x) * S.q x ^ j * S.rr (S.P.e x) = S.q x ^ j * S.rr (S.P.e x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.qpow_comm_e {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) (j : ℕ) : S.q x ^ j * S.rr (S.P.e x) = S.rr (S.P.e x) * S.q x ^ j

theorem MultiplicativeBasisDeformations.RaySys.Sys.qpow_cases {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) (j : ℕ) : S.q x ^ j * S.rr (S.P.e x) = 0 ∨ ∃ (g : R), S.q x ^ j * S.rr (S.P.e x) = S.rr g ∧ S.P.src g = x ∧ S.P.tgt g = x ∧ S.P.wt g = j • S.χ x

Powers of the local generator are zero or loops of weight j χ_x.

theorem MultiplicativeBasisDeformations.RaySys.Sys.qpow_mul_rr_mul_qpow {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) (i j : ℕ) : S.q (S.P.src r) ^ i * S.rr r * S.q (S.P.tgt r) ^ j = 0 ∨ ∃ (t : R), S.q (S.P.src r) ^ i * S.rr r * S.q (S.P.tgt r) ^ j = S.rr t ∧ S.P.src t = S.P.src r ∧ S.P.tgt t = S.P.tgt r ∧ S.P.wt t = i • S.χ (S.P.src r) + S.P.wt r + j • S.χ (S.P.tgt r)

The weight of a nonzero product of a ray with powers of the local generators.

theorem MultiplicativeBasisDeformations.RaySys.Sys.local_eq {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) (h : S.P.src r = S.P.tgt r) : ∃ (j : ℕ), S.q (S.P.src r) ^ j * S.rr (S.P.e (S.P.src r)) = S.rr r ∧ S.P.wt r = j • S.χ (S.P.src r)

Local rays are powers of the local generator.

theorem MultiplicativeBasisDeformations.RaySys.Sys.χ_deg_pos {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) (hq : S.q x ≠ 0) : 0 < S.P.deg (S.χ x)

theorem MultiplicativeBasisDeformations.RaySys.Sys.χ_eq_zero {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) (hq : S.q x = 0) : S.χ x = 0

Endpoint subbimodules and generating rays

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

s ∈ U(r): s = q^i r q^j.

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

Generating rays (def:generating-rays(1)): every ray of the Hom lies in U(r).

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

The Hom of a ray is cyclic at its source, generated by it.

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

The Hom of a ray is cyclic at its target, generated by it.

theorem MultiplicativeBasisDeformations.RaySys.Sys.inU_endpoints {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {s r : R} (h : S.InU s r) : S.P.src s = S.P.src r ∧ S.P.tgt s = S.P.tgt r ∧ ∃ (i : ℕ) (j : ℕ), S.P.wt s = i • S.χ (S.P.src r) + S.P.wt r + j • S.χ (S.P.tgt r) ∧ (0 < i → S.q (S.P.src r) ≠ 0) ∧ (0 < j → S.q (S.P.tgt r) ≠ 0)

theorem MultiplicativeBasisDeformations.RaySys.Sys.nsmul_χ_deg {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) (i : ℕ) (h : 0 < i → S.q x ≠ 0) : 0 ≤ S.P.deg (i • S.χ x) ∧ (S.P.deg (i • S.χ x) = 0 → i = 0)

theorem MultiplicativeBasisDeformations.RaySys.Sys.deg_le_of_inU {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {s r : R} (h : S.InU s r) : S.P.deg (S.P.wt r) ≤ S.P.deg (S.P.wt s) ∧ (S.P.deg (S.P.wt s) = S.P.deg (S.P.wt r) → s = r)

Elements of U(r) have degree at least that of r, with equality only for r.

theorem MultiplicativeBasisDeformations.RaySys.Sys.inU_refl {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : S.InU r r

theorem MultiplicativeBasisDeformations.RaySys.Sys.inU_trans {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {s r t : R} (h1 : S.InU s r) (h2 : S.InU r t) : S.InU s t

theorem MultiplicativeBasisDeformations.RaySys.Sys.inU_antisymm {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {s r : R} (h1 : S.InU s r) (h2 : S.InU r s) : s = r

theorem MultiplicativeBasisDeformations.RaySys.Sys.inU_total {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {s r : R} (h1 : S.P.src s = S.P.src r) (h2 : S.P.tgt s = S.P.tgt r) : S.InU s r ∨ S.InU r s

theorem MultiplicativeBasisDeformations.RaySys.Sys.exists_gen {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r : R) : ∃ (f : R), S.P.src f = S.P.src r ∧ S.P.tgt f = S.P.tgt r ∧ S.IsGen f

Every nonzero Hom has a generating ray (the top of the endpoint chain).

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_unique {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f f' : R} (hf : S.IsGen f) (hf' : S.IsGen f') (h1 : S.P.src f = S.P.src f') (h2 : S.P.tgt f = S.P.tgt f') : f = f'

theorem MultiplicativeBasisDeformations.RaySys.Sys.gen_cyc {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (hf : S.IsGen f) : S.CycL f ∨ S.CycR f

A generating ray generates its Hom over one endpoint (Lemma 3.1(3)).

theorem MultiplicativeBasisDeformations.RaySys.Sys.isGen_of_cycL {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (h : S.CycL f) : S.IsGen f

theorem MultiplicativeBasisDeformations.RaySys.Sys.isGen_of_cycR {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {f : R} (h : S.CycR f) : S.IsGen f

Weights of elements

theorem MultiplicativeBasisDeformations.RaySys.Sys.wtM_mul {V R L : Type} [AddCommGroup 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.wtM (a * b) = S.wtM a + S.wtM b

theorem MultiplicativeBasisDeformations.RaySys.Sys.wtM_pow {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (a : M S.P.toMult) (n : ℕ) (h : a ^ n ≠ 0) : S.wtM (a ^ n) = n • S.wtM a

theorem MultiplicativeBasisDeformations.RaySys.Sys.wtM_qpow {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (x : V) (n : ℕ) (h : S.q x ^ n ≠ 0) : S.wtM (S.q x ^ n) = n • S.χ x

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_rr_of_ne {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (a : M S.P.toMult) (h0 : a ≠ 0) (h1 : a ≠ 1) : ∃ (r : R), a = S.rr r

theorem MultiplicativeBasisDeformations.RaySys.Sys.rf_deg_le {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r s : R} (h : S.P.RF r s) : S.P.deg (S.P.wt r) ≤ S.P.deg (S.P.wt s)

theorem MultiplicativeBasisDeformations.RaySys.Sys.lf_deg_le {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r s : R} (h : S.P.LF r s) : S.P.deg (S.P.wt s) ≤ S.P.deg (S.P.wt r)

theorem MultiplicativeBasisDeformations.RaySys.Sys.rf_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s : R) : S.P.RF r s ↔ ∃ (v : R), S.rr r * S.rr v = S.rr s

theorem MultiplicativeBasisDeformations.RaySys.Sys.lf_iff {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) (r s : R) : S.P.LF r s ↔ ∃ (v : R), S.rr v * S.rr s = S.rr r

theorem MultiplicativeBasisDeformations.RaySys.Sys.src_of_mul_ne {V R L : Type} [AddCommGroup 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.P.tgt r = S.P.src s

theorem MultiplicativeBasisDeformations.RaySys.Sys.eq_e_of_deg_zero {V R L : Type} [AddCommGroup L] [Fintype V] [DecidableEq V] [Fintype R] [DecidableEq R] (S : Sys V R L) {r : R} (h : S.P.deg (S.P.wt r) = 0) : r = S.P.e (S.P.src r)

A loop of degree zero is the identity.