§5 definitions: the word complex (30)/(31) and the lift group A ⋊ C

The definition layer of the paper's §5 finite (candidate-side) cochain theory, split off from GQ2.FoxHeisenberg. For a finite lower target C and an elementary 𝔽₂[C]-module A this file provides:

• the relator values Marking.tameValue = τ^σ (τ²)⁻¹ and Marking.wildValue = h₀u₁⁻¹x₁^σc₀ (relations (5)/(6) as elements) with their naturality lemmas;
• the lift group A ⋊ C (WordLift A C) with the paper's convention (u, g)(v, h) = (u + g•v, gh);
• the finite word complex (30)/(31): d0, d1Fun/d1, Z1w/H0w/H1w/H2w, and the proved tame-row stress test d1Fun_tame;
• the 𝔽₂-dual ElemDual A := A →+ ZMod 2 (the Tate-duality interface's def-synonym recipe) with its contragredient C-action, the shared helper ElemDual.add_self_eq_zero, and the evaluation pairing dualEval.

See GQ2.FoxHeisenberg for the umbrella module docstring.

Relations (5)/(6) as elements of any marked group

def GQ2.Marking.tameValue {G : Type u_1} [Group G] (t : Marking G) : G

The tame relator value τ^σ · (τ²)⁻¹ at a marking (relation (5) as an element).

Equations

• t.tameValue = GQ2.conjP t.τ t.σ * (t.τ ^ 2)⁻¹

@[simp]

theorem GQ2.Marking.tameValue_eq_one_iff {G : Type u_1} [Group G] (t : Marking G) : t.tameValue = 1 ↔ t.TameRel

The tame relator dies iff the tame relation holds.

noncomputable def GQ2.Marking.wildValue {G : Type u_1} [Group G] (t : Marking G) : G

The wild relator value h₀ · u₁⁻¹ · x₁^σ · c₀ at a marking (relation (6) as an element; the ω₂-powers are powOmega2).

Equations

• t.wildValue = t.h0 * t.u1⁻¹ * GQ2.conjP t.x₁ t.σ * t.c0

@[simp]

theorem GQ2.Marking.wildValue_eq_one_iff {G : Type u_1} [Group G] (t : Marking G) : t.wildValue = 1 ↔ t.WildRel

The wild relator dies iff the wild relation holds.

theorem GQ2.Marking.map_tameValue {G : Type u_1} {H : Type u_2} [Group G] [Group H] (φ : G →* H) (t : Marking G) : (map φ t).tameValue = φ t.tameValue

Naturality of the tame relator value under a group homomorphism. (No ω₂-power occurs in the tame word, so no finiteness is needed.)

theorem GQ2.Marking.map_wildValue {G : Type u_1} {H : Type u_2} [Group G] [Group H] [Finite G] (φ : G →* H) (t : Marking G) : (map φ t).wildValue = φ t.wildValue

Naturality of the wild relator value under a group homomorphism. The ω₂-powers in the wild word push through φ via powOmega2_map, which needs the source group finite.

The lift group A ⋊ C (paper convention (u,g)(v,h) = (u + g•v, gh))

structure GQ2.FoxH.WordLift (A : Type u_1) (C : Type u_2) : Type (max u_1 u_2)

The lift group A ⋊ C of §5: pairs (u, g) with the multiplication of Lemma 5.5's proof, (u, g)(v, h) = (u + g•v, gh).

• u : A

  The A-offset of the lift.

• g : C

  The base value in C.

theorem GQ2.FoxH.WordLift.ext_iff {A : Type u_1} {C : Type u_2} {x y : WordLift A C} : x = y ↔ x.u = y.u ∧ x.g = y.g

theorem GQ2.FoxH.WordLift.ext {A : Type u_1} {C : Type u_2} {x y : WordLift A C} (u : x.u = y.u) (g : x.g = y.g) : x = y

@[implicit_reducible]

instance GQ2.FoxH.WordLift.instOne {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] : One (WordLift A C)

Equations

• GQ2.FoxH.WordLift.instOne = { one := { u := 0, g := 1 } }

@[implicit_reducible]

instance GQ2.FoxH.WordLift.instMul {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] : Mul (WordLift A C)

Equations

• GQ2.FoxH.WordLift.instMul = { mul := fun (p q : GQ2.FoxH.WordLift A C) => { u := p.u + p.g • q.u, g := p.g * q.g } }

@[implicit_reducible]

instance GQ2.FoxH.WordLift.instInv {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] : Inv (WordLift A C)

Equations

• GQ2.FoxH.WordLift.instInv = { inv := fun (p : GQ2.FoxH.WordLift A C) => { u := -(p.g⁻¹ • p.u), g := p.g⁻¹ } }

@[simp]

theorem GQ2.FoxH.WordLift.one_u {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] : u 1 = 0

@[simp]

theorem GQ2.FoxH.WordLift.one_g {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] : g 1 = 1

@[simp]

theorem GQ2.FoxH.WordLift.mul_u {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p q : WordLift A C) : (p * q).u = p.u + p.g • q.u

@[simp]

theorem GQ2.FoxH.WordLift.mul_g {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p q : WordLift A C) : (p * q).g = p.g * q.g

@[simp]

theorem GQ2.FoxH.WordLift.inv_u {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p : WordLift A C) : p⁻¹.u = -(p.g⁻¹ • p.u)

@[simp]

theorem GQ2.FoxH.WordLift.inv_g {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p : WordLift A C) : p⁻¹.g = p.g⁻¹

@[implicit_reducible]

instance GQ2.FoxH.WordLift.instGroup {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] : Group (WordLift A C)

Equations

• One or more equations did not get rendered due to their size.

def GQ2.FoxH.WordLift.equivProd {C : Type u_1} {A : Type u_2} : WordLift A C ≃ A × C

WordLift A C ≃ A × C (the underlying data), for the finiteness instance.

Equations

• GQ2.FoxH.WordLift.equivProd = { toFun := fun (p : GQ2.FoxH.WordLift A C) => (p.u, p.g), invFun := fun (p : A × C) => { u := p.1, g := p.2 }, left_inv := ⋯, right_inv := ⋯ }

instance GQ2.FoxH.WordLift.instFinite {C : Type u_1} {A : Type u_2} [Finite A] [Finite C] : Finite (WordLift A C)

def GQ2.FoxH.WordLift.map {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {A' : Type u_3} [AddCommGroup A'] [DistribMulAction C A'] (f : A →+ A') (hf : ∀ (g : C) (a : A), f (g • a) = g • f a) : WordLift A C →* WordLift A' C

Coefficient functoriality: a C-equivariant f : A →+ A' induces a group homomorphism WordLift A C →* WordLift A' C (the identity on the base C).

Equations

• GQ2.FoxH.WordLift.map f hf = { toFun := fun (p : GQ2.FoxH.WordLift A C) => { u := f p.u, g := p.g }, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem GQ2.FoxH.WordLift.map_u {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {A' : Type u_3} [AddCommGroup A'] [DistribMulAction C A'] (f : A →+ A') (hf : ∀ (g : C) (a : A), f (g • a) = g • f a) (p : WordLift A C) : ((map f hf) p).u = f p.u

@[simp]

theorem GQ2.FoxH.WordLift.map_g {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {A' : Type u_3} [AddCommGroup A'] [DistribMulAction C A'] (f : A →+ A') (hf : ∀ (g : C) (a : A), f (g • a) = g • f a) (p : WordLift A C) : ((map f hf) p).g = p.g

def GQ2.FoxH.WordLift.baseEmbed {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] : C →* WordLift A C

The base embedding C →* WordLift A C, g ↦ (0, g) (the offset-zero lift).

Equations

• GQ2.FoxH.WordLift.baseEmbed = { toFun := fun (g : C) => { u := 0, g := g }, map_one' := ⋯, map_mul' := ⋯ }

theorem GQ2.FoxH.WordLift.conj_baseEmbed {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (v : A) (g : C) : { u := v, g := 1 }⁻¹ * { u := 0, g := g } * { u := v, g := 1 } = { u := g • v - v, g := g }

Conjugating a base generator (0, g) by (v, 1) produces the coboundary offset (g • v − v, g) — the shape of d⁰.

@[simp]

theorem GQ2.FoxH.WordLift.pow_g {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p : WordLift A C) (n : ℕ) : (p ^ n).g = p.g ^ n

The base coordinate of a power is the power of the base (.g is multiplicative).

theorem GQ2.FoxH.WordLift.pow_u {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p : WordLift A C) (n : ℕ) : (p ^ n).u = ∑ i ∈ Finset.range n, p.g ^ i • p.u

The norm-of-power (geometric sum) formula — the source of the paper's "norm projector" P = 1 + T + ⋯ + Tᵉ⁻¹ in the finite Fox rules (Lemma 5.4/5.5). The A-offset of pⁿ is the partial norm (1 + g + ⋯ + gⁿ⁻¹) • u of the offset u under the base action g.

theorem GQ2.FoxH.WordLift.powOmega2_u_of_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (hA₂ : ∀ (a : A), a + a = 0) (p : WordLift A C) (hg : ∀ (a : A), p.g • a = a) : (powOmega2 p).u = p.u

Norm collapse under a trivially-acting base — the engine that flattens every ω₂-power in the wild row once the wild inertia acts trivially. If the base p.g acts trivially on the char-2 module A, the A-offset of the 2-primary part p^{ω₂} (powOmega2) is just p.u.

The ω₂-exponent e = omega2Exp (orderOf p) is odd exactly when orderOf p is even, which is exactly when p.u ≠ 0 (then addOrderOf p.u = 2 ∣ orderOf p); for odd e and a 2-torsion p.u, e • p.u = p.u. When p.u = 0 both sides vanish, so the identity is uniform.

theorem GQ2.FoxH.WordLift.powOmega2_g_smul_of_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p : WordLift A C) (hg : ∀ (a : A), p.g • a = a) (a : A) : (powOmega2 p).g • a = a

If the base p.g acts trivially, so does the base of the 2-primary part p^{ω₂} (any power of a trivially-acting element acts trivially). Companion to powOmega2_u_of_trivial for the .g-action, used to push offsets through the collapsed ω₂-powers in the wild row.

theorem GQ2.FoxH.WordLift.powOmega2_u_zero {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p : WordLift A C) (hpu : p.u = 0) : (powOmega2 p).u = 0

An offset-zero element stays offset-zero under the 2-primary part (its powers do).

theorem GQ2.FoxH.WordLift.sum_pow_smul_eq_zero {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] {σ : C} (hfpf : ∀ (a : A), σ • a = a → a = 0) {K : ℕ} {u : A} (hK : σ ^ K • u = u) : ∑ i ∈ Finset.range K, σ ^ i • u = 0

The P = 0 ledger, general form: a partial norm ∑_{i<K} σⁱ • u vanishes whenever σ acts fixed-point-freely on A (A^σ = 0) and σᴷ fixes u. The sum S is σ-invariant — σ·S = S + σᴷu − u = S (telescope) — so S ∈ A^σ = 0. (No char-2 needed.)

theorem GQ2.FoxH.WordLift.norm_eq_zero_of_fixedPointFree {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite C] (σ : C) (hfpf : ∀ (a : A), σ • a = a → a = 0) (a : A) : ∑ i ∈ Finset.range (orderOf σ), σ ^ i • a = 0

The P = 0 ledger (ramified norm collapse, Lemma 5.13(ii)): when the base σ acts fixed-point-freely on A (A^σ = 0), the norm projector P = 1 + σ + ⋯ + σ^{n−1} (n = orderOf σ) annihilates every element. The ramified analogue of powOmega2_u_of_trivial: in the split case σ acts trivially and the ω₂-power collapses to its offset; here σ is non-trivial (A^T = 0), so the geometric sum vanishes instead.

theorem GQ2.FoxH.WordLift.powOmega2_u_of_oddFixedPointFree {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (p : WordLift A C) (hfpf : ∀ (a : A), p.g • a = a → a = 0) (hodd : ∀ (a : A), powOmega2 p.g • a = a) : (powOmega2 p).u = 0

The ω₂-collapse for a fixed-point-free odd-order base (the ramified wild-row engine): if the base p.g acts fixed-point-freely on A and its 2-primary part powOmega2 p.g acts trivially (i.e. p.g acts with odd order), then the ω₂-power's offset vanishes, (powOmega2 p).u = 0. Proof: (powOmega2 p).u = ∑_{i<ω₂Exp(ord p)} p.gⁱ • p.u (pow_u); its length ω₂Exp(ord p) is a multiple of the odd action-period, so (p.g)^{ω₂Exp(ord p)} = powOmega2 p.g (finite-exponent independence powOmega2_pow_eq) fixes p.u, and sum_pow_smul_eq_zero applies. This is the ramified twin of powOmega2_u_of_trivial, consuming the hTodd hypothesis of lemma_5_13_ramified.

theorem GQ2.FoxH.WordLift.powOmega2_smul_of_trivial_mul {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite C] (g h : C) (hg : ∀ (a : A), g • a = a) (hh : ∀ (a : A), powOmega2 h • a = a) (a : A) : powOmega2 (g * h) • a = a

Trivial left factor is ω₂-transparent: if g acts trivially on A, then powOmega2 (g·h) acts the same as powOmega2 h. (ω₂ is natural through MulAction.toPermHom C A (powOmega2_map), and a trivially-acting g maps to 1.) Lets the ramified aux-word bases x₁·τ, x₀·τ inherit hTodd's odd-order condition from τ alone.

.u as an additive homomorphism on the trivially-based subgroup

At a tame lower map every wild aux word evaluates to an element whose base g acts trivially on the coefficient module. On that subgroup (p*q).u = p.u + q.u and p⁻¹.u = -p.u, so .u is a group hom into (A, +). Consequently conjugates keep the offset (conjP p g).u = p.u) and commutators have zero offset (commP p q).u = 0) — the mechanised form of the paper's "the wild factors h₀, [d₀,z₀] have zero first derivative".

theorem GQ2.FoxH.WordLift.inv_g_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p : WordLift A C) (hp : ∀ (a : A), p.g • a = a) (a : A) : p⁻¹.g • a = a

theorem GQ2.FoxH.WordLift.mul_g_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p q : WordLift A C) (hp : ∀ (a : A), p.g • a = a) (hq : ∀ (a : A), q.g • a = a) (a : A) : (p * q).g • a = a

theorem GQ2.FoxH.WordLift.mul_u_of_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p q : WordLift A C) (hp : ∀ (a : A), p.g • a = a) : (p * q).u = p.u + q.u

theorem GQ2.FoxH.WordLift.inv_u_of_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p : WordLift A C) (hp : ∀ (a : A), p.g • a = a) : p⁻¹.u = -p.u

