§5.11 dévissage: the evaluation pairings χ⁰, χ²

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

The duality ladder: the evaluation pairings χ⁰, χ² (and transposes)

The chain map from the word complex of A to the reversed dual of the word complex of A^∨ = ElemDual A, in the two degrees where it is an evaluation pairing (degree 1 — the mixedB pairing — comes separately). Well-definedness against im d¹/ker d⁰ is exactly Prop 5.8 (left/right). Four maps: chi0/chi2 (primal A against dual classes) and their transposes chi0T/chi2T (primal A^∨ against A-classes). Two are always injective (separation) and two are always surjective (extension/biduality) — no self-duality input.

theorem GQ2.FoxH.H0w_two_torsion {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (t : Marking C) (hA₂ : ∀ (a : A), a + a = 0) (a : ↥(H0w t)) : a + a = 0

2-torsion of the word-complex H⁰w (a subgroup of A).

theorem GQ2.FoxH.H1w_two_torsion {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (hA₂ : ∀ (a : A), a + a = 0) (h : H1w t) : h + h = 0

2-torsion of the word-complex H¹w (a subquotient of A⁴).

theorem GQ2.FoxH.H2w_two_torsion {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (hA₂ : ∀ (a : A), a + a = 0) (h : H2w t) : h + h = 0

2-torsion of the word-complex H²w (a quotient of A²).

theorem GQ2.FoxH.mixedB_zero_right {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (x : Fin 4 → A) : mixedB t x 0 = 0

mixedB t x 0 = 0 (from right-additivity, in the 2-torsion target).

theorem GQ2.FoxH.mixedB_zero_left {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] (t : Marking C) (y : Fin 4 → ElemDual A) : mixedB t 0 y = 0

mixedB t 0 y = 0 (from left-additivity, in the 2-torsion target).

noncomputable def GQ2.FoxH.chi0 {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) : ↥(H0w t) →+ ElemDual (H2w t)

χ⁰ (degree-(0,2) evaluation): H⁰w(A) →+ (H²w(A^∨))^∨, a ↦ ([λ,μ] ↦ λ(a) + μ(a)). Well-defined on H²w(A^∨)-classes by Prop 5.8 (left): on (λ,μ) = d¹y the value is B(d⁰a, y) = B(0, y) = 0.

Equations

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

noncomputable def GQ2.FoxH.chi2 {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) : H2w t →+ ElemDual ↥(H0w t)

χ² (degree-(2,0) evaluation): H²w(A) →+ (H⁰w(A^∨))^∨, [(u,v)] ↦ (λ ↦ λ(u+v)). Well-defined on H²w(A)-classes by Prop 5.8 (right).

Equations

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

noncomputable def GQ2.FoxH.chi0T {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) : ↥(H0w t) →+ ElemDual (H2w t)

χ⁰ transposed: H⁰w(A^∨) →+ (H²w(A))^∨, λ ↦ ([(u,v)] ↦ λ(u+v)). Well-defined by Prop 5.8 (right), like chi2 with the roles of the arguments exchanged.

Equations

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

noncomputable def GQ2.FoxH.chi2T {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) : H2w t →+ ElemDual ↥(H0w t)

χ² transposed: H²w(A^∨) →+ (H⁰w(A))^∨, [(λ,μ)] ↦ (a ↦ λ(a) + μ(a)). Well-defined by Prop 5.8 (left), like chi0 with the roles exchanged.

Equations

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

theorem GQ2.FoxH.chi0_injective {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) (hA₂ : ∀ (a : A), a + a = 0) : Function.Injective ⇑(chi0 t ht hw)

χ⁰ is always injective (the dual separates points; no self-duality input).

theorem GQ2.FoxH.chi0T_injective {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) : Function.Injective ⇑(chi0T t ht hw)

χ⁰ transposed is always injective (evaluation at [(u,0)] recovers λ(u)).

theorem GQ2.FoxH.chi2_surjective {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) (hA₂ : ∀ (a : A), a + a = 0) : Function.Surjective ⇑(chi2 t ht hw)

χ² is always surjective (extension along H⁰w(A^∨) ≤ A^∨ + biduality).

theorem GQ2.FoxH.chi2T_surjective {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) (hA₂ : ∀ (a : A), a + a = 0) : Function.Surjective ⇑(chi2T t ht hw)

χ² transposed is always surjective (extension along H⁰w(A) ≤ A).

The evaluation squares: χ⁰/χ² commute with coefficient maps

Four squares, general in an equivariant φ : A →+ B; each unfolds on classes to map_add or to a literal rfl.

theorem GQ2.FoxH.chi2_square {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] {B : Type u_3} [AddCommGroup B] [DistribMulAction C B] [Finite B] (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (h : H2w t) : (chi2 t ht hw) ((H2wMap t φ hφ) h) = (dualMap (H0wMap t (dualMap φ) ⋯)) ((chi2 t ht hw) h)

The χ² square: χ²_B ∘ H²wMap φ = (H⁰wMap φ^∨)^∨ ∘ χ²_A.

theorem GQ2.FoxH.chi0_square {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] {B : Type u_3} [AddCommGroup B] [DistribMulAction C B] [Finite B] (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (a : ↥(H0w t)) : (chi0 t ht hw) ((H0wMap t φ hφ) a) = (dualMap (H2wMap t (dualMap φ) ⋯)) ((chi0 t ht hw) a)

The χ⁰ square: χ⁰_B ∘ H⁰wMap φ = (H²wMap φ^∨)^∨ ∘ χ⁰_A.

theorem GQ2.FoxH.chi0T_square {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] [Finite A] [Finite C] {B : Type u_3} [AddCommGroup B] [DistribMulAction C B] [Finite B] (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (lam : ↥(H0w t)) : (chi0T t ht hw) ((H0wMap t (dualMap φ) ⋯) lam) = (dualMap (H2wMap t φ hφ)) ((chi0T t ht hw) lam)

The transposed χ⁰ square: χ⁰ᵀ_A ∘ H⁰wMap φ^∨ = (H²wMap φ)^∨ ∘ χ⁰ᵀ_B.