Documentation

GQ2.Devissage.ElemDualPack

§5.11 dévissage: the elementary-dual pack #

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

The elementary-dual pack #

ElemDual-infrastructure for the dual side of the dévissage: contravariant functoriality, the extension lemma (ZMod 2 is injective for finite elementary 2-groups), separation, the dimension count, biduality, and exactness of dualization. Module (ZMod 2)-structures appear only locally inside proofs (AddCommGroup.zmodModule), per the repo's no-Module-instances convention.

source
def GQ2.FoxH.dualMap {A : Type u_2} {B : Type u_3} [AddCommGroup A] [AddCommGroup B] (φ : A →+ B) :
ElemDual B →+ ElemDual A

Contravariant functoriality of the 𝔽₂-dual: precomposition λ ↦ λ ∘ φ.

Equations
Instances For
    source
    @[simp]
    theorem GQ2.FoxH.dualMap_apply {A : Type u_2} {B : Type u_3} [AddCommGroup A] [AddCommGroup B] (φ : A →+ B) (lam : ElemDual B) (a : A) :
    ((dualMap φ) lam) a = lam (φ a)
    source
    theorem GQ2.FoxH.dualMap_equivariant {C : Type u_1} [Group C] {A : Type u_2} {B : Type u_3} [AddCommGroup A] [AddCommGroup B] [DistribMulAction C A] [DistribMulAction C B] (φ : A →+ B) (hφ : ∀ (c : C) (a : A), φ (c • a) = c • φ a) (c : C) (lam : ElemDual B) :
    (dualMap φ) (c • lam) = c • (dualMap φ) lam

    dualMap is equivariant for the contragredient actions.

    source
    theorem GQ2.FoxH.elemDual_extend {A' : Type u_2} {A : Type u_3} [AddCommGroup A'] [AddCommGroup A] [Finite A] (hA₂ : ∀ (a : A), a + a = 0) (f : A' →+ A) (hinj : Function.Injective ⇑f) (lam' : ElemDual A') :
    ∃ (lam : ElemDual A), ∀ (a' : A'), lam (f a') = lam' a'

    Extension lemma: every 𝔽₂-functional extends along an injection into a finite elementary 2-group (ZMod 2 is self-injective on this category; proof by complementing the image subspace).

    source
    theorem GQ2.FoxH.elemDual_separates {A : Type u_2} [AddCommGroup A] (hA₂ : ∀ (a : A), a + a = 0) {a : A} (ha : a ≠ 0) :
    ∃ (lam : ElemDual A), lam a ≠ 0

    The 𝔽₂-dual separates points on an elementary 2-group.

    source
    theorem GQ2.FoxH.card_elemDual {A : Type u_2} [AddCommGroup A] [Finite A] (hA₂ : ∀ (a : A), a + a = 0) :
    Nat.card (ElemDual A) = Nat.card A

    The dimension count #(ElemDual A) = #A for finite elementary A.

    source
    theorem GQ2.FoxH.dualEval_bijective {A : Type u_2} [AddCommGroup A] [Finite A] (hA₂ : ∀ (a : A), a + a = 0) :
    Function.Bijective ⇑(dualEval A)

    Biduality: evaluation A →+ ElemDual (ElemDual A) is bijective for finite elementary A.

    source
    theorem GQ2.FoxH.dualMap_injective {Y : Type u_2} {Z : Type u_3} [AddCommGroup Y] [AddCommGroup Z] (v : Y →+ Z) (hsurj : Function.Surjective ⇑v) :
    Function.Injective ⇑(dualMap v)

    Dualizing a surjection gives an injection.

    source
    theorem GQ2.FoxH.dualMap_surjective {A' : Type u_2} {A : Type u_3} [AddCommGroup A'] [AddCommGroup A] [Finite A] (hA₂ : ∀ (a : A), a + a = 0) (f : A' →+ A) (hinj : Function.Injective ⇑f) :
    Function.Surjective ⇑(dualMap f)

    Dualizing an injection into a finite elementary 2-group gives a surjection (the extension lemma, bundled).

    source
    theorem GQ2.FoxH.two_torsion_of_injective {A' : Type u_2} {A : Type u_3} [AddCommGroup A'] [AddCommGroup A] (f : A' →+ A) (hinj : Function.Injective ⇑f) (hA₂ : ∀ (a : A), a + a = 0) (a' : A') :
    a' + a' = 0

    2-torsion passes to subobjects along an injection.

    source
    theorem GQ2.FoxH.two_torsion_of_surjective {A : Type u_2} {A'' : Type u_3} [AddCommGroup A] [AddCommGroup A''] (g : A →+ A'') (hsurj : Function.Surjective ⇑g) (hA₂ : ∀ (a : A), a + a = 0) (a'' : A'') :
    a'' + a'' = 0

    2-torsion passes to quotients along a surjection.

    source
    theorem GQ2.FoxH.dual_exact_pair {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [AddCommGroup X] [AddCommGroup Y] [AddCommGroup Z] [Finite Z] (hZ₂ : ∀ (z : Z), z + z = 0) (u : X →+ Y) (v : Y →+ Z) (hexact : u.range = v.ker) (lam : ElemDual Y) :
    (dualMap u) lam = 0 ↔ lam ∈ (dualMap v).range

    Dual exactness: dualizing an exact pair is exact (finite elementary target; the factored functional extends via kerLift).

    source
    theorem GQ2.FoxH.dual_ses_exact {A' : Type u_2} {A : Type u_3} {A'' : Type u_4} [AddCommGroup A'] [AddCommGroup A] [AddCommGroup A''] [Finite A''] (hA''₂ : ∀ (a'' : A''), a'' + a'' = 0) (f : A' →+ A) (g : A →+ A'') (hexact : f.range = g.ker) :
    (dualMap g).range = (dualMap f).ker

    The dualized SES is exact in the middle, subgroup form: range g^∨ = ker f^∨.