The dévissage induction: prop_5_15 from the simple case

prop_5_15_of_simple: if IsSelfDual t B holds for every simple finite elementary-2 C-module B (hypothesis hsimp — the split/ramified dispatch, the other the Prop. 5.15 proof half), then it holds for every finite elementary-2 C-module A.

Strong induction on Nat.card A:

• Subsingleton A — the zero module carries the trivial action, so trivialSelfDual (the Prop. 5.15 proof part (i), proved) applies;
• IsSimpleModTwo C A — the hypothesis hsimp;
• otherwise A has a C-stable additive subgroup W ∉ {⊥, ⊤}; the short exact sequence 0 → W → A → A ⧸ W → 0 (with the transported actions below) has both ends of strictly smaller cardinality, so the inductive hypothesis applies to them, and lemma_5_11 (the dévissage proof, proved — the mapping-cone two-out-of-three for IsSelfDual) yields the middle.

Infrastructure (reusable): the transported actions stableSubAction on ↥W and stableQuotAction on A ⧸ W for a C-stable W, the equivariance of W.subtype and QuotientAddGroup.mk' W, exactness, the char-2 transfer to both subquotients, and the strict cardinality drops.

Glue (proved): GQ2.FoxH.prop_5_15 in GQ2/DualityAssembly.lean composes prop_5_15_of_simple t ht hw hgen with the simple-case assembly selfDual_of_simple (dispatched via the tau_split_or_ramified dichotomy). Paper: Prop. 5.15, proof by dévissage along a composition series (§5.3); Ax = ∅ (std-3).

@[reducible]

def GQ2.FoxH.stableSubAction {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (W : AddSubgroup A) (hW : ∀ (g : C), ∀ w ∈ W, g • w ∈ W) : DistribMulAction C ↥W

The restricted action on a C-stable additive subgroup.

Equations

• GQ2.FoxH.stableSubAction W hW = { smul := fun (c : C) (w : ↥W) => ⟨c • ↑w, ⋯⟩, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

@[reducible]

def GQ2.FoxH.stableQuotAction {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (W : AddSubgroup A) (hW : ∀ (g : C), ∀ w ∈ W, g • w ∈ W) : DistribMulAction C (A ⧸ W)

The descended action on the quotient by a C-stable additive subgroup.

Equations

• GQ2.FoxH.stableQuotAction W hW = { smul := fun (c : C) => ⇑(QuotientAddGroup.map W W (DistribSMul.toAddMonoidHom A c) ⋯), mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

theorem GQ2.FoxH.stableSubAction_subtype_equivariant {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (W : AddSubgroup A) (hW : ∀ (g : C), ∀ w ∈ W, g • w ∈ W) (c : C) (w : ↥W) : W.subtype (c • w) = c • W.subtype w

W.subtype is C-equivariant for the restricted action.

theorem GQ2.FoxH.stableQuotAction_mk'_equivariant {C : Type u_1} [Group C] {A : Type u_2} [AddCommGroup A] [DistribMulAction C A] (W : AddSubgroup A) (hW : ∀ (g : C), ∀ w ∈ W, g • w ∈ W) (c : C) (a : A) : (QuotientAddGroup.mk' W) (c • a) = c • (QuotientAddGroup.mk' W) a

QuotientAddGroup.mk' W is C-equivariant for the descended action.

theorem GQ2.FoxH.subtype_range_eq_mk'_ker {A : Type u_2} [AddCommGroup A] (W : AddSubgroup A) : W.subtype.range = (QuotientAddGroup.mk' W).ker

Exactness of 0 → W → A → A ⧸ W → 0 at the middle.

theorem GQ2.FoxH.two_torsion_sub {A : Type u_2} [AddCommGroup A] (W : AddSubgroup A) (hA₂ : ∀ (a : A), a + a = 0) (w : ↥W) : w + w = 0

Char-2 transfers to a subgroup.

theorem GQ2.FoxH.two_torsion_quot {A : Type u_2} [AddCommGroup A] (W : AddSubgroup A) (hA₂ : ∀ (a : A), a + a = 0) (q : A ⧸ W) : q + q = 0

Char-2 transfers to a quotient.

theorem GQ2.FoxH.card_lt_of_ne_top {A : Type u_2} [AddCommGroup A] [Finite A] (W : AddSubgroup A) (hWtop : W ≠ ⊤) : Nat.card ↥W < Nat.card A

A proper additive subgroup has strictly smaller cardinality (via Lagrange: the quotient is nontrivial).

theorem GQ2.FoxH.card_quot_lt_of_ne_bot {A : Type u_2} [AddCommGroup A] [Finite A] (W : AddSubgroup A) (hWbot : W ≠ ⊥) : Nat.card (A ⧸ W) < Nat.card A

The quotient by a nonzero additive subgroup has strictly smaller cardinality.

theorem GQ2.FoxH.prop_5_15_of_simple {C : Type u_1} [Group C] [Finite C] (t : Marking C) (ht : t.TameRel) (hw : t.WildRel) (hgen : t.Generates) (hsimp : ∀ (B : Type u) [inst : AddCommGroup B] [inst_1 : DistribMulAction C B] [inst_2 : Finite B], (∀ (b : B), b + b = 0) → IsSimpleModTwo C B → IsSelfDual t B) {A : Type u} [AddCommGroup A] [DistribMulAction C A] [Finite A] (hA₂ : ∀ (a : A), a + a = 0) : IsSelfDual t A

Prop 5.15, dévissage half (the Prop. 5.15 proof): IsSelfDual for all finite elementary-2 C-modules, parameterized over the simple case (hsimp — the split/ramified dispatch). Strong induction on Nat.card A; the induction step is lemma_5_11 (the dévissage proof) along 0 → W → A → A ⧸ W → 0 for a C-stable W ∉ {⊥, ⊤}; the subsingleton base is trivialSelfDual (the Prop. 5.15 proof part (i)).

Paper-tag ledger (auto-generated by paperforge; do not edit)

• Prop 5.15 = ⟦prop-defduality⟧