Documentation

GQ2.Block.HeadDat

The head-inflated block enrichment (`blockEnrichmentD`) #

Substrate for the c3-G0 head-inflation reshape (docs/orchestration/p16d6e4aA-p4-tame-package.md, authoritative; the frozen TamePackage/hpack shape is refuted there). This leaf builds:

the head identification headEquiv : Y⧸L_Y ≃* H and the H-action on V = P/S (headAct, the blockHtame construction as data), with the C-head blockPiCH : Y⧸K →* H and the compatibility c • v = blockPiCH c • v;
the faithful head quotient HVq := H ⧸ headActKer with its descended action (hvAct), faithfulness by construction (hvAct_faithful), and the full projection blockProjF : Y⧸K →* HVq;
the tame pair hvSigma/hvTau (classes of α σ, α τ) with generation and the tame relation, the invariance/simplicity transports, and the H_V-level κ⁰ datum blockDatHV := (kappa0_exists_tame …).choose;
blockEnrichmentD — blockEnrichment with dat := (blockDatHV).reindexHom blockProjF (definitionally transparent: blockEnrichmentD_dat_eq is rfl), so every QZero/Q0loc evaluation transports down graphPullback_reindexHom/Q0loc_reindexHom to C := HVq, where every boundary lift is tame-factored through the fixed mk' ∘ F.alpha (the boundary equation's head component, boundaryLift_head_*), hfaith holds by construction, and the wild slots are literally 1;
the boundary-equation head components boundaryLift_head_gammaA/boundaryLift_head_local (the per-lift tame factorization at the head — rfl-level from IsBoundaryLift).

Everything here is std-3 (no sorries; kappa0_exists_tame is the proved the §9 induction theorem). Consumers: P4c (local residue twins at blockEnrichmentD), P4d (Γ_A twins), P4e (the hypothesis-free G0-obtain), P5 (the ThmFourTwo En-swap).

The head action as data (the `blockHtame` construction, unpacked) #

noncomputable def GQ2.SectionNine.headEquiv {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) :

Y ⧸ T.LY ≃* H

The head identification Y ⧸ L_Y ≃* H: π_Y descends with kernel exactly L_Y.

Equations

GQ2.SectionNine.headEquiv T = MulEquiv.ofBijective (QuotientGroup.lift T.LY T.piY ⋯) ⋯

Instances For

@[reducible]

noncomputable def GQ2.SectionNine.headAct {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] :

DistribMulAction H (Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P))

The H-action on V = P/S: the Y⧸L_Y-conjugation action (blockActLY) transported along headEquiv.symm.

Equations

GQ2.SectionNine.headAct T Blk = DistribMulAction.compHom (Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P)) (GQ2.SectionNine.headEquiv T).symm.toMonoidHom

Instances For

noncomputable def GQ2.SectionNine.blockPiCH {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [Blk.K.Normal] :

Y ⧸ Blk.K →* H

The C-target's head map Y⧸K →* H (defeq to (blockFrame T Blk hE2).TC.piY).

Equations

GQ2.SectionNine.blockPiCH T Blk = QuotientGroup.lift Blk.K T.piY ⋯

Instances For

theorem GQ2.SectionNine.blockPiCH_compat {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (c : Y ⧸ Blk.K) (v : Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P)) :

c • v = (blockPiCH T Blk) c • v

The Y⧸K-action on V is the blockPiCH-pullback of the H-action (the blockHtame compatibility clause, as a standalone fact).

The faithful head quotient `H_V` #

noncomputable def GQ2.SectionNine.headActKer {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] :

Subgroup H

The kernel of the H-action on V (the acts-trivially subgroup).

Equations

GQ2.SectionNine.headActKer T Blk = { carrier := {h : H | ∀ (v : Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P)), h • v = v}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

Instances For

instance GQ2.SectionNine.headActKer_normal {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] :

(headActKer T Blk).Normal

@[reducible, inline]

abbrev GQ2.SectionNine.HVq {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] :

The faithful head quotient H_V := H ⧸ ker(action).

Equations

GQ2.SectionNine.HVq T Blk = (H ⧸ GQ2.SectionNine.headActKer T Blk)

Instances For

@[reducible]

noncomputable def GQ2.SectionNine.hvAct {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] :

DistribMulAction (HVq T Blk) (Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P))

The descended (faithful) H_V-action on V.

Equations

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

Instances For

theorem GQ2.SectionNine.hvAct_faithful {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (g : HVq T Blk) :

(∀ (v : Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P)), g • v = v) → g = 1

Faithfulness by construction: the H_V-action on V is faithful — the hfaith input of the local residue chain, free at the faithful head quotient.

noncomputable def GQ2.SectionNine.blockProjF {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] :

Y ⧸ Blk.K →* HVq T Blk

The full projection Y⧸K →* H_V (head, then faithful quotient).

Equations