theorem GQ2.FoxH.WordLift.conjP_u_of_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p g : WordLift A C) (hp : ∀ (a : A), p.g • a = a) (hg : ∀ (a : A), g.g • a = a) : (conjP p g).u = p.u

theorem GQ2.FoxH.WordLift.conjP_u_of_base_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p g : WordLift A C) (hp : ∀ (a : A), p.g • a = a) : (conjP p g).u = g.g⁻¹ • p.u

General conjugation offset with only the conjugated word's base trivial: the conjugator's prefix survives as g.g⁻¹ • ·. (The x₂-cancellation in the ramified h₀-row then happens in g₀-conjugate pairs — hU is not needed.)

theorem GQ2.FoxH.WordLift.commP_u_of_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p q : WordLift A C) (hp : ∀ (a : A), p.g • a = a) (hq : ∀ (a : A), q.g • a = a) : (commP p q).u = 0

theorem GQ2.FoxH.WordLift.conjP_g_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p g : WordLift A C) (hp : ∀ (a : A), p.g • a = a) (a : A) : (conjP p g).g • a = a

A conjugate of a trivially-based element is trivially-based (for any conjugator).

theorem GQ2.FoxH.WordLift.commP_g_trivial {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (p q : WordLift A C) (hp : ∀ (a : A), p.g • a = a) (hq : ∀ (a : A), q.g • a = a) (a : A) : (commP p q).g • a = a

A commutator of two trivially-based elements is trivially-based.

The word complex (30)/(31)

def GQ2.FoxH.liftMarking {C : Type u_1} {A : Type u_2} (t : Marking C) (x : Fin 4 → A) : Marking (WordLift A C)

The lifted marking ((ρσ, a), (ρτ, b), (ρx₀, c), (ρx₁, d)) over t with offsets x.

Equations

• GQ2.FoxH.liftMarking t x = { σ := { u := x 0, g := t.σ }, τ := { u := x 1, g := t.τ }, x₀ := { u := x 2, g := t.x₀ }, x₁ := { u := x 3, g := t.x₁ } }

def GQ2.FoxH.d0 {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) : A →+ Fin 4 → A

d⁰ (display (31)): simultaneous infinitesimal conjugation, v ↦ ((S−1)v, (T−1)v, (X₀−1)v, (X₁−1)v).

Equations

• GQ2.FoxH.d0 t = AddMonoidHom.mk' (fun (v : A) => ![t.σ • v - v, t.τ • v - v, t.x₀ • v - v, t.x₁ • v - v]) ⋯

noncomputable def GQ2.FoxH.d1Fun {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) (x : Fin 4 → A) : A × A

d¹, function level (display (30)): the pair of A-coordinates of the evaluated tame and wild relators at the lifted marking — "the coefficient of A in the evaluated relators".

Equations

• GQ2.FoxH.d1Fun t x = ((GQ2.FoxH.liftMarking t x).tameValue.u, (GQ2.FoxH.liftMarking t x).wildValue.u)

theorem GQ2.FoxH.d1Fun_add {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (x y : Fin 4 → A) : d1Fun t (x + y) = d1Fun t x + d1Fun t y

d¹ is additive in the lift variables — the paper's "finite Fox rules" linearity (§5.1/§5.2, displays (36)–(37)). Proof by functoriality: evaluate the relators over the coefficient module A × A, then push the value through the three C-equivariant maps fst, snd, fst + snd : A × A →+ A (Marking.map_tameValue/map_wildValue + WordLift.map); the u-coordinates give d1Fun at x, y, and x + y respectively.

(Requires A, C finite: the wild relator's ω₂-powers only push through coefficient maps in finite groups — powOmega2_map. This is the paper's finite-word setting.)

noncomputable def GQ2.FoxH.d1 {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) : (Fin 4 → A) →+ A × A

d¹ (display (30)), bundled on d1Fun_add (finite coefficients, per d1Fun_add).

Equations

• GQ2.FoxH.d1 t = AddMonoidHom.mk' (GQ2.FoxH.d1Fun t) ⋯

theorem GQ2.FoxH.d1Fun_comp_d0 {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (v : A) : d1Fun t ((d0 t) v) = 0

(30) is a complex: d¹ ∘ d⁰ = 0 when the marking satisfies the two relations. Proof: liftMarking t (d0 t v) is t pushed through g ↦ ⟨g•v − v, g⟩ = ⟨v,1⟩⁻¹⟨0,g⟩⟨v,1⟩ (conjugation of the base embedding), so its relator values are conjugates of t's — which are 1 by the relations — hence have zero A-coordinate.

def GQ2.FoxH.H0w {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) : AddSubgroup A

H⁰_{A,ρ}(A) = ker d⁰ (the t-invariants).

Equations

• GQ2.FoxH.H0w t = (GQ2.FoxH.d0 t).ker

noncomputable def GQ2.FoxH.Z1w {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) : AddSubgroup (Fin 4 → A)

Z¹_{A,ρ}(A) = ker d¹ (display (30)'s degree-one kernel).

Equations

• GQ2.FoxH.Z1w t = (GQ2.FoxH.d1 t).ker

def GQ2.FoxH.B1w {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) : AddSubgroup (Fin 4 → A)

B¹_{A,ρ}(A) = im d⁰.

Equations

• GQ2.FoxH.B1w t = (GQ2.FoxH.d0 t).range

noncomputable def GQ2.FoxH.H1w {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) : Type u_2

H¹_{A,ρ}(A) (as in GQ2/Cohomology.lean: the addSubgroupOf-quotient is total — the chain inclusion B¹ ≤ Z¹ is d1Fun_comp_d0, needed only for lemmas).

Equations

• GQ2.FoxH.H1w t = (↥(GQ2.FoxH.Z1w t) ⧸ (GQ2.FoxH.B1w t).addSubgroupOf (GQ2.FoxH.Z1w t))

@[implicit_reducible]

noncomputable instance GQ2.FoxH.instAddCommGroupH1w {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) : AddCommGroup (H1w t)

Equations

• One or more equations did not get rendered due to their size.

noncomputable def GQ2.FoxH.h1wMk {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (x : ↥(Z1w t)) : H1w t

The class of a degree-one cocycle in H¹_{A,ρ}.

Equations

• GQ2.FoxH.h1wMk t x = ↑x

noncomputable def GQ2.FoxH.H2w {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) : Type u_2

H²_{A,ρ}(A) = A² ⧸ im d¹.

Equations

• GQ2.FoxH.H2w t = ((A × A) ⧸ (GQ2.FoxH.d1 t).range)

@[implicit_reducible]

noncomputable instance GQ2.FoxH.instAddCommGroupH2w {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) : AddCommGroup (H2w t)

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.FoxH.d1Fun_tame {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) (ht : t.TameRel) (x : Fin 4 → A) : (d1Fun t x).1 = t.σ⁻¹ • t.τ • x 0 - t.σ⁻¹ • x 0 + t.σ⁻¹ • x 1 - (x 1 + t.τ • x 1)

The tame row of d¹, in closed form — the general (pre-𝔽₂) form of display (34), D(τ^σ τ⁻²)(a, b) = S⁻¹(T−1)a + S⁻¹b − (1+T)b, valid at a marking satisfying the tame relation. This is the Fox–Heisenberg design stress test: it pins the lift convention, the conjP direction, and the (30)-encoding against the paper's own computation (Lemma 5.5's proof).

The 𝔽₂-dual

def GQ2.FoxH.ElemDual (A : Type u_1) [AddCommGroup A] : Type u_1

The 𝔽₂-dual A^∨ = Hom(A, 𝔽₂), as a def-synonym (a plain abbrev would pick up Mathlib's codomain-action instances — the Tate-duality interface diamond).

Equations

• GQ2.FoxH.ElemDual A = (A →+ ZMod 2)

@[implicit_reducible]

noncomputable instance GQ2.FoxH.ElemDual.instAddCommGroup {A : Type u_1} [AddCommGroup A] : AddCommGroup (ElemDual A)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance GQ2.FoxH.ElemDual.instFunLikeZModOfNatNat {A : Type u_1} [AddCommGroup A] : FunLike (ElemDual A) A (ZMod 2)

Equations

• GQ2.FoxH.ElemDual.instFunLikeZModOfNatNat = { coe := GQ2.FoxH.ElemDual.instFunLikeZModOfNatNat._aux_1, coe_injective := ⋯ }

instance GQ2.FoxH.ElemDual.instAddMonoidHomClassZModOfNatNat {A : Type u_1} [AddCommGroup A] : AddMonoidHomClass (ElemDual A) A (ZMod 2)

instance GQ2.FoxH.ElemDual.instFinite {A : Type u_1} [AddCommGroup A] [Finite A] : Finite (ElemDual A)

theorem GQ2.FoxH.ElemDual.ext {A : Type u_1} [AddCommGroup A] {lam mu : ElemDual A} (h : ∀ (a : A), lam a = mu a) : lam = mu

theorem GQ2.FoxH.ElemDual.ext_iff {A : Type u_1} [AddCommGroup A] {lam mu : ElemDual A} : lam = mu ↔ ∀ (a : A), lam a = mu a

@[simp]

theorem GQ2.FoxH.ElemDual.zero_apply {A : Type u_1} [AddCommGroup A] (a : A) : 0 a = 0

@[simp]

theorem GQ2.FoxH.ElemDual.add_apply {A : Type u_1} [AddCommGroup A] (lam mu : ElemDual A) (a : A) : (lam + mu) a = lam a + mu a

@[simp]

theorem GQ2.FoxH.ElemDual.neg_apply {A : Type u_1} [AddCommGroup A] (lam : ElemDual A) (a : A) : (-lam) a = -lam a

@[simp]

theorem GQ2.FoxH.ElemDual.sub_apply {A : Type u_1} [AddCommGroup A] (lam mu : ElemDual A) (a : A) : (lam - mu) a = lam a - mu a

theorem GQ2.FoxH.ElemDual.add_self_eq_zero {A : Type u_1} [AddCommGroup A] (lam : ElemDual A) : lam + lam = 0

ElemDual A is elementary (2-torsion): every 𝔽₂-dual functional kills itself. The canonical form of the ubiquitous hV₂d-style hypotheses; also applies to raw A →+ ZMod 2 maps (ElemDual is a def-synonym).

@[implicit_reducible]

noncomputable instance GQ2.FoxH.ElemDual.instDistribMulAction {A : Type u_1} [AddCommGroup A] {C : Type u_2} [Group C] [DistribMulAction C A] : DistribMulAction C (ElemDual A)

The contragredient action (g•λ)(a) = λ(g⁻¹•a).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem GQ2.FoxH.ElemDual.smul_apply {A : Type u_1} [AddCommGroup A] {C : Type u_2} [Group C] [DistribMulAction C A] (g : C) (lam : ElemDual A) (a : A) : (g • lam) a = lam (g⁻¹ • a)

noncomputable def GQ2.FoxH.dualEval (A : Type u_1) [AddCommGroup A] : A →+ ElemDual A →+ ZMod 2

The evaluation pairing A →+ A^∨ →+ 𝔽₂, (a, λ) ↦ λ(a) (bundled for the cup-product API cup products; equivariant into the trivial module by contragredience).

Equations

• GQ2.FoxH.dualEval A = AddMonoidHom.mk' (fun (a : A) => AddMonoidHom.mk' (fun (lam : GQ2.FoxH.ElemDual A) => lam a) ⋯) ⋯

@[simp]

theorem GQ2.FoxH.dualEval_apply {A : Type u_1} [AddCommGroup A] (a : A) (lam : ElemDual A) : ((dualEval A) a) lam = lam a