Documentation

GQ2.Roe.Devissage.SelfDual

§5.11 dévissage on the r_R spine: word-internal self-duality #

Mechanical R-spine clone of GQ2/Devissage/SelfDual.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 generic four lemma four_lemma_inj and H0w_two_torsion are reused from GQ2.Devissage.*, never cloned.

Word-internal self-duality #

The marking-internal form of the IsSelfDual_R 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_R's dévissage propagates the internal form, and the fixedPts-form follows wherever generation is available.

source
def GQ2.FoxH.IsSelfDualW_R {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_R 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.
Instances For
    source
    theorem GQ2.FoxH.isSelfDualW_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) (hA₂ : ∀ (a : A), a + a = 0) :
    IsSelfDualW_R t A ↔ Function.Bijective ⇑(chi2_R t ht hw) ∧ Function.Injective ⇑(chi1_R t ht hw) ∧ Function.Injective ⇑(chi1T_R t ht hw)

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

    source
    theorem GQ2.FoxH.chi_bij_of_selfdualW_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) (hsd : IsSelfDualW_R t A) :
    Function.Bijective ⇑(chi2_R t ht hw) ∧ Function.Bijective ⇑(chi2T_R t ht hw) ∧ Function.Bijective ⇑(chi0_R t ht hw) ∧ Function.Bijective ⇑(chi0T_R t ht hw) ∧ Function.Bijective ⇑(chi1_R t ht hw) ∧ Function.Bijective ⇑(chi1T_R t ht hw)

    From a IsSelfDualW_R-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. It is word-free ((A)-generic, recon §1.13), so the r_R spine reuses GQ2.FoxH.four_lemma_inj from GQ2.Devissage.SelfDual verbatim; there is deliberately no _R clone.