Twisted traces when two is invertible

Appendix A, periodic-mesh-calculations.tex ("Assume two is invertible and put v = y - z = x + 2y"): when m + m = 0 forces m = 0 on the target, a twisted trace kills every element r with 2^n r in the ideal of relations. It therefore factors through the quotient R₂ of the free ring by the 2-saturation of the relations, where 2 r = 0 implies r = 0.

def MultiplicativeBasisDeformations.TraceAlg.J2 {t : ℕ} (L : Fin t → ℕ) : AddSubgroup (FreeRing (Fin t))

The 2-saturation of the relations.

theorem MultiplicativeBasisDeformations.TraceAlg.J_le_J2 {t : ℕ} (L : Fin t → ℕ) {r : FreeRing (Fin t)} (h : r ∈ J L) : r ∈ J2 L

theorem MultiplicativeBasisDeformations.TraceAlg.J2_mul_left {t : ℕ} (L : Fin t → ℕ) (c : FreeRing (Fin t)) {r : FreeRing (Fin t)} (h : r ∈ J2 L) : c * r ∈ J2 L

theorem MultiplicativeBasisDeformations.TraceAlg.J2_mul_right {t : ℕ} (L : Fin t → ℕ) (c : FreeRing (Fin t)) {r : FreeRing (Fin t)} (h : r ∈ J2 L) : r * c ∈ J2 L

def MultiplicativeBasisDeformations.TraceAlg.con2 {t : ℕ} (L : Fin t → ℕ) : RingCon (FreeRing (Fin t))

The congruence of the saturated relations.

@[reducible, inline]

abbrev MultiplicativeBasisDeformations.TraceAlg.R2 {t : ℕ} (L : Fin t → ℕ) : Type

The ring of centre words with two cancelled.

def MultiplicativeBasisDeformations.TraceAlg.mk2 {t : ℕ} (L : Fin t → ℕ) : FreeRing (Fin t) →+* R2 L

The quotient map.

theorem MultiplicativeBasisDeformations.TraceAlg.mk2_surjective {t : ℕ} (L : Fin t → ℕ) : Function.Surjective ⇑(mk2 L)

def MultiplicativeBasisDeformations.TraceAlg.y {t : ℕ} (L : Fin t → ℕ) (i : Fin t) : R2 L

The closed path x_i in R₂.

theorem MultiplicativeBasisDeformations.TraceAlg.mk2_eq_zero {t : ℕ} (L : Fin t → ℕ) {a : FreeRing (Fin t)} (h : a ∈ J2 L) : (mk2 L) a = 0

theorem MultiplicativeBasisDeformations.TraceAlg.sum_y {t : ℕ} (L : Fin t → ℕ) : ∑ i : Fin t, y L i = 0

theorem MultiplicativeBasisDeformations.TraceAlg.y_pow {t : ℕ} (L : Fin t → ℕ) (i : Fin t) : y L i ^ (L i + 2) = 0

theorem MultiplicativeBasisDeformations.TraceAlg.cancel_two {t : ℕ} (L : Fin t → ℕ) {r : R2 L} (h : 2 * r = 0) : r = 0

Two can be cancelled in R₂.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trA_J2 {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) {r : FreeRing (Fin t)} (hr : r ∈ J2 L) : D.trA r = 0

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

The trace on R₂.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.tr2_mk {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) (a : FreeRing (Fin t)) : (D.tr2 h2) ((mk2 L) a) = D.trA a

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.twist_J2 {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) {r : FreeRing (Fin t)} (hr : r ∈ J2 L) : D.twist r ∈ J2 L

def MultiplicativeBasisDeformations.TraceAlg.TraceData.tw2 {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) : R2 L →+* R2 L

The twist on R₂.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.tw2_mk {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (a : FreeRing (Fin t)) : D.tw2 ((mk2 L) a) = (mk2 L) (D.twist a)

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.tw2_y {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (i : Fin t) : D.tw2 (y L i) = y L (D.θ i)

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.tr2_rotate {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) (p q : R2 L) : (D.tr2 h2) (p * q) = (D.tr2 h2) (q * D.tw2 p)

Twisted rotation in R₂.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.mk2_word {t : ℕ} {L : Fin t → ℕ} (w : List (Fin t)) : (mk2 L) (word w) = (List.map (y L) w).prod

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.tr2_word {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) (w : List (Fin t)) : (D.tr2 h2) (List.map (y L) w).prod = D.tr w

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.tr2_fixed {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (h2 : ∀ (m : M), m + m = 0 → m = 0) (i : Fin t) (hi : D.θ i = i) (q : ℕ) (hq : 1 ≤ q) : (D.tr2 h2) (y L i ^ q) = 0