Twisted traces in characteristic two

Appendix B (characteristic-two-mesh-calculations.tex) works in the centre corner over a field of characteristic two. When m + m = 0 on the target, a twisted trace kills 2 r for every r, so it factors through the quotient Rc of the free ring by the relations and by 2; in Rc we have 2 = 0.

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

The relations together with the multiples of two.

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

theorem MultiplicativeBasisDeformations.TraceAlg.two_mem_Jc {t : ℕ} (L : Fin t → ℕ) (u : FreeRing (Fin t)) : 2 * u ∈ Jc L

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

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

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

The congruence of the relations and two.

@[reducible, inline]

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

The ring of centre words in characteristic two.

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

The quotient map.

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

def MultiplicativeBasisDeformations.TraceAlg.z {t : ℕ} (L : Fin t → ℕ) (i : Fin t) : Rc L

The closed path x_i in Rc.

theorem MultiplicativeBasisDeformations.TraceAlg.mkc_eq_zero {t : ℕ} (L : Fin t → ℕ) {a : FreeRing (Fin t)} (h : a ∈ Jc L) : (mkc L) a = 0

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

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

theorem MultiplicativeBasisDeformations.TraceAlg.two_eq_zero {t : ℕ} (L : Fin t → ℕ) : 2 = 0

Two is zero in Rc.

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

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

The trace on Rc.

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

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

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

The twist on Rc.

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

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

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

Twisted rotation in Rc.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.mkc_word {t : ℕ} {L : Fin t → ℕ} (w : List (Fin t)) : (mkc L) (word w) = (List.map (z L) w).prod

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

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

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.twc_id {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (hθ : ∀ (i : Fin t), D.θ i = i) (r : Rc L) : D.twc r = r