Stage E foundation — the candidate linear-lifting word complex (manuscript §5)

This file formalises the candidate side of the linear lifting theory of reference/q2_manuscript.tex §5 ("Linear lifting theory and duality", l.1215–1490): the finite word complex

  C_{ρ,A}^•:   0 ⟶ A  --d⁰-->  A⁴  --d¹-->  A²  ⟶ 0           (eq:defcomplex)

attached to a finite group C, a boundary-compatible epimorphism ρ : Γ ↠ C (Γ = G_A, the candidate group), and a finite elementary F₂[C]-module A (an F₂-vector space, here [AddCommGroup A] [Module (ZMod 2) A]).

The data (l.1251)

S, T, X₀, X₁ : A →ₗ[ZMod 2] A are the actions on A of the four lower values ρ(σ), ρ(τ), ρ(x₀), ρ(x₁) of the marked generators σ, τ, x₀, x₁ (Q2Presentation.Gen). They are the images of the four generators under ρ followed by the C-action; in §FromRepresentation below they are produced from a genuine ρ : C →* Module.End (ZMod 2) A (this monoid hom is the datum Representation (ZMod 2) C A) and four group elements s t x₀ x₁ : C.

d⁰ (eq:d0explicit, l.1254)

Simultaneous infinitesimal conjugation with the lift convention (a,g) in the semidirect product gives

  d⁰(v) = ((S-1)v, (T-1)v, (X₀-1)v, (X₁-1)v).

Here 1 is LinearMap.id and, since A is an F₂-module, S - 1 = S + 1.

d¹ — the evaluated Fox Jacobian (lem:jacobian, eq:simplejac/Ltactual/Lwactual)

d¹ is the ordered pair of the tame-relator defect and the wild-relator defect (l.1257): writing the lift of the four generators into C ⋉ A as (ρ(σ),a), (ρ(τ),b), (ρ(x₀),c), (ρ(x₁),d), the value d¹(a,b,c,d) is the A-coefficient of the two evaluated relators (Q2Word.tameRelator, Q2Word.wildRelator). This is functorial in A because it evaluates the same two finite words in semidirect products.

The manuscript's closed form (lem:jacobian, eq:simplejac) — which we take here as the definition — is, with P = 1 + T + ⋯ + T^{e-1} the norm of the cyclic group ⟨T⟩ (e = orderOf T):

  d¹ = ⎛ S⁻¹(1+T)   S⁻¹+1+T    0    0     ⎞      (tame row L_t, eq:Ltactual)
       ⎝ 0          P          0    P+S⁻¹ ⎠      (wild row L_w, eq:Lwactual)

i.e. L_t = S⁻¹(1+T)·a + (S⁻¹+1+T)·b and L_w = P·b + (P+S⁻¹)·d.

Derivation of the tame row (proof of lem:jacobian, l.1463): differentiating τ^σ·τ⁻² = rconj τ σ · (τ²)⁻¹ (= Q2Word.tameRelator) in A⋊C with (u,g)(v,h)=(u+gv,gh) gives D(τ^σ τ⁻²)(a,b) = S⁻¹(T-1)a + (S⁻¹-(1+T))b, which over F₂ is exactly L_t.

Derivation of the wild row (lem:fullwordledger, l.1387; lem:h0shadow, l.1342): Q2Word.wildRelator = h₀·u₁⁻¹·x₁^σ·c₀. By lem:h0shadow the factor h₀ has the first-order value of x₀², hence first derivative 0; the commutator c₀ = (d₀,z₀) has first derivative 0; u₁ = (x₁τ)^{ω₂} differentiates to the norm projector P of the odd T-orbit (lem:finiteexponent makes the ω₂-power independent of the chosen finite integer representative, so D(g^{ω₂}) = P on the odd part — this is the only place ω₂ enters d¹, and it enters as P); x₁^σ contributes S⁻¹. The factor ledger (l.1402) sums to L_w = P·b + (P+S⁻¹)·d.

The complex property and cohomology

d¹∘d⁰ = 0 is the Fox fundamental identity Σᵢ (∂r/∂xᵢ)(xᵢ-1) = r-1: each relator r is trivial in Γ, so its image in GL(A) is trivial, and the row of d¹∘d⁰ is (image of r) − 1 = 0. Concretely the three linear shadows of the group relations are needed:

