Lemma A.6 over any coefficient ring

lem:e78-traces (periodic-mesh-calculations.tex). Over any commutative coefficient ring, with a = yx³, b = yx⁴, t_j = [yx^j]:

(1) the positive part of T₅ is spanned by t₁, t₂, t₃, t₄, [a²], [abʳ] (r ≥ 1) (span_all), with 2t₁ = 2t₃ = 0, 3t₂ = 0, 5t₄ = 0, 2[a²] = 0, 3[ab] = 0, 2[abʳ] = 0 (r ≥ 2) (t1_two, t3_two, t2_three, t4_five, a2_two, ab_three, abr_two); for nonempty W in a, b: [a²W] = 0, [abW] = -[baW], and [b^q] = 0 (q ≥ 2) (aa, ab_ba, bq);

(2) if two is invertible, (T₅)₊ is spanned by [yx²], [yx⁴], [(yx³)(yx⁴)], annihilated by 3, 5, 3, and (T₄)₊ (impose x⁴ = 0) by [yx²], annihilated by 3 (span_two, span_two_E7).

The proof is that of the source: the gap reductions (red0, red1, red2) lower the number of y's; a gap two between gaps of length at least three has zero trace (gap2); the identity F multiplied by x^k W gives the block relations (Fk). As usual we work with an additive map tr killing commutators and positive powers of x, y; T_m is the universal such map. The char-two-free statements in TraceE78.lean are the case two invertible.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.blk_zero_of_mem {S : Type u_1} [Ring S] {x y : S} (g : List ℕ) (e : ℕ) (he : e ∈ g) (hx : x ^ e = 0) : E78.blk x y g = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.xpow_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) {e : ℕ} (he : 5 ≤ e) : x ^ e = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.blk_zero_big {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (g : List ℕ) (e : ℕ) (he : e ∈ g) (h5 : 5 ≤ e) : E78.blk x y g = 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.tr_bump_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (g₀ : List ℕ) (h j : ℕ) (hb : 5 ≤ h + j) : tr (x ^ j * E78.blk x y (g₀ ++ [h])) = 0

