§5.11 dévissage: word-internal self-duality and the four lemma

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

Word-internal self-duality

The marking-internal form of the IsSelfDual package: #H⁰w(A^∨) in place of #fixedPts C (A^∨). For a generating marking (t.Generates) the two agree — ker d⁰ is then exactly the C-fixed points; lemma_5_11's dévissage propagates the internal form, and the fixedPts-form follows wherever generation is available.

def GQ2.FoxH.IsSelfDualW {C : Type u_1} [Group C] [Finite C] (t : Marking C) (A : Type u_3) [AddCommGroup A] [DistribMulAction C A] [Finite A] : Prop

Word-internal self-duality (the IsSelfDual package with the invariants of the dual replaced by the word-complex H⁰w of the dual).

Equations

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

theorem GQ2.FoxH.isSelfDualW_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) (hA₂ : ∀ (a : A), a + a = 0) : IsSelfDualW t A ↔ Function.Bijective ⇑(chi2 t ht hw) ∧ Function.Injective ⇑(chi1 t ht hw) ∧ Function.Injective ⇑(chi1T t ht hw)

IsSelfDualW in χ-language: χ² bijective and χ¹, χ¹ᵀ injective. (The second card clause is rank-nullity; the pairing clause is pairing_clause_iff.)

theorem GQ2.FoxH.chi_bij_of_selfdualW {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) (hsd : IsSelfDualW t A) : Function.Bijective ⇑(chi2 t ht hw) ∧ Function.Bijective ⇑(chi2T t ht hw) ∧ Function.Bijective ⇑(chi0 t ht hw) ∧ Function.Bijective ⇑(chi0T t ht hw) ∧ Function.Bijective ⇑(chi1 t ht hw) ∧ Function.Bijective ⇑(chi1T t ht hw)

From a IsSelfDualW-package, all six χ-maps are bijective (the free halves plus the Euler-characteristic swap #H⁰w(A) = #H²w(A^∨)).

The four lemma (injectivity form)

The standard diagram chase, hand-rolled for AddMonoidHoms with pointwise exactness data — the engine that turns the ladder squares into the conditional halves of the χ-bijectivities.

theorem GQ2.FoxH.four_lemma_inj {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₄ : Type u_5} {B₁ : Type u_6} {B₂ : Type u_7} {B₃ : Type u_8} {B₄ : Type u_9} [AddCommGroup A₁] [AddCommGroup A₂] [AddCommGroup A₃] [AddCommGroup A₄] [AddCommGroup B₁] [AddCommGroup B₂] [AddCommGroup B₃] [AddCommGroup B₄] (a₁ : A₁ →+ A₂) (a₂ : A₂ →+ A₃) (a₃ : A₃ →+ A₄) (b₁ : B₁ →+ B₂) (b₂ : B₂ →+ B₃) (b₃ : B₃ →+ B₄) (m₁ : A₁ →+ B₁) (m₂ : A₂ →+ B₂) (m₃ : A₃ →+ B₃) (m₄ : A₄ →+ B₄) (sq₁ : ∀ (x : A₁), m₂ (a₁ x) = b₁ (m₁ x)) (sq₂ : ∀ (x : A₂), m₃ (a₂ x) = b₂ (m₂ x)) (sq₃ : ∀ (x : A₃), m₄ (a₃ x) = b₃ (m₃ x)) (htop₂ : ∀ (x : A₂), a₂ x = 0 ↔ x ∈ a₁.range) (htop₃ : ∀ (x : A₃), a₃ x = 0 ↔ x ∈ a₂.range) (hbot₂ : ∀ (y : B₂), b₂ y = 0 → y ∈ b₁.range) (hm₁ : Function.Surjective ⇑m₁) (hm₂ : Function.Injective ⇑m₂) (hm₄ : Function.Injective ⇑m₄) : Function.Injective ⇑m₃

Four lemma, injectivity: in a commuting ladder with exact rows, if m₁ is surjective and m₂, m₄ are injective, then m₃ is injective. (Exactness is taken pointwise; only the ker ⊆ im direction is needed on the bottom row.)