§5.11 dévissage: naturality, functoriality, rank-nullity

Part of the §5.11 dévissage development (split from GQ2/Devissage.lean).

Naturality of the word complex under coefficient maps

The maps d⁰, d¹ commute with a C-equivariant additive map φ : A →+ B (applied degreewise), so φ induces a chain map C(A) → C(B). These are the arrows of the SES of complexes.

theorem GQ2.FoxH.d0_natural {C : Type u_1} [Group C] {A : Type u_2} {B : Type u_3} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup B] [DistribMulAction C B] (t : Marking C) (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) (v : A) : (d0 t) (φ v) = fun (i : Fin 4) => φ ((d0 t) v i)

d⁰ is natural: d⁰_B(φ v) = φ ∘ d⁰_A(v) for a C-equivariant φ.

theorem GQ2.FoxH.d1_natural {C : Type u_1} [Group C] {A : Type u_2} {B : Type u_3} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup B] [DistribMulAction C B] [Finite A] [Finite B] [Finite C] (t : Marking C) (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) (x : Fin 4 → A) : (d1Fun t fun (i : Fin 4) => φ (x i)) = (φ (d1Fun t x).1, φ (d1Fun t x).2)

d¹ is natural: d¹_B(φ ∘ x) = (φ, φ) ∘ d¹_A(x) for a C-equivariant φ — the finite Fox rule pushed through the coefficient map (WordLift.map φ + Marking.map_{tame,wild}Value).

Functoriality of the cohomology

A C-equivariant φ : A →+ B induces maps Z¹w, H²w, H¹w — the arrows the module SES turns into the LES.

theorem GQ2.FoxH.d1_ker_map {C : Type u_1} [Group C] {A : Type u_2} {B : Type u_3} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup B] [DistribMulAction C B] [Finite A] [Finite B] [Finite C] (t : Marking C) (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) {x : Fin 4 → A} (hx : (d1 t) x = 0) : ((d1 t) fun (i : Fin 4) => φ (x i)) = 0

d¹-kernel is preserved: x ∈ Z¹w(A) ⟹ φ ∘ x ∈ Z¹w(B).

noncomputable def GQ2.FoxH.Z1wMap {C : Type u_1} [Group C] {A : Type u_2} {B : Type u_3} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup B] [DistribMulAction C B] [Finite A] [Finite B] [Finite C] (t : Marking C) (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) : ↥(Z1w t) →+ ↥(Z1w t)

The induced map Z¹w(A) →+ Z¹w(B).

Equations

• GQ2.FoxH.Z1wMap t φ hφ = { toFun := fun (x : ↥(GQ2.FoxH.Z1w t)) => ⟨fun (i : Fin 4) => φ (↑x i), ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def GQ2.FoxH.H2wMap {C : Type u_1} [Group C] {A : Type u_2} {B : Type u_3} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup B] [DistribMulAction C B] [Finite A] [Finite B] [Finite C] (t : Marking C) (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) : H2w t →+ H2w t

The induced map H²w(A) →+ H²w(B), descended from (φ, φ) : A × A →+ B × B through the im d¹-quotient (well-defined by d1_natural).

Equations

• GQ2.FoxH.H2wMap t φ hφ = QuotientAddGroup.map (GQ2.FoxH.d1 t).range (GQ2.FoxH.d1 t).range (φ.prodMap φ) ⋯

def GQ2.FoxH.H0wMap {C : Type u_1} [Group C] {A : Type u_2} {B : Type u_3} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup B] [DistribMulAction C B] (t : Marking C) (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) : ↥(H0w t) →+ ↥(H0w t)

The induced map H⁰w(A) →+ H⁰w(B): φ restricted to the d⁰-kernels (d⁰-naturality sends ker d⁰_A into ker d⁰_B).

Equations

• GQ2.FoxH.H0wMap t φ hφ = { toFun := fun (a : ↥(GQ2.FoxH.H0w t)) => ⟨φ ↑a, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def GQ2.FoxH.H1wMap {C : Type u_1} [Group C] {A : Type u_2} {B : Type u_3} [AddCommGroup A] [DistribMulAction C A] [AddCommGroup B] [DistribMulAction C B] [Finite A] [Finite B] [Finite C] (t : Marking C) (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) : H1w t →+ H1w t

The induced map H¹w(A) →+ H¹w(B), descended from Z1wMap through the B¹w-quotient (coboundaries map to coboundaries by d⁰-naturality).

Equations

• GQ2.FoxH.H1wMap t φ hφ = QuotientAddGroup.map ((GQ2.FoxH.B1w t).addSubgroupOf (GQ2.FoxH.Z1w t)) ((GQ2.FoxH.B1w t).addSubgroupOf (GQ2.FoxH.Z1w t)) (GQ2.FoxH.Z1wMap t φ hφ) ⋯

Rank-nullity on d¹: the two card clauses of IsSelfDual are equivalent

d¹ : A⁴ → A² gives #A⁴ = #Z¹w · #(im d¹) (rank-nullity) and #A² = #H²w · #(im d¹) (H²w = A²/im d¹). Eliminating #(im d¹) yields #Z¹w = #A² · #H²w for every A, so the two IsSelfDual card clauses (#H²w = #fixedPts and #Z¹w = #A²·#fixedPts) are equivalent — one need only track #H²w. (Flagged in the module header as the key simplification.)

theorem GQ2.FoxH.card_Z1w_eq_sq_mul_card_H2w {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) : Nat.card ↥(Z1w t) = Nat.card A ^ 2 * Nat.card (H2w t)

Rank-nullity for the word complex: #Z¹w(A) = #A² · #H²w(A), for every finite A.

theorem GQ2.FoxH.B1w_le_Z1w {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) : B1w t ≤ Z1w t

B¹w ≤ Z¹w (the chain condition, subgroup form of d1Fun_comp_d0).

theorem GQ2.FoxH.card_H1w_eq {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) : Nat.card (H1w t) = Nat.card A * Nat.card ↥(H0w t) * Nat.card (H2w t)

Euler characteristic of the word complex: #H¹w = #A · #H⁰w · #H²w. (Lagrange on the B¹w-quotient, first isomorphism on d⁰, and rank-nullity on d¹.)