A leading power x^j rotated into the last gap of a word with a large last gap.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.Fk {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (k : ℕ) (g : List ℕ) : E78.blk x y (3 :: (k + 1) :: g) = -E78.blk x y (4 :: k :: g) - x ^ 1 * E78.blk x y (3 :: k :: g) + x ^ 2 * E78.blk x y ((k + 3) :: g) + x ^ 3 * E78.blk x y ((k + 2) :: g)

The identity F x^k W.

Gap two

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.gap2 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (q p : ℕ) (U : List ℕ) (hq : 3 ≤ q) (hp : 3 ≤ p) : tr (E78.blk x y (2 :: q :: (U ++ [p]))) = 0

A gap two between gaps of length at least three has zero trace.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.gap2' {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (q : ℕ) (hq : 3 ≤ q) : tr (E78.blk x y [2, q]) = 0

Block relations

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.aa {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (g : List ℕ) (hne : g ≠ []) (hg : ∀ e ∈ g, 3 ≤ e) : tr (E78.blk x y (3 :: 3 :: g)) = 0

[a²W] = 0 for nonempty W with all gaps at least three.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.bc {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) : tr (E78.blk x y [4, 2]) = 0

[bc] = [yx⁴yx²] = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.a2_two {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) : tr (E78.blk x y [3, 3]) + tr (E78.blk x y [3, 3]) = 0

2[a²] = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.ab_ba {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (g : List ℕ) (hne : g ≠ []) (hg : ∀ e ∈ g, 3 ≤ e) : tr (E78.blk x y (3 :: 4 :: g)) = -tr (E78.blk x y (4 :: 3 :: g))

[abW] = -[baW] for nonempty W with all gaps at least three.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.ab_three {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) : tr (E78.blk x y [3, 4]) + tr (E78.blk x y [3, 4]) + tr (E78.blk x y [3, 4]) = 0

3[ab] = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.bq {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (r : ℕ) : tr (E78.blk x y (List.replicate (r + 2) 4)) = 0

[b^{r+2}] = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.abr_two {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (r : ℕ) : tr (E78.blk x y (3 :: List.replicate (r + 2) 4)) + tr (E78.blk x y (3 :: List.replicate (r + 2) 4)) = 0

2[abʳ] = 0 for r ≥ 2.

The one-y relations

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.tr_comm {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (p q : S) : tr (p * q) = tr (q * p)

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.t1_two {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) : tr (E78.blk x y [1]) + tr (E78.blk x y [1]) = 0

2t₁ = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.t2_three {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) : tr (E78.blk x y [2]) + tr (E78.blk x y [2]) + tr (E78.blk x y [2]) = 0

3t₂ = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.t3_two {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) : tr (E78.blk x y [3]) + tr (E78.blk x y [3]) = 0

2t₃ = 0.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.t4_five {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) : tr (E78.blk x y [4]) + tr (E78.blk x y [4]) + tr (E78.blk x y [4]) + tr (E78.blk x y [4]) + tr (E78.blk x y [4]) = 0

5t₄ = 0, from the trace of the third identity multiplied by x.

Spanning

def MultiplicativeBasisDeformations.TraceAlg.E78i.cand {S : Type u_1} [Ring S] (x y : S) {M : Type u_2} [AddCommGroup M] (tr : S →+ M) : Set M

The candidate classes t₁, t₂, t₃, t₄, [a²], [abʳ] (r ≥ 1).

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.TraceAlg.E78i.A {S : Type u_1} [Ring S] (x y : S) {M : Type u_2} [AddCommGroup M] (tr : S →+ M) : AddSubgroup M

Their span.

def MultiplicativeBasisDeformations.TraceAlg.E78i.Zs {S : Type u_1} [Ring S] (x y : S) {M : Type u_2} [AddCommGroup M] (tr : S →+ M) (K : ℕ) : Prop

All words with at most K letters y and positive degree have trace in A.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.mem_A {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} {m : M} (h : m ∈ cand x y tr) : m ∈ A x y tr

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.Zs_zero {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) : Zs x y tr 0

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.single {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (h : ℕ) : tr (E78.blk x y [h]) ∈ A x y tr

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.bad_mem {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) {K : ℕ} (hZ : Zs x y tr K) (g : List ℕ) (hg : g.length = K + 1) (hK : 1 ≤ K) (e : ℕ) (he : e ∈ g) (hbad : e ≤ 2 ∨ 5 ≤ e) : tr (E78.blk x y g) ∈ A x y tr

A gap of length at most two, or at least five, reduces to fewer y's.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.chain {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (r : ℕ) (g : List ℕ) (hg : ∀ e ∈ g, e = 3 ∨ e = 4) (hne : r ≠ 0 ∨ g ≠ []) : tr (E78.blk x y (3 :: (List.replicate r 4 ++ 3 :: g))) = 0

Two a's are brought together using [abW] = -[baW].

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.blocks_mem {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (g : List ℕ) (hg : ∀ e ∈ g, e = 3 ∨ e = 4) (hlen : 2 ≤ g.length) : tr (E78.blk x y g) ∈ A x y tr

Cyclic words in a, b with at least two blocks.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.all_mem {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (K : ℕ) : Zs x y tr K

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.span_all {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (j : ℕ) (g : List ℕ) (hj : g = [] → 1 ≤ j) : tr (x ^ j * E78.blk x y g) ∈ A x y tr

Lemma A.6(1), spanning: every word of positive degree has trace in the span of t₁, t₂, t₃, t₄, [a²], [abʳ] (r ≥ 1).

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.span_mem {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (n : ℕ) (hn : 1 ≤ n) {r : S} (hr : r ∈ E78.span x y n) : tr r ∈ A x y tr

The same for every element of the span of the words of a positive degree n.

Two invertible

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.TraceAlg.E78i.A2 {S : Type u_1} [Ring S] (x y : S) {M : Type u_2} [AddCommGroup M] (tr : S →+ M) : AddSubgroup M

The span of [yx²], [yx⁴], [(yx³)(yx⁴)].

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.span_two {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (two : ∀ (m : M), m + m = 0 → m = 0) (j : ℕ) (g : List ℕ) (hj : g = [] → 1 ≤ j) : tr (x ^ j * E78.blk x y g) ∈ A2 x y tr ∧ 3 • tr (E78.blk x y [2]) = 0 ∧ 5 • tr (E78.blk x y [4]) = 0 ∧ 3 • tr (E78.blk x y [3, 4]) = 0

Lemma A.6(2): if two is invertible, (T₅)₊ is spanned by [yx²], [yx⁴], [(yx³)(yx⁴)], annihilated by 3, 5, 3.

theorem MultiplicativeBasisDeformations.TraceAlg.E78i.span_two_E7 {S : Type u_1} [Ring S] {x y : S} {M : Type u_2} [AddCommGroup M] {tr : S →+ M} (H : E78.Hyp0 x y tr) (two : ∀ (m : M), m + m = 0 → m = 0) (x4 : x ^ 4 = 0) (j : ℕ) (g : List ℕ) (hj : g = [] → 1 ≤ j) : tr (x ^ j * E78.blk x y g) ∈ AddSubgroup.closure {tr (E78.blk x y [2])} ∧ 3 • tr (E78.blk x y [2]) = 0

Lemma A.6(2) for T₄ (impose x⁴ = 0): (T₄)₊ is spanned by [yx²], annihilated by 3.