§5.11 dévissage: the degree-1 pairings χ¹

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

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

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

noncomputable def GQ2.FoxH.chi1Aux {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) (x : ↥(Z1w t)) : ElemDual (H1w t)

The inner functional: a fixed Z¹w(A)-cocycle x pairs against H¹w(A^∨)-classes via mixedB (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.

noncomputable def GQ2.FoxH.chi1 {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) : H1w t →+ ElemDual (H1w t)

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

Equations

• GQ2.FoxH.chi1 t ht hw = QuotientAddGroup.lift ((GQ2.FoxH.B1w t).addSubgroupOf (GQ2.FoxH.Z1w t)) { toFun := GQ2.FoxH.chi1Aux t ht hw, map_zero' := ⋯, map_add' := ⋯ } ⋯

noncomputable def GQ2.FoxH.chi1TAux {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) (y : ↥(Z1w t)) : ElemDual (H1w 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.

noncomputable def GQ2.FoxH.chi1T {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) : H1w t →+ ElemDual (H1w t)

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

Equations

• GQ2.FoxH.chi1T t ht hw = QuotientAddGroup.lift ((GQ2.FoxH.B1w t).addSubgroupOf (GQ2.FoxH.Z1w t)) { toFun := GQ2.FoxH.chi1TAux t ht hw, map_zero' := ⋯, map_add' := ⋯ } ⋯

theorem GQ2.FoxH.chi1T_flip {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) (h : H1w t) (h' : H1w t) : ((chi1T t ht hw) h') h = ((chi1 t ht hw) h) h'

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

theorem GQ2.FoxH.pairing_clause_iff {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) : (∃ (P : H1w t → H1w t → ZMod 2), (∀ (x : ↥(Z1w t)) (y : ↥(Z1w t)), P (h1wMk t x) (h1wMk t y) = mixedB t ↑x ↑y) ∧ (∀ (h : H1w t), h ≠ 0 → ∃ (h' : H1w t), P h h' ≠ 0) ∧ ∀ (h' : H1w t), h' ≠ 0 → ∃ (h : H1w t), P h h' ≠ 0) ↔ Function.Injective ⇑(chi1 t ht hw) ∧ Function.Injective ⇑(chi1T t ht hw)

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

theorem GQ2.FoxH.chi1_bij_of_inj {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) (hinj : Function.Injective ⇑(chi1 t ht hw)) (hinjT : Function.Injective ⇑(chi1T t ht hw)) : Function.Bijective ⇑(chi1 t ht hw) ∧ Function.Bijective ⇑(chi1T t ht hw) ∧ Nat.card (H1w t) = Nat.card (H1w 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.

theorem GQ2.FoxH.chi1_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 : H1w t) : (chi1 t ht hw) ((H1wMap t φ hφ) h) = (dualMap (H1wMap t (dualMap φ) ⋯)) ((chi1 t ht hw) h)

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

theorem GQ2.FoxH.chi1T_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) (z : H1w t) : (chi1T t ht hw) ((H1wMap t (dualMap φ) ⋯) z) = (dualMap (H1wMap t φ hφ)) ((chi1T t ht hw) z)

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