Documentation

GQ2.Roe.Devissage.EvalPairings

§5.11 dévissage on the r_R spine: the evaluation pairings χ⁰, χ² #

Mechanical R-spine clone of GQ2/Devissage/EvalPairings.lean (campaign decision, docs/orchestration/roe-r20-recon.md); proofs ported verbatim. Spine renames Z1w → Z1wR, H1w → H1wR, H2w → H2wR, d1Fun → d1FunR, d1 → d1R, mixedB → mixedB_R, WildRel → WildRelR, IsSelfDual(W) → IsSelfDual(W)_R, with R-suffixed public names. The (A) helper H0w_two_torsion and the whole elementary-dual pack are reused from GQ2.Devissage.*; mixedB_zero_left/right ⇒ mixedB_R_zero_left/right and prop_5_8_left/right ⇒ prop_5_8_left/right_R (GQ2.Roe.Devissage.TracedRows).

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_R pairing — comes separately). Well-definedness against im d¹/ker d⁰ is exactly Prop 5.8 (left/right). Four maps: chi0_R/chi2_R (primal A against dual classes) and their transposes chi0T_R/chi2T_R (primal A^∨ against A-classes). Two are always injective (separation) and two are always surjective (extension/biduality) — no self-duality input.

source
theorem GQ2.FoxH.H1w_two_torsion_R {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 : H1wR t) :
h + h = 0

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

source
theorem GQ2.FoxH.H2w_two_torsion_R {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 : H2wR t) :
h + h = 0

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

source
noncomputable def GQ2.FoxH.chi0_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) :
↥(H0w t) →+ ElemDual (H2wR 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.
Instances For
    source
    noncomputable def GQ2.FoxH.chi2_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) :
    H2wR 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.
    Instances For
      source
      noncomputable def GQ2.FoxH.chi0T_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) :
      ↥(H0w t) →+ ElemDual (H2wR t)

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

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        noncomputable def GQ2.FoxH.chi2T_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) :
        H2wR t →+ ElemDual ↥(H0w t)

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

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem GQ2.FoxH.chi0_injective_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) (hA₂ : ∀ (a : A), a + a = 0) :
          Function.Injective ⇑(chi0_R t ht hw)

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

          source
          theorem GQ2.FoxH.chi0T_injective_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) :
          Function.Injective ⇑(chi0T_R t ht hw)

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

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

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

          source
          theorem GQ2.FoxH.chi2T_surjective_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) (hA₂ : ∀ (a : A), a + a = 0) :
          Function.Surjective ⇑(chi2T_R 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.

          source
          theorem GQ2.FoxH.chi2_square_R {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.WildRelR) (h : H2wR t) :
          (chi2_R t ht hw) ((H2wMap_R t φ hφ) h) = (dualMap (H0wMap t (dualMap φ) ⋯)) ((chi2_R t ht hw) h)

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

          source
          theorem GQ2.FoxH.chi0_square_R {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.WildRelR) (a : ↥(H0w t)) :
          (chi0_R t ht hw) ((H0wMap t φ hφ) a) = (dualMap (H2wMap_R t (dualMap φ) ⋯)) ((chi0_R t ht hw) a)

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

          source
          theorem GQ2.FoxH.chi0T_square_R {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.WildRelR) (lam : ↥(H0w t)) :
          (chi0T_R t ht hw) ((H0wMap t (dualMap φ) ⋯) lam) = (dualMap (H2wMap_R t φ hφ)) ((chi0T_R t ht hw) lam)

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