Twisted traces of type E_6

Appendix A, "Type E_6 and the small-period exclusion" (periodic-mesh-calculations.tex). The arms have one, two and two vertices; x is the closed path along the short arm and p, q the others, so x + p + q = 0 and x² = p³ = q³ = 0. With v = p - q = x + 2p, "adding and subtracting the cubic relations gives x² = 0, v³ = -xvx, v²x + vxv + xv² = 0", and the words x, v; xv, vx, v²; xvx, xv², vxv; xvxv, vxv²; xvxv² span the positive part, with all words of degree six zero.

theorem MultiplicativeBasisDeformations.TraceAlg.e6_xv2x {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hrel : v ^ 2 * x + v * x * v + x * v ^ 2 = 0) : x * v ^ 2 * x = -(x * v * x * v)

theorem MultiplicativeBasisDeformations.TraceAlg.e6_vxvx {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hrel : v ^ 2 * x + v * x * v + x * v ^ 2 = 0) : v * x * v * x = x * v * x * v

theorem MultiplicativeBasisDeformations.TraceAlg.e6_xv3 {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hv3 : v ^ 3 = -(x * v * x)) : x * v ^ 3 = 0

theorem MultiplicativeBasisDeformations.TraceAlg.e6_v3x {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hv3 : v ^ 3 = -(x * v * x)) : v ^ 3 * x = 0

def MultiplicativeBasisDeformations.TraceAlg.e6Table {S : Type u_1} [Ring S] (x v : S) : ℕ → Set S

The spanning words of the corner, by word degree.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.TraceAlg.e6Span {S : Type u_1} [Ring S] (x v : S) (n : ℕ) : AddSubgroup S

Their additive span.

theorem MultiplicativeBasisDeformations.TraceAlg.e6_closed {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hv3 : v ^ 3 = -(x * v * x)) (hrel : v ^ 2 * x + v * x * v + x * v ^ 2 = 0) (n : ℕ) (w : S) (hw : w ∈ e6Table x v n) : w * x ∈ e6Span x v (n + 1) ∧ w * v ∈ e6Span x v (n + 1)

Closure under right multiplication (periodic-mesh-calculations.tex).

theorem MultiplicativeBasisDeformations.TraceAlg.e6Span_mul {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hv3 : v ^ 3 = -(x * v * x)) (hrel : v ^ 2 * x + v * x * v + x * v ^ 2 = 0) (n : ℕ) {w : S} (hw : w ∈ e6Span x v n) : w * x ∈ e6Span x v (n + 1) ∧ w * v ∈ e6Span x v (n + 1)

theorem MultiplicativeBasisDeformations.TraceAlg.e6Span_mul_one {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hv3 : v ^ 3 = -(x * v * x)) (hrel : v ^ 2 * x + v * x * v + x * v ^ 2 = 0) (n : ℕ) {w u : S} (hw : w ∈ e6Span x v n) (hu : u ∈ e6Span x v 1) : w * u ∈ e6Span x v (n + 1)

Right multiplication by an element of degree one.

theorem MultiplicativeBasisDeformations.TraceAlg.e6_prod_mem {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hv3 : v ^ 3 = -(x * v * x)) (hrel : v ^ 2 * x + v * x * v + x * v ^ 2 = 0) (l : List S) (hl : ∀ u ∈ l, u ∈ e6Span x v 1) : l.reverse.prod ∈ e6Span x v l.length

Products of n elements of degree one lie in the span of degree n.

theorem MultiplicativeBasisDeformations.TraceAlg.e6_psi4'x {S : Type u_1} [Ring S] (x v : S) (hx : x * x = 0) (hrel : v ^ 2 * x + v * x * v + x * v ^ 2 = 0) : v * x * v ^ 2 * x = -(x * v * x * v ^ 2)

