Ray tables (Part III, Setting 8.4)

The local arguments of Part III (local-ray-geometry.tex, primitive-ray-equations.tex, integral-partial-lifts.tex, local-ray-restrictions.tex) concern the normed homogeneous ray basis of A₀ = kP (set:projective-companion): products of rays are rays or zero, every ray has a weight in the lattice L, the categorical degree is positive on nonidentity rays, and a ray is determined by its endpoints and weight.

We record this as an abstract finite table Tab: rays with source and target, identities, a partial associative product, weights and a degree. The rays together with a formal unit and a zero form a monoid with zero M P, in which all products of the paper are computed.

structure MultiplicativeBasisDeformations.RaySys.Mult (V R : Type) : Type

A table of rays with a partial associative product and identities.

• src : R → V
• tgt : R → V
• e : V → R
• src_e (x : V) : self.src (self.e x) = x
• tgt_e (x : V) : self.tgt (self.e x) = x
• mul : R → R → Option R
• mul_src (r s t : R) : self.mul r s = some t → self.src t = self.src r
• mul_tgt (r s t : R) : self.mul r s = some t → self.tgt t = self.tgt s
• mul_mid (r s t : R) : self.mul r s = some t → self.tgt r = self.src s
• e_mul (r : R) : self.mul (self.e (self.src r)) r = some r
• mul_e (r : R) : self.mul r (self.e (self.tgt r)) = some r
• assoc (r s u : R) : ((self.mul r s).bind fun (t : R) => self.mul t u) = (self.mul s u).bind fun (t : R) => self.mul r t

structure MultiplicativeBasisDeformations.RaySys.Tab (V R L : Type) [AddCommGroup L] extends MultiplicativeBasisDeformations.RaySys.Mult V R : Type

A finite ray table: a Mult with weights in L and a positive degree, the weight determining a ray with given endpoints.

