The concrete block-form enrichment fields (scratch)

Assembly of the §9 block enrichment's non-κ⁰ fields for the concrete frame RF = blockFrame T Blk hE2: q/qbar (from prop_7_4 + mForm_of_qbar), the coupling hqbar, the radical/vanishing clauses hrad/hTzero, invariance hinv, quadraticity/ nonsingularity hquad/hns (the §9 induction packaging), and the frame-local cover square hq.

All per-λ items are stated over l : BlockDR T Blk (defeq to RF.DR) with hlne : l.1 ≠ Blk.frattiniK (defeq-encoding of l ≠ RF.zeroDR); the final assembly (the §9 induction) drops them into the record.

@[reducible, inline]

abbrev GQ2.BlockDR {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) : Type

The scalar-character index type; reducibly (blockFrame T Blk hE2).DR.

Equations

• GQ2.BlockDR T Blk = { R' : Subgroup Y // R'.Normal ∧ R' ≤ Blk.frattiniK ∧ R'.relIndex Blk.frattiniK ≤ 2 }

instance GQ2.blockDR_normal {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (l : BlockDR T Blk) : (↑l).Normal

Each l : BlockDR is Y-normal (its defining property), as an instance.

theorem GQ2.blockHRn {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) : Blk.frattiniK.Normal

R = Φ(K) is Y-normal.

theorem GQ2.blockHsq {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (k : Y) : k ∈ Blk.K → k * k ∈ Blk.frattiniK

k² ∈ R for k ∈ K (public route: squares generate Φ(K)).

theorem GQ2.blockHidx {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : ((↑l).subgroupOf Blk.frattiniK).index = 2

The relative index is exactly 2 for a proper l.

theorem GQ2.blockHlt {H E : Type} [Group H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : ↑l < Blk.frattiniK

l.1 < Blk.frattiniK.

The Prop 7.4 / mForm packages

noncomputable def GQ2.blockProp74 {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : ∃ (qbar : ↥Blk.P ⧸ Blk.S.subgroupOf Blk.P → ZMod 2), (∀ (k : Y) (hk : k ∈ Blk.K), blockLam Blk ↑l ⟨k * k, ⋯⟩ = qbar ↑⟨k, ⋯⟩) ∧ qbar ≠ 0 ∧ ∀ (y p : Y) (hp : p ∈ Blk.P), qbar ↑⟨y * p * y⁻¹, ⋯⟩ = qbar ↑⟨p, hp⟩

The Prop 7.4 output existential for the block character λ_l.

Equations

• ⋯ = ⋯

noncomputable def GQ2.blockQbarRaw {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : ↥Blk.P ⧸ Blk.S.subgroupOf Blk.P → ZMod 2

The descended form q̄_λ on V = P/S (Prop 7.4's output, multiplicative model).

Equations

• GQ2.blockQbarRaw T Blk cH hcH l hlne = ⋯.choose

noncomputable def GQ2.blockMForm {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : ∃ (qM : ↥(Subgroup.map (QuotientGroup.mk' Blk.frattiniK) Blk.K) → ZMod 2), (∀ (k : Y) (hk : k ∈ Blk.K), qM ⟨(QuotientGroup.mk' Blk.frattiniK) k, ⋯⟩ = blockLam Blk ↑l ⟨k * k, ⋯⟩) ∧ (∀ (t : Y ⧸ Blk.frattiniK) (ht : t ∈ Subgroup.map (QuotientGroup.mk' Blk.frattiniK) (Blk.K ⊓ Blk.S ⊔ Blk.frattiniK)) (m : Y ⧸ Blk.frattiniK) (hm : m ∈ Subgroup.map (QuotientGroup.mk' Blk.frattiniK) Blk.K), SectionEight.polarMul qM (fun (a b : ↥(Subgroup.map (QuotientGroup.mk' Blk.frattiniK) Blk.K)) => ⟨↑a * ↑b, ⋯⟩) ⟨t, ⋯⟩ ⟨m, hm⟩ = 0) ∧ ∀ (t : Y ⧸ Blk.frattiniK) (ht : t ∈ Subgroup.map (QuotientGroup.mk' Blk.frattiniK) (Blk.K ⊓ Blk.S ⊔ Blk.frattiniK)), qM ⟨t, ⋯⟩ = 0

The mForm output existential (the M_B-level square form).

Equations

• ⋯ = ⋯

noncomputable def GQ2.blockQ {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : ↥(Subgroup.map (QuotientGroup.mk' Blk.frattiniK) Blk.K) → ZMod 2

The M_B-level square form q_λ (the Enrichment q field).

Equations

• GQ2.blockQ T Blk cH hcH l hlne = ⋯.choose

noncomputable def GQ2.blockQbar {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : Additive (↥Blk.P ⧸ Blk.S.subgroupOf Blk.P) → ZMod 2

The descended form on Vmod = Additive (P/S) (the Enrichment qbar field).

Equations

• GQ2.blockQbar T Blk cH hcH l hlne v = GQ2.blockQbarRaw T Blk cH hcH l hlne (Additive.toMul v)

Direct consequences (Prop 7.4 / mForm clauses)

theorem GQ2.blockHspec {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (k : Y) (hk : k ∈ Blk.K) : blockLam Blk ↑l ⟨k * k, ⋯⟩ = blockQbarRaw T Blk cH hcH l hlne ↑⟨k, ⋯⟩

hspec: λ(k²) = q̄(⟦k⟧).

theorem GQ2.blockHne {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : blockQbarRaw T Blk cH hcH l hlne ≠ 0

q̄_λ ≠ 0 (Prop 7.4 nonzero).

theorem GQ2.blockHinvRaw {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (y p : Y) (hp : p ∈ Blk.P) : blockQbarRaw T Blk cH hcH l hlne ↑⟨y * p * y⁻¹, ⋯⟩ = blockQbarRaw T Blk cH hcH l hlne ↑⟨p, hp⟩

Raw Y-invariance of q̄_λ (Prop 7.4 third clause).

theorem GQ2.blockHval {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (k : Y) (hk : k ∈ Blk.K) : blockQ T Blk cH hcH l hlne ⟨(QuotientGroup.mk' Blk.frattiniK) k, ⋯⟩ = blockLam Blk ↑l ⟨k * k, ⋯⟩

mForm value clause: q_λ(π_B k) = λ(k²).

theorem GQ2.blockHrad {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (t : Y ⧸ Blk.frattiniK) (ht : t ∈ Subgroup.map (QuotientGroup.mk' Blk.frattiniK) (Blk.K ⊓ Blk.S ⊔ Blk.frattiniK)) (m : Y ⧸ Blk.frattiniK) (hm : m ∈ Subgroup.map (QuotientGroup.mk' Blk.frattiniK) Blk.K) : SectionEight.polarMul (blockQ T Blk cH hcH l hlne) (fun (a b : ↥(Subgroup.map (QuotientGroup.mk' Blk.frattiniK) Blk.K)) => ⟨↑a * ↑b, ⋯⟩) ⟨t, ⋯⟩ ⟨m, hm⟩ = 0

hrad: T_B lies in the polar radical of q_λ.

theorem GQ2.blockHTzero {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (t : Y ⧸ Blk.frattiniK) (ht : t ∈ Subgroup.map (QuotientGroup.mk' Blk.frattiniK) (Blk.K ⊓ Blk.S ⊔ Blk.frattiniK)) : blockQ T Blk cH hcH l hlne ⟨t, ⋯⟩ = 0

hTzero: q_λ vanishes on T_B.

Quadraticity, nonsingularity

theorem GQ2.blockHquad {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : QuadraticFp2.IsQuadraticFp2 (blockQbar T Blk cH hcH l hlne)

hquad: q̄_λ is a quadratic form (biadditive polar).

theorem GQ2.blockHns {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : QuadraticFp2.Nonsingular (blockQbar T Blk cH hcH l hlne)

hns: q̄_λ is nonsingular.

Invariance packaged over the C = Y/K action

theorem GQ2.blockHinv {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) [(Blk.S.subgroupOf Blk.P).Normal] [Blk.K.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : QuadraticFp2.IsInvariant (Y ⧸ Blk.K) (blockQbar T Blk cH hcH l hlne)

hinv: q̄_λ is invariant under the Y/K-action (blockActV).

The coupling hqbar : q_λ = q̄_λ ∘ descend

theorem GQ2.blockHqbar {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup E] {Y : Type} [Group Y] [Finite Y] (T : MarkedTarget H E Y) (Blk : SectionSeven.MinimalBlock T.LY) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) [Blk.frattiniK.Normal] [(Blk.S.subgroupOf Blk.P).Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (m : ↥(blockMB Blk)) : blockQ T Blk cH hcH l hlne m = blockQbarRaw T Blk cH hcH l hlne ((blockDescend Blk) m)

hqbar: q_λ(m) = q̄_λ(descend m).

The frame-local cover square hq

noncomputable def GQ2.blockScalarCover {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) (hE2 : ∀ (e : E), e ^ 2 = 1) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) : SectionEight.CentralCover (Y ⧸ Blk.frattiniK)

The scalar cover of l (reducibly RF.scalarCover l (·)).

Equations

• GQ2.blockScalarCover T Blk hE2 l hlne = (GQ2.SectionNine.blockFrame T Blk hE2).scalarCover l ⋯

theorem GQ2.blockScalarCover_p {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) (hE2 : ∀ (e : E), e ^ 2 = 1) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (y : Y) : (blockScalarCover T Blk hE2 l hlne).p ((QuotientGroup.mk' ↑l) y) = (QuotientGroup.mk' Blk.frattiniK) y

The cover projection sends ⟦y⟧_l to ⟦y⟧_R.

theorem GQ2.blockZ_pow_lam {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) (hE2 : ∀ (e : E), e ^ 2 = 1) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (r : Y) (hr : r ∈ Blk.frattiniK) : (QuotientGroup.mk' ↑l) r = (blockScalarCover T Blk hE2 l hlne).z ^ (blockLam Blk ↑l ⟨r, hr⟩).val

Auxiliary: for r ∈ R, the class ⟦r⟧_{l} = z^{λ_l(r)} in the cover.

theorem GQ2.blockHq {H E : Type} [Group H] [TopologicalSpace H] [DiscreteTopology H] [Finite H] [CommGroup 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) (cH : ↑Ttame.toProfinite.toTop →ₜ* H) (hcH : Function.Surjective ⇑cH) [Blk.frattiniK.Normal] (l : BlockDR T Blk) (hlne : ↑l ≠ Blk.frattiniK) (x : (blockScalarCover T Blk hE2 l hlne).cover) (hx : (blockScalarCover T Blk hE2 l hlne).p x ∈ Subgroup.map (QuotientGroup.mk' Blk.frattiniK) Blk.K) : x * x = (blockScalarCover T Blk hE2 l hlne).z ^ (blockQ T Blk cH hcH l hlne ⟨(blockScalarCover T Blk hE2 l hlne).p x, hx⟩).val

hq: the cover square relation x² = z^{q_λ(p x)} on M_B.

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

• Prop 7.4 = ⟦prop-simpleheaddet⟧