The ring of centre words and its twisted traces

Proof of Lemmas A.3–A.4 in algebraic form (periodic-mesh-calculations.tex). The centre corner of Π(Δ) for a star with arms of L i + 1 vertices is a quotient of ℤ⟨x_1, …, x_t⟩ / (∑ x_i, x_i^{L i + 2}) (eq:star-corner-presentation; the coefficients of all relations are integers). A twisted trace on words is an additive function tr on words, compatible with these relations, with tr (u v) = tr (v θ(u)) and tr (x_i^q) = 0 for arms fixed by θ. It descends to an additive map on the quotient ring R, in which the calculations of Appendix A are ring identities.

def MultiplicativeBasisDeformations.TraceAlg.word {t : ℕ} (w : List (Fin t)) : FreeRing (Fin t)

A word as an element of the free ring.

theorem MultiplicativeBasisDeformations.TraceAlg.word_append {t : ℕ} (u v : List (Fin t)) : word (u ++ v) = word u * word v

theorem MultiplicativeBasisDeformations.TraceAlg.word_eq_of {t : ℕ} (w : List (Fin t)) : word w = FreeAbelianGroup.of (FreeMonoid.ofList w)

def MultiplicativeBasisDeformations.TraceAlg.gens {t : ℕ} (L : Fin t → ℕ) : Set (FreeRing (Fin t))

The relations of the centre corner.

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

The two-sided ideal they generate, as an additive subgroup.

theorem MultiplicativeBasisDeformations.TraceAlg.J_mul_left {t : ℕ} (L : Fin t → ℕ) (c : FreeRing (Fin t)) {x : FreeRing (Fin t)} (hx : x ∈ J L) : c * x ∈ J L

theorem MultiplicativeBasisDeformations.TraceAlg.J_mul_right {t : ℕ} (L : Fin t → ℕ) (c : FreeRing (Fin t)) {x : FreeRing (Fin t)} (hx : x ∈ J L) : x * c ∈ J L

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

The congruence of the relations.

@[reducible, inline]

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

The ring of centre words modulo the star relations.

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

The quotient map.

def MultiplicativeBasisDeformations.TraceAlg.x {t : ℕ} (L : Fin t → ℕ) (i : Fin t) : R L

The closed path x_i.

theorem MultiplicativeBasisDeformations.TraceAlg.mk_eq_zero {t : ℕ} (L : Fin t → ℕ) {a : FreeRing (Fin t)} (h : a ∈ J L) : (mk L) a = 0

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

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

The centre relation ∑ x_i = 0.

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

The arm relation x_i^{L i + 2} = 0.

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

structure MultiplicativeBasisDeformations.TraceAlg.TraceData {t : ℕ} (L : Fin t → ℕ) (M : Type u_1) [AddCommGroup M] : Type u_1

A twisted trace on words for the star with arms of L i + 1 vertices.

• tr : List (Fin t) → M
• θ : Equiv.Perm (Fin t)
• hL (i : Fin t) : L (self.θ i) = L i
• rotate (u v : List (Fin t)) : self.tr (u ++ v) = self.tr (v ++ List.map (⇑self.θ) u)
• centre (u v : List (Fin t)) : ∑ i : Fin t, self.tr (u ++ i :: v) = 0
• arm (u v : List (Fin t)) (i : Fin t) : self.tr (u ++ List.replicate (L i + 2) i ++ v) = 0
• fixed (i : Fin t) : self.θ i = i → ∀ (q : ℕ), 1 ≤ q → self.tr (List.replicate q i) = 0

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

The trace on the free ring.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trA_word {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (w : List (Fin t)) : D.trA (word w) = D.tr w

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

The twist on the free ring.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.twist_word {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (w : List (Fin t)) : D.twist (word w) = word (List.map (⇑D.θ) w)

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.induction_word {t : ℕ} {C : FreeRing (Fin t) → Prop} (a : FreeRing (Fin t)) (h0 : C 0) (hw : ∀ (w : List (Fin t)), C (word w)) (hneg : ∀ (a : FreeRing (Fin t)), C a → C (-a)) (hadd : ∀ (a b : FreeRing (Fin t)), C a → C b → C (a + b)) : C a

Induction over the free ring, through words.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trA_rotate {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (a b : FreeRing (Fin t)) : D.trA (a * b) = D.trA (b * D.twist a)

Twisted rotation on the free ring.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trA_gen {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) {r : FreeRing (Fin t)} (hr : r ∈ gens L) (a b : FreeRing (Fin t)) : D.trA (a * r * b) = 0

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trA_J {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) {y : FreeRing (Fin t)} (hy : y ∈ J L) : D.trA y = 0

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

The trace on the ring of centre words.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trR_mk {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (a : FreeRing (Fin t)) : D.trR ((TraceAlg.mk L) a) = D.trA a

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.twist_J {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) {y : FreeRing (Fin t)} (hy : y ∈ J L) : D.twist y ∈ J L

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

The twist on the ring of centre words.

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

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

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trR_rotate {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (p q : R L) : D.trR (p * q) = D.trR (q * D.twR p)

Twisted rotation in the ring of centre words: [p q] = [q θ(p)].

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.mk_word {t : ℕ} {L : Fin t → ℕ} (w : List (Fin t)) : (TraceAlg.mk L) (word w) = (List.map (x L) w).prod

The closed path of a word.

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trR_word {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (w : List (Fin t)) : D.trR (List.map (x L) w).prod = D.tr w

theorem MultiplicativeBasisDeformations.TraceAlg.TraceData.trR_fixed {t : ℕ} {L : Fin t → ℕ} {M : Type u_1} [AddCommGroup M] (D : TraceData L M) (i : Fin t) (hi : D.θ i = i) (q : ℕ) (hq : 1 ≤ q) : D.trR (x L i ^ q) = 0

Powers of the closed path along a fixed arm have zero trace.