GQ2.SectionNine.blockProjF T Blk = (QuotientGroup.mk' (GQ2.SectionNine.headActKer T Blk)).comp (GQ2.SectionNine.blockPiCH T Blk)

Instances For

theorem GQ2.SectionNine.blockProjF_compat {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (c : Y ⧸ Blk.K) (v : Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P)) :

c • v = (blockProjF T Blk) c • v

The Y⧸K-action on V is the blockProjF-pullback of the faithful H_V-action.

The tame pair in `H_V` and the transports #

noncomputable def GQ2.SectionNine.hvSigma {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) :

HVq T Blk

The σ-generator of the tame pair in H_V: the class of α(tameSigma).

Equations

GQ2.SectionNine.hvSigma T Blk F = (QuotientGroup.mk' (GQ2.SectionNine.headActKer T Blk)) (F.alpha GQ2.tameSigma)

Instances For

noncomputable def GQ2.SectionNine.hvTau {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) :

HVq T Blk

The τ-generator of the tame pair in H_V: the class of α(tameTau).

Equations

GQ2.SectionNine.hvTau T Blk F = (QuotientGroup.mk' (GQ2.SectionNine.headActKer T Blk)) (F.alpha GQ2.tameTau)

Instances For

theorem GQ2.SectionNine.hv_gen {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) :

Subgroup.closure {hvSigma T Blk F, hvTau T Blk F} = ⊤

H_V is generated by the tame pair (image of gen_ttame_quotient at F.alpha).

theorem GQ2.SectionNine.hv_rel {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) :

(hvSigma T Blk F)⁻¹ * hvTau T Blk F * hvSigma T Blk F = hvTau T Blk F ^ 2

The tame relation in H_V (image of tame_relation through α and the quotient).

theorem GQ2.SectionNine.hv_inv {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) :

QuadraticFp2.IsInvariant (HVq T Blk) (blockQbar T Blk F.alpha ⋯ l hlne)

Invariance of q̄_λ under the faithful H_V-action (transport of blockHinv).

theorem GQ2.SectionNine.hv_simple {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (W : AddSubgroup (Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P))) :

(∀ (g : HVq T Blk), ∀ w ∈ W, g • w ∈ W) → W = ⊥ ∨ W = ⊤

Simplicity of V under the faithful H_V-action (transport of blockHsimple).

The `H_V`-level κ⁰ datum and the head-inflated enrichment #

noncomputable def GQ2.SectionNine.blockKappa0HV {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) :

∃ (dat : FactorSet (HVq T Blk) (Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P))), IsEquivariantFactorSet (blockQbar T Blk F.alpha ⋯ l hlne) dat

The H_V-level κ⁰ existential: Lemma 6.3 (kappa0_exists_tame, proved the §9 induction) at the faithful head quotient with the tame pair (hvSigma, hvTau).

Equations

⋯ = ⋯

Instances For

noncomputable def GQ2.SectionNine.blockDatHV {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) :

FactorSet (HVq T Blk) (Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P))

The chosen H_V-level base-class datum.

Equations

GQ2.SectionNine.blockDatHV T Blk F l hlne = ⋯.choose

Instances For

theorem GQ2.SectionNine.blockDatHV_spec {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (F : BoundaryFrame H E) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) :

IsEquivariantFactorSet (blockQbar T Blk F.alpha ⋯ l hlne) (blockDatHV T Blk F l hlne)

noncomputable def GQ2.SectionNine.blockEnrichmentD {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [Blk.frattiniK.Normal] [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) (F : BoundaryFrame H E) :

(blockFrame T Blk hE2).Enrichment

The head-inflated block enrichment (the Γ_A Gauss-sum package): blockEnrichment with the κ⁰ datum replaced by the definitionally-transparent inflation (blockDatHV …).reindexHom blockProjF of the faithful-head-quotient datum — every other field (module, action, forms, descent) is blockEnrichment's own. At this enrichment every QZero/Q0loc evaluation transports down graphPullback_reindexHom to C := H_V, where every boundary lift is tame-factored through the fixed mk' ∘ F.alpha and hfaith holds by construction (hvAct_faithful) — see docs/orchestration/p16d6e4aA-p4-tame-package.md.

Equations

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

Instances For

The boundary equation's head component #

Every boundary lift of either source is tame-factored at the head, through the fixed F.alpha — the first component of IsBoundaryLift, rfl-deep. This replaces the refuted per-lift hpack factorizations: composing with mk' (headActKer) gives the H_V-level factorization through mk' ∘ F.alpha, uniformly in ρ.

theorem GQ2.SectionNine.boundaryLift_head_gammaA {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bA F (blockFrame T Blk hE2).TC) (γ : ↑GammaA.toProfinite.toTop) :

(blockFrame T Blk hE2).TC.piY (↑↑ρ γ) = F.alpha (B.tameA γ)

Γ_A version: TC.piY ∘ ρ = α ∘ tameA.

theorem GQ2.SectionNine.boundaryLift_head_local {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] [TopologicalSpace E] [DiscreteTopology E] [Finite E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (hE2 : ∀ (e : E), e ^ 2 = 1) (B : BoundaryMaps) (F : BoundaryFrame H E) (ρ : BoundaryLifts B.bF F (blockFrame T Blk hE2).TC) (γ : AbsGalQ2) :

(blockFrame T Blk hE2).TC.piY (↑↑ρ γ) = F.alpha (B.tameF γ)

Local version: TC.piY ∘ ρ = α ∘ tameF.

theorem GQ2.SectionNine.blockPiCH_eq_TC_piY {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [TopologicalSpace Y] [DiscreteTopology Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) [Blk.K.Normal] (hE2 : ∀ (e : E), e ^ 2 = 1) :

blockPiCH T Blk = (blockFrame T Blk hE2).TC.piY

The block frame's C-head is blockPiCH (definitional alignment for the consumers).

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

Lemma 6.3 = ⟦lem-basedetclass⟧