Twisted traces killed by two (Lemma B.2, the trace calculations)

characteristic-two-mesh-calculations.tex (proof of lem:integral-mesh-cokernels), over an arbitrary coefficient group (no division by two):

• type D: "In either case the fixed long-arm power gives 0 = [(-x-y)^j] = ±2[w_j]. Thus every possible retained type-D trace quotient is killed by two." (trace_D_two, trace_D_any_two);
• the reflection of E₆: "[ξ₆] = [(xyx²)y] = -[x²yx²] = -[ξ₆]" (trace_E6r_two);
• E₇, E₈: the candidate classes [yx³], [(yx³)²], [(yx³)(yx⁴)²] of word degrees 4, 8, 14 are killed by two (trace_E78_two), by the identities of Lemma A.6 without its final division.

Type D

theorem MultiplicativeBasisDeformations.TraceAlg.trace_D_two {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) (hθc : D.θ c = c) (hθ : D.θ a = a ∧ D.θ b = b ∨ D.θ a = b ∧ D.θ b = a) {w : List (Fin 3)} (hw : w ≠ []) : D.tr w + D.tr w = 0

Type D: with short arms a, b and long arm c fixed by the twist, every positive trace is killed by two.

theorem MultiplicativeBasisDeformations.TraceAlg.trace_D_any_two {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) {a b c : Fin 3} (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (hLa : L a = 0) (hLb : L b = 0) {w : List (Fin 3)} (hw : 2 ≤ w.length) : D.tr w + D.tr w = 0

Type D with any twist preserving the arm lengths: all traces of length at least two are killed by two.

The corner identities of the types E

theorem MultiplicativeBasisDeformations.TraceAlg.e_d2 {S : Type u_2} [Ring S] {x y : S} (hy3 : y ^ 3 = 0) (hd1 : y * y + y * x + x * y + x * x = 0) : y * x * y - x * y * x - x ^ 3 = 0

theorem MultiplicativeBasisDeformations.TraceAlg.e_d3 {S : Type u_2} [Ring S] {x y : S} (hy3 : y ^ 3 = 0) (hd1 : y * y + y * x + x * y + x * x = 0) : y * x ^ 2 * y + y * x ^ 3 + x * y * x ^ 2 + x ^ 2 * y * x + x ^ 3 * y + 2 * x ^ 4 = 0

theorem MultiplicativeBasisDeformations.TraceAlg.e_F {S : Type u_2} [Ring S] {x y : S} (hy3 : y ^ 3 = 0) (hd1 : y * y + y * x + x * y + x * x = 0) (hx5 : x ^ 5 = 0) : y * x ^ 3 * y * x + y * x ^ 4 * y + x * y * x ^ 3 * y - x ^ 2 * y * x ^ 3 - x ^ 3 * y * x ^ 2 = 0

The types E

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

theorem MultiplicativeBasisDeformations.TraceAlg.e_hy3 {L : Fin 3 → ℕ} {b : Fin 3} (hLb : L b = 1) : x L b ^ 3 = 0

theorem MultiplicativeBasisDeformations.TraceAlg.trace_E6r_two {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) {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θc : D.θ c = b) : D.tr [c, c, b, c, c] + D.tr [c, c, b, c, c] = 0

The reflection of E₆: [x²yx²] = -[x²yx²].

theorem MultiplicativeBasisDeformations.TraceAlg.twR_id {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) (hθ : ∀ (i : Fin 3), D.θ i = i) (r : R L) : D.twR r = r

theorem MultiplicativeBasisDeformations.TraceAlg.trace_E78_two {M : Type u_1} [AddCommGroup M] {L : Fin 3 → ℕ} (D : TraceData L M) {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 ≤ 3) (hθ : ∀ (i : Fin 3), D.θ i = i) : D.tr [b, c, c, c] + D.tr [b, c, c, c] = 0 ∧ D.tr [b, c, c, c, b, c, c, c] + D.tr [b, c, c, c, b, c, c, c] = 0 ∧ D.tr [b, c, c, c, b, c, c, c, c, b, c, c, c, c] + D.tr [b, c, c, c, b, c, c, c, c, b, c, c, c, c] = 0

The candidates of E₇, E₈ are killed by two: the classes of word degrees 4, 8, 14.