Documentation

GQ2.Roe.Devissage.Chi1

§5.11 dévissage on the r_R spine: the degree-1 pairings χ¹ #

Mechanical R-spine clone of GQ2/Devissage/Chi1.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. lemma_5_6 ⇒ lemma_5_6_R and prop_5_8_* ⇒ prop_5_8_*_R from GQ2.Roe.Devissage.TracedRows; mixedB_add/zero ⇒ mixedB_R_* from GQ2.Roe.FoxBasic.

The duality ladder, degree 1: the mixedB_R pairings χ¹, χ¹-transposed #

The degree-(1,1) rung: mixedB_R descends to H¹w(A) × H¹w(A^∨) (both coboundary directions die by Prop 5.8), giving chi1_R : H¹w(A) →+ (H¹w(A^∨))^∨ and its transpose. IsSelfDual_R's pairing clause is exactly the injectivity of both (the descended pairing is forced to be chi1_R).

source
noncomputable def GQ2.FoxH.chi1Aux_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) (x : ↥(Z1wR t)) :
ElemDual (H1wR t)

The inner functional: a fixed Z¹w(A)-cocycle x pairs against H¹w(A^∨)-classes via mixedB_R (dual coboundary offsets die by Prop 5.8 right, since d¹x = 0).

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

    χ¹ (degree-(1,1) mixedB_R pairing): H¹w(A) →+ (H¹w(A^∨))^∨.

    Equations
    Instances For
      source
      noncomputable def GQ2.FoxH.chi1TAux_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) (y : ↥(Z1wR t)) :
      ElemDual (H1wR t)

      The transposed inner functional: a fixed dual cocycle y pairs against H¹w(A)-classes (primal coboundary offsets die by Prop 5.8 left, since d¹y = 0).

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

        χ¹ transposed: H¹w(A^∨) →+ (H¹w(A))^∨.

        Equations
        Instances For
          source
          theorem GQ2.FoxH.chi1T_flip_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) (h : H1wR t) (h' : H1wR t) :
          ((chi1T_R t ht hw) h') h = ((chi1_R t ht hw) h) h'

          The two orientations pair the same classes: χ¹ᵀ(h', h) = χ¹(h, h').

          source
          theorem GQ2.FoxH.pairing_clause_iff_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) :
          (∃ (P : H1wR t → H1wR t → ZMod 2), (∀ (x : ↥(Z1wR t)) (y : ↥(Z1wR t)), P (h1wMkR t x) (h1wMkR t y) = mixedB_R t ↑x ↑y) ∧ (∀ (h : H1wR t), h ≠ 0 → ∃ (h' : H1wR t), P h h' ≠ 0) ∧ ∀ (h' : H1wR t), h' ≠ 0 → ∃ (h : H1wR t), P h h' ≠ 0) ↔ Function.Injective ⇑(chi1_R t ht hw) ∧ Function.Injective ⇑(chi1T_R t ht hw)

          The IsSelfDual_R pairing clause, characterized: a descended two-sided-nondegenerate pairing exists iff χ¹ and χ¹ᵀ are both injective. (The descent condition forces P = χ¹-evaluation.)

          source
          theorem GQ2.FoxH.chi1_bij_of_inj_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) (hinj : Function.Injective ⇑(chi1_R t ht hw)) (hinjT : Function.Injective ⇑(chi1T_R t ht hw)) :
          Function.Bijective ⇑(chi1_R t ht hw) ∧ Function.Bijective ⇑(chi1T_R t ht hw) ∧ Nat.card (H1wR t) = Nat.card (H1wR t)

          Both-injectivity upgrades to both-bijectivity (finite cards through #X^∨ = #X), and gives the H¹w-card equality.

          The Lemma 5.6 squares: χ¹ commutes with coefficient maps #

          For an equivariant φ : A →+ B, the degree-1 ladder square commutes — in both orientations it unfolds on classes to exactly lemma_5_6_R.

          source
          theorem GQ2.FoxH.chi1_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 : H1wR t) :
          (chi1_R t ht hw) ((H1wMap_R t φ hφ) h) = (dualMap (H1wMap_R t (dualMap φ) ⋯)) ((chi1_R t ht hw) h)

          The χ¹ square over a coefficient map: χ¹_B ∘ H¹wMap φ = (H¹wMap φ^∨)^∨ ∘ χ¹_A.

          source
          theorem GQ2.FoxH.chi1T_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) (z : H1wR t) :
          (chi1T_R t ht hw) ((H1wMap_R t (dualMap φ) ⋯) z) = (dualMap (H1wMap_R t φ hφ)) ((chi1T_R t ht hw) z)

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