theorem MultiplicativeBasisDeformations.TraceAlg.e6_derive {S : Type u_1} [Ring S] (x p q : S) (hp : p ^ 3 = 0) (hq : q ^ 3 = 0) (hs : x + p + q = 0) (c2 : ∀ (r : S), 2 * r = 0 → r = 0) (hx' : x * x = 0) : (p - q) ^ 3 = -(x * (p - q) * x) ∧ (p - q) ^ 2 * x + (p - q) * x * (p - q) + x * (p - q) ^ 2 = 0

Adding and subtracting the cubic relations (periodic-mesh-calculations.tex).

theorem MultiplicativeBasisDeformations.TraceAlg.pow_mul_prod_map {S : Type u_1} {α : Type u_2} [Ring S] (t : S) (ht : ∀ (r : S), Commute t r) (l : List α) (f : α → S) : t ^ l.length * (List.map f l).prod = (List.map (fun (i : α) => t * f i) l).prod

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.TraceAlg.vE6 {L : Fin 3 → ℕ} (b c : Fin 3) : R2 L

The corner element v = p - q.

theorem MultiplicativeBasisDeformations.TraceAlg.e6_sum {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) : y L a + y L b + y L c = 0

theorem MultiplicativeBasisDeformations.TraceAlg.e6_hx {L : Fin 3 → ℕ} {a : Fin 3} (hLa : L a = 0) : y L a * y L a = 0

theorem MultiplicativeBasisDeformations.TraceAlg.e6_rels {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 1) (hLc : L c = 1) : vE6 b c ^ 3 = -(y L a * vE6 b c * y L a) ∧ vE6 b c ^ 2 * y L a + vE6 b c * y L a * vE6 b c + y L a * vE6 b c ^ 2 = 0

The corner relations v³ = -xvx and v²x + vxv + xv² = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.e6_two_mem {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 1) (hLc : L c = 1) (i : Fin 3) : 2 * y L i ∈ e6Span (y L a) (vE6 b c) 1

theorem MultiplicativeBasisDeformations.TraceAlg.e6_word_mem {L : Fin 3 → ℕ} {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 1) (hLc : L c = 1) (w : List (Fin 3)) : 2 ^ w.length * (List.map (y L) w).prod ∈ e6Span (y L a) (vE6 b c) w.length

2^n times a word of length n lies in the span of degree n.

theorem MultiplicativeBasisDeformations.TraceAlg.tr2_self {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) (r : R2 L) : (D.tr2 h2) r = (D.tr2 h2) (D.tw2 r)

theorem MultiplicativeBasisDeformations.TraceAlg.tr2_nsmul_two_pow {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) (n : ℕ) (r : R2 L) : (D.tr2 h2) (2 ^ n * r) = 2 ^ n • (D.tr2 h2) r

theorem MultiplicativeBasisDeformations.TraceAlg.cancel_two_pow {M : Type u_1} [AddCommGroup M] (h2 : ∀ (m : M), m + m = 0 → m = 0) (n : ℕ) {m : M} (hm : 2 ^ n • m = 0) : m = 0

theorem MultiplicativeBasisDeformations.TraceAlg.e6_tr_of_span {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 1) (hLc : L c = 1) (P : M → Prop) (hsmul : ∀ (n : ℕ) (m : M), P (2 ^ n • m) → P m) (w : List (Fin 3)) (hspan : ∀ r ∈ e6Span (y L a) (vE6 b c) w.length, P ((D.tr2 h2) r)) : P (D.tr w)

Traces of words are determined by traces on the spanning set.

theorem MultiplicativeBasisDeformations.TraceAlg.tr2_zero_of_tw_neg {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {r : R2 L} (hr : D.tw2 r = -r) : (D.tr2 h2) r = 0

theorem MultiplicativeBasisDeformations.TraceAlg.tr2_zero_of_eq_neg {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {r : R2 L} (e : (D.tr2 h2) r = -(D.tr2 h2) r) : (D.tr2 h2) r = 0

theorem MultiplicativeBasisDeformations.TraceAlg.tr2_span_zero {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {X V : R2 L} (n : ℕ) (hgen : ∀ w ∈ e6Table X V n, (D.tr2 h2) w = 0) {r : R2 L} (hr : r ∈ e6Span X V n) : (D.tr2 h2) r = 0

theorem MultiplicativeBasisDeformations.TraceAlg.trace_E6_swap {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 1) (hLc : L c = 1) (hθa : D.θ a = a) (hθb : D.θ b = c) (hθc : D.θ c = b) (w : List (Fin 3)) (hw : 1 ≤ w.length) : D.tr w = 0

The reflection-twisted traces of E_6 vanish (periodic-mesh-calculations.tex).

theorem MultiplicativeBasisDeformations.TraceAlg.trace_E6_id {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 1) (hLc : L c = 1) (hθa : D.θ a = a) (hθb : D.θ b = b) (hθc : D.θ c = c) (w : List (Fin 3)) (hw : 1 ≤ w.length) : (w.length ≠ 3 → D.tr w = 0) ∧ 3 • D.tr w = 0

The ordinary traces of E_6 (periodic-mesh-calculations.tex): all positive traces vanish except possibly in word degree three, where they are killed by 3.