§9 concrete block enrichment — SectionNine.blockEnrichment #
Assembles (blockFrame T Blk hE2).Enrichment from the descent (GQ2/BlockDescent.lean),
the form fields (GQ2/BlockFormFields.lean), and the κ⁰ base-class datum. Placed in a
separate module (under namespace SectionNine, preserving the FQN SectionNine.blockEnrichment)
because it consumes SectionNine.kappa0_exists/ActsThroughTame, so it must sit downstream of
GQ2.SectionNine. The two substantive pieces use only the standard axioms:
blockHsimple—V = P/Sis a simple𝔽₂[Y/K]-module (blockPS_exp2exp-2 +Blk.chiefunder theW ↦ WP ≤ ↥P ↦ X ≤ Ysubgroup correspondence);blockHtame— theY/K-action factors through the tame headH(blockLY_smul_eqYviaFoxH.lemma_5_12⟹ the action descendsY/K ↠ Y/L_Y ≅ H, generatorsα σ, α τ).
dat/hdat come from blockKappa0 (= kappa0_exists). The signature takes
F : BoundaryFrame H E (cH := F.alpha, hcH := F.alpha_surjective
for prop_7_4, and the tame generators F.alpha tameSigma/tameTau for htame).
L_Y ◁ Y (the marked normal subgroup), as an instance for Y ⧸ T.LY.
hsimple : V = P/S is a simple 𝔽₂[Y/K]-module #
V = P/S is exponent 2: every element has a K-representative k, and k² ∈ R ≤ S.
hsimple: V = P/S is a simple 𝔽₂[Y/K]-module (nontrivial; the only Y/K-stable
AddSubgroups are ⊥/⊤, by Blk.chief under the subgroup correspondence).
hnt: the Y/K-action on V = P/S is nontrivial — the enrichment-module form of
the block's nontrivial_action field. Only nontriviality is assumed: faithfulness is not
block-derivable (a central
2-part of Y outside K centralizes V), but the capstone only consumed hfaith through
hnt.) The moving pair is (⟦y⟧_K, ⟦p⟧_S): ⟦y⟧•⟦p⟧ = ⟦p⟧ would put y p y⁻¹ p⁻¹ ∈ S
(conjugating the coset relation by p), against nontrivial_action.
htame : the Y/K-action factors through the tame head H #
L_Y acts trivially on V: L_Y/K is a normal 2-subgroup of Y/K acting on the simple
module V, hence trivial by FoxH.lemma_5_12; pull back to the Y-conjugation action.
The descended Y/L_Y-action on V — blockActVY descends because L_Y acts trivially
(blockLY_smul_eqY); mirrors blockActV's descent through Y/K.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Y/L_Y-action on mk' L_Y y reduces to the Y-conjugation action of y.
htame: the Y/K-action on V factors through the tame head H (α : Ttame ↠ H);
the action descends Y/K ↠ Y/L_Y ≅ H, generators α σ, α τ satisfy the tame relation.
dat/hdat and the final assembly #
The κ⁰ base-class datum for q̄_λ, from the proved kappa0_exists (Lemma 6.3),
discharging its hsimple/htame hypotheses via blockHsimple/blockHtame.
Equations
- ⋯ = ⋯
Instances For
The concrete block enrichment (the §9 induction): the full RF.Enrichment record assembled from
the §9 induction descent (blockDescend*/blockActV), the §9 induction form fields
(blockQ/blockQbar/…), and the κ⁰ datum (blockKappa0). Takes the boundary frame F
(supplying cH := F.alpha for prop_7_4 and the tame generators for htame). Axiom-clean
modulo kappa0_exists (the §9 induction).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Paper-tag ledger (auto-generated by paperforge; do not edit) #
- Lemma 6.3 = ⟦lem-basedetclass⟧