Documentation

GQ2.Roe.Devissage.Naturality

§5.11 dévissage on the r_R spine: naturality, functoriality, rank-nullity #

Mechanical R-spine clone of GQ2/Devissage/Naturality.lean (campaign decision, docs/orchestration/roe-r20-recon.md); proofs ported verbatim. Spine renames d1Fun → d1FunR, d1 → d1R, Z1w → Z1wR, H1w → H1wR, H2w → H2wR, with R-suffixed public names. The (A)-generic helpers d0_natural, H0wMap, and B1w_le_Z1w (⇒ the existing B1wR_le_Z1wR) are reused from GQ2.Devissage.Naturality, never cloned.

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.

source
theorem GQ2.FoxH.d1_natural_R {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) :
(d1FunR t fun (i : Fin 4) => φ (x i)) = (φ (d1FunR t x).1, φ (d1FunR 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.

source
theorem GQ2.FoxH.d1_ker_map_R {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 : (d1R t) x = 0) :
((d1R t) fun (i : Fin 4) => φ (x i)) = 0

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

source
noncomputable def GQ2.FoxH.Z1wMap_R {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) :
↥(Z1wR t) →+ ↥(Z1wR t)

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

Equations
  • GQ2.FoxH.Z1wMap_R t φ hφ = { toFun := fun (x : ↥(GQ2.FoxH.Z1wR t)) => ⟨fun (i : Fin 4) => φ (↑x i), ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
Instances For
    source
    noncomputable def GQ2.FoxH.H2wMap_R {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) :
    H2wR t →+ H2wR 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_R).

    Equations
    Instances For
      source
      noncomputable def GQ2.FoxH.H1wMap_R {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) :
      H1wR t →+ H1wR t

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

      Equations
      Instances For

        Rank-nullity on d¹: the two card clauses of IsSelfDual_R 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_R 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.)

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

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

        source
        theorem GQ2.FoxH.card_H1w_eq_R {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.WildRelR) :
        Nat.card (H1wR t) = Nat.card A * Nat.card ↥(H0w t) * Nat.card (H2wR 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¹.)