• Sinv * T * S = T^2 — the image of the tame relation σ⁻¹τσ = τ²;
• P * (T - 1) = 0 — P is the norm of ⟨T⟩ (automatic from T^{orderOf T}=1);
• (P + Sinv) * (X₁ - 1) = 0 — the linear shadow of the wild relator (automatic on a simple tame factor, where X₁ = 1, by lem:h0shadow).

Cohomology: Z¹ = ker d¹, H¹ = ker d¹ / im d⁰, H² = coker d¹.

Char-2 and telescoping helpers

The two boundary maps d⁰, d¹

def Q2Presentation.Lifting.d0 {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (S T X₀ X₁ : Module.End (ZMod 2) A) : A →ₗ[ZMod 2] A × A × A × A

The candidate d⁰ (manuscript eq:d0explicit): v ↦ ((S-1)v, (T-1)v, (X₀-1)v, (X₁-1)v).

Equations

• Q2Presentation.Lifting.d0 S T X₀ X₁ = LinearMap.prod (S - 1) (LinearMap.prod (T - 1) (LinearMap.prod (X₀ - 1) (X₁ - 1)))

def Q2Presentation.Lifting.d1 {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T P : Module.End (ZMod 2) A) : A × A × A × A →ₗ[ZMod 2] A × A

The candidate d¹, the evaluated Fox Jacobian (manuscript lem:jacobian, eq:simplejac): tame row (S⁻¹(1+T), S⁻¹+1+T, 0, 0) and wild row (0, P, 0, P+S⁻¹), where P is the norm of ⟨T⟩ and Sinv = S⁻¹.

Equations

• Q2Presentation.Lifting.d1 Sinv T P = ((Sinv * (1 + T)).coprod ((Sinv + 1 + T).coprod (LinearMap.coprod 0 0))).prod (LinearMap.coprod 0 (LinearMap.coprod P (LinearMap.coprod 0 (P + Sinv))))

The complex property d¹ ∘ d⁰ = 0

theorem Q2Presentation.Lifting.d1_comp_d0 {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (S T X₀ X₁ Sinv P : Module.End (ZMod 2) A) (hSinv : Sinv * S = 1) (htame : Sinv * T * S = T ^ 2) (hnorm : P * (T - 1) = 0) (hwild : (P + Sinv) * (X₁ - 1) = 0) : d1 Sinv T P ∘ₗ d0 S T X₀ X₁ = 0

The complex property (C_{ρ,A}^• is a cochain complex): d¹ ∘ d⁰ = 0. Hypotheses are the linear shadows of the candidate group relations: hSinv (S⁻¹ is the inverse of S), htame (image of σ⁻¹τσ = τ²), hnorm (P is the norm of ⟨T⟩), hwild (wild relator linear shadow).

theorem Q2Presentation.Lifting.range_d0_le_ker_d1 {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (S T X₀ X₁ Sinv P : Module.End (ZMod 2) A) (hSinv : Sinv * S = 1) (htame : Sinv * T * S = T ^ 2) (hnorm : P * (T - 1) = 0) (hwild : (P + Sinv) * (X₁ - 1) = 0) : (d0 S T X₀ X₁).range ≤ (d1 Sinv T P).ker

im d⁰ ≤ ker d¹, the submodule form of the complex property.

Cohomology of C_{ρ,A}^•

def Q2Presentation.Lifting.Z1 {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T P : Module.End (ZMod 2) A) : Submodule (ZMod 2) (A × A × A × A)

Z¹ = ker d¹, the candidate 1-cocycles.

Equations

• Q2Presentation.Lifting.Z1 Sinv T P = (Q2Presentation.Lifting.d1 Sinv T P).ker

def Q2Presentation.Lifting.B1 {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (S T X₀ X₁ : Module.End (ZMod 2) A) : Submodule (ZMod 2) (A × A × A × A)

B¹ = im d⁰, the candidate 1-coboundaries.

Equations

• Q2Presentation.Lifting.B1 S T X₀ X₁ = (Q2Presentation.Lifting.d0 S T X₀ X₁).range

@[reducible, inline]

abbrev Q2Presentation.Lifting.H1 {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (S T X₀ X₁ Sinv P : Module.End (ZMod 2) A) : Type u_1

H¹_{A,ρ}(A) = ker d¹ / im d⁰ (manuscript H^i_{A,ρ}, l.1268). The coboundaries B¹ are pulled back into Z¹ along the inclusion; when B¹ ≤ Z¹ (i.e. the complex property, range_d0_le_ker_d1) this is the genuine homology.

Equations

• Q2Presentation.Lifting.H1 S T X₀ X₁ Sinv P = (↥(Q2Presentation.Lifting.Z1 Sinv T P) ⧸ Submodule.comap (Q2Presentation.Lifting.Z1 Sinv T P).subtype (Q2Presentation.Lifting.B1 S T X₀ X₁))

@[reducible, inline]

abbrev Q2Presentation.Lifting.H2 {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] (Sinv T P : Module.End (ZMod 2) A) : Type u_1

H²_{A,ρ}(A) = coker d¹, the degree-two obstruction group.

Equations

• Q2Presentation.Lifting.H2 Sinv T P = ((A × A) ⧸ (Q2Presentation.Lifting.d1 Sinv T P).range)

Instantiation from a representation ρ : C →* End A

A ρ : C →* Module.End (ZMod 2) A is exactly the datum of a Representation (ZMod 2) C A (a C-action by ZMod 2-linear maps). Given the four lower values s t x₀ x₁ : C (the images ρ(σ), ρ(τ), ρ(x₀), ρ(x₁)), the four endomorphisms are ρ s, ρ t, ρ x₀, ρ x₁, with ρ s⁻¹ the inverse of ρ s and P = ∑_{i<orderOf t} (ρ t)^i the norm. All hypotheses of d1_comp_d0 except the wild shadow are then automatic; the wild shadow is automatic on a simple tame factor (ρ x₁ = 1).

noncomputable def Q2Presentation.Lifting.repNorm {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] {C : Type u_2} [Group C] (ρ : C →* Module.End (ZMod 2) A) (t : C) : Module.End (ZMod 2) A

The norm element P = 1 + (ρ t) + ⋯ + (ρ t)^{e-1} of the cyclic group ⟨ρ t⟩, e = orderOf t.

Equations

• Q2Presentation.Lifting.repNorm ρ t = ∑ i ∈ Finset.range (orderOf t), ρ t ^ i

theorem Q2Presentation.Lifting.repSinv_mul {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] {C : Type u_2} [Group C] (ρ : C →* Module.End (ZMod 2) A) (s : C) : ρ s⁻¹ * ρ s = 1

ρ s⁻¹ is the (two-sided) inverse of ρ s.

theorem Q2Presentation.Lifting.repNorm_mul_sub {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] {C : Type u_2} [Group C] (ρ : C →* Module.End (ZMod 2) A) (t : C) : repNorm ρ t * (ρ t - 1) = 0

The norm kills ρ t - 1 (manuscript: P is the norm of the T-orbit).

theorem Q2Presentation.Lifting.repTame {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] {C : Type u_2} [Group C] (ρ : C →* Module.End (ZMod 2) A) (s t : C) (hrel : s⁻¹ * t * s = t ^ 2) : ρ s⁻¹ * ρ t * ρ s = ρ t ^ 2

The tame relation in C lifts to the endomorphism identity (ρ s⁻¹)(ρ t)(ρ s) = (ρ t)².

theorem Q2Presentation.Lifting.d1_comp_d0_ofRep {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] {C : Type u_2} [Group C] (ρ : C →* Module.End (ZMod 2) A) (s t x₀ x₁ : C) (hrel : s⁻¹ * t * s = t ^ 2) (hwild : (repNorm ρ t + ρ s⁻¹) * (ρ x₁ - 1) = 0) : d1 (ρ s⁻¹) (ρ t) (repNorm ρ t) ∘ₗ d0 (ρ s) (ρ t) (ρ x₀) (ρ x₁) = 0

The candidate word complex of a representation is a complex: given the tame relation s⁻¹ t s = t² in C (image of Q2Word.tameRelator) and the wild linear shadow, d¹ ∘ d⁰ = 0.

theorem Q2Presentation.Lifting.d1_comp_d0_ofRep_tameFactor {A : Type u_1} [AddCommGroup A] [Module (ZMod 2) A] {C : Type u_2} [Group C] (ρ : C →* Module.End (ZMod 2) A) (s t x₀ x₁ : C) (hrel : s⁻¹ * t * s = t ^ 2) (hx1 : ρ x₁ = 1) : d1 (ρ s⁻¹) (ρ t) (repNorm ρ t) ∘ₗ d0 (ρ s) (ρ t) (ρ x₀) (ρ x₁) = 0

On a simple tame factor the wild generator acts trivially (ρ x₁ = 1), so the wild linear shadow is automatic (lem:h0shadow) and the complex property holds from the tame relation alone.