• src : R → V
• tgt : R → V
• e : V → R
• src_e (x : V) : self.src (self.e x) = x
• tgt_e (x : V) : self.tgt (self.e x) = x
• mul : R → R → Option R
• mul_src (r s t : R) : self.mul r s = some t → self.src t = self.src r
• mul_tgt (r s t : R) : self.mul r s = some t → self.tgt t = self.tgt s
• mul_mid (r s t : R) : self.mul r s = some t → self.tgt r = self.src s
• e_mul (r : R) : self.mul (self.e (self.src r)) r = some r
• mul_e (r : R) : self.mul r (self.e (self.tgt r)) = some r
• assoc (r s u : R) : ((self.mul r s).bind fun (t : R) => self.mul t u) = (self.mul s u).bind fun (t : R) => self.mul r t
• wt : R → L
• wt_mul (r s t : R) : self.mul r s = some t → self.wt t = self.wt r + self.wt s
• deg : L →+ ℤ
• deg_pos (r : R) : r ≠ self.e (self.src r) → 0 < self.deg (self.wt r)
• sep (r r' : R) : self.src r = self.src r' → self.tgt r = self.tgt r' → self.wt r = self.wt r' → r = r'

inductive MultiplicativeBasisDeformations.RaySys.Elt (R : Type) : Type

Rays with a formal unit and a zero.

• one {R : Type} : Elt R
• zero {R : Type} : Elt R
• ray {R : Type} : R → Elt R

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.instDecidableEqElt {R✝ : Type} [DecidableEq R✝] : DecidableEq (Elt R✝)

def MultiplicativeBasisDeformations.RaySys.instDecidableEqElt.decEq {R✝ : Type} [DecidableEq R✝] (x✝ x✝¹ : Elt R✝) : Decidable (x✝ = x✝¹)

def MultiplicativeBasisDeformations.RaySys.M {V R : Type} (_P : Mult V R) : Type

The monoid with zero of a ray table.

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.instDecidableEqM {V R : Type} (P : Mult V R) [DecidableEq R] : DecidableEq (M P)

def MultiplicativeBasisDeformations.RaySys.Mult.emul {V R : Type} (P : Mult V R) : Elt R → Elt R → Elt R

The product of the monoid with zero.

theorem MultiplicativeBasisDeformations.RaySys.Mult.emul_ray {V R : Type} (P : Mult V R) (r s : R) : P.emul (Elt.ray r) (Elt.ray s) = (P.mul r s).elim Elt.zero Elt.ray

theorem MultiplicativeBasisDeformations.RaySys.Mult.emul_one {V R : Type} (P : Mult V R) (a : Elt R) : P.emul a Elt.one = a

theorem MultiplicativeBasisDeformations.RaySys.Mult.emul_zero {V R : Type} (P : Mult V R) (a : Elt R) : P.emul a Elt.zero = Elt.zero

theorem MultiplicativeBasisDeformations.RaySys.Mult.emul_assoc {V R : Type} (P : Mult V R) (a b c : Elt R) : P.emul (P.emul a b) c = P.emul a (P.emul b c)

@[instance_reducible]

instance MultiplicativeBasisDeformations.RaySys.instMonoidWithZeroM {V R : Type} (P : Mult V R) : MonoidWithZero (M P)

def MultiplicativeBasisDeformations.RaySys.Mult.rr {V R : Type} (P : Mult V R) (r : R) : M P

A ray as an element of the monoid with zero.

theorem MultiplicativeBasisDeformations.RaySys.Mult.one_def {V R : Type} (P : Mult V R) : 1 = Elt.one

theorem MultiplicativeBasisDeformations.RaySys.Mult.zero_def {V R : Type} (P : Mult V R) : 0 = Elt.zero

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_mul_rr {V R : Type} (P : Mult V R) (r s : R) : P.rr r * P.rr s = (P.mul r s).elim 0 P.rr

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_ne_zero {V R : Type} (P : Mult V R) (r : R) : P.rr r ≠ 0

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_ne_one {V R : Type} (P : Mult V R) (r : R) : P.rr r ≠ 1

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_injective {V R : Type} (P : Mult V R) : Function.Injective P.rr

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_mul_rr_eq_rr {V R : Type} (P : Mult V R) {r s t : R} : P.rr r * P.rr s = P.rr t ↔ P.mul r s = some t

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_mul_rr_eq_zero {V R : Type} (P : Mult V R) {r s : R} : P.rr r * P.rr s = 0 ↔ P.mul r s = none

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_inj {V R : Type} (P : Mult V R) {r s : R} : P.rr r = P.rr s ↔ r = s

theorem MultiplicativeBasisDeformations.RaySys.Mult.cases_elt {V R : Type} (P : Mult V R) (a : M P) : a = 1 ∨ a = 0 ∨ ∃ (r : R), a = P.rr r

Every element is the unit, zero, or a ray.

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_mul_rr_ne_zero {V R : Type} (P : Mult V R) {r s : R} (h : P.rr r * P.rr s ≠ 0) : ∃ (t : R), P.mul r s = some t ∧ P.rr r * P.rr s = P.rr t

theorem MultiplicativeBasisDeformations.RaySys.Mult.mul_eq_rr_of {V R : Type} (P : Mult V R) {r s t : R} (h : P.rr r * P.rr s = P.rr t) : P.src t = P.src r ∧ P.tgt t = P.tgt s ∧ P.tgt r = P.src s

theorem MultiplicativeBasisDeformations.RaySys.Mult.e_mul_rr {V R : Type} (P : Mult V R) (r : R) : P.rr (P.e (P.src r)) * P.rr r = P.rr r

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_mul_e {V R : Type} (P : Mult V R) (r : R) : P.rr r * P.rr (P.e (P.tgt r)) = P.rr r

theorem MultiplicativeBasisDeformations.RaySys.Mult.rr_mul_rr_eq_zero_of_ne {V R : Type} (P : Mult V R) {r s : R} (h : P.tgt r ≠ P.src s) : P.rr r * P.rr s = 0

Weights and degrees

theorem MultiplicativeBasisDeformations.RaySys.Tab.wt_of_mul {V R L : Type} [AddCommGroup L] (P : Tab V R L) {r s t : R} (h : P.rr r * P.rr s = P.rr t) : P.wt t = P.wt r + P.wt s

theorem MultiplicativeBasisDeformations.RaySys.Tab.wt_e {V R L : Type} [AddCommGroup L] (P : Tab V R L) (x : V) : P.wt (P.e x) = 0

theorem MultiplicativeBasisDeformations.RaySys.Tab.deg_nonneg {V R L : Type} [AddCommGroup L] (P : Tab V R L) (r : R) : 0 ≤ P.deg (P.wt r)

theorem MultiplicativeBasisDeformations.RaySys.Tab.eq_e_of_deg {V R L : Type} [AddCommGroup L] (P : Tab V R L) {r : R} (h : P.deg (P.wt r) = 0) : r = P.e (P.src r)

theorem MultiplicativeBasisDeformations.RaySys.Tab.eq_e_of_wt {V R L : Type} [AddCommGroup L] (P : Tab V R L) {r : R} (h : P.wt r = 0) : r = P.e (P.src r)

theorem MultiplicativeBasisDeformations.RaySys.Tab.tgt_of_eq_e {V R L : Type} [AddCommGroup L] (P : Tab V R L) {r : R} (h : r = P.e (P.src r)) : P.tgt r = P.src r

def MultiplicativeBasisDeformations.RaySys.Tab.IsId {V R L : Type} [AddCommGroup L] (P : Tab V R L) (r : R) : Prop

A nonidentity ray: its degree is positive.