The index-2 character blockLam (scratch)

The lam input to prop_7_4 / mForm_of_qbar: for a Y-normal l ≤ R of relative index 2, the character λ_l : ↥R → 𝔽₂ cutting R ↠ R/l ≅ 𝔽₂. Additive (blockLam_hom), Y-conjugation invariant (blockLam_conj), and nonzero (blockLam_ne). Self-contained (no prop_7_4).

noncomputable def GQ2.blockLam {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (l : Subgroup Y) : ↥B.frattiniK → ZMod 2

The index-2 character λ_l : ↥R → 𝔽₂ cutting out l ≤ R (R ↠ R/l ≅ 𝔽₂): r ↦ 0 if r ∈ l, else 1.

Equations

• GQ2.blockLam B l r = if ↑r ∈ l then 0 else 1

theorem GQ2.blockLam_eq_zero_iff {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (l : Subgroup Y) (r : ↥B.frattiniK) : blockLam B l r = 0 ↔ ↑r ∈ l

theorem GQ2.blockLam_hom {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (l : Subgroup Y) (hidx : (l.subgroupOf B.frattiniK).index = 2) (r r' : ↥B.frattiniK) : blockLam B l (r * r') = blockLam B l r + blockLam B l r'

Additivity: λ_l(r·r') = λ_l(r) + λ_l(r') — from index-2 product membership (mul_mem_iff_of_index_two).

theorem GQ2.blockLam_conj {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (l : Subgroup Y) (hlN : l.Normal) (hRN : B.frattiniK.Normal) (y r : Y) (hr : r ∈ B.frattiniK) : blockLam B l ⟨y * r * y⁻¹, ⋯⟩ = blockLam B l ⟨r, hr⟩

Y-conjugation invariance: λ_l(y r y⁻¹) = λ_l(r) — because l is Y-normal.

theorem GQ2.blockLam_ne {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (l : Subgroup Y) (hlt : l < B.frattiniK) : blockLam B l ≠ 0

Nonzero: since l < R, some r ∈ R∖l has λ_l(r) = 1.

theorem GQ2.relIndex_two_of_le {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (l : Subgroup Y) (hlR : l ≤ B.frattiniK) (hle2 : l.relIndex B.frattiniK ≤ 2) (hne : l ≠ B.frattiniK) : l.relIndex B.frattiniK = 2

Relative index is exactly 2 for a proper l < R with relIndex ≤ 2 (the DR shape).

hquad: the descended form qbar is quadratic (biadditive polar)

theorem GQ2.comm_mem_R_of_K {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (hRN : B.frattiniK.Normal) (hsq : ∀ k ∈ B.K, k * k ∈ B.frattiniK) {a b : Y} (ha : a ∈ B.K) (hb : b ∈ B.K) : b * a * b⁻¹ * a⁻¹ ∈ B.frattiniK

Commutators of K land in R = Φ(K): [b,a] = b a b⁻¹ a⁻¹ ∈ R — via a[b,a]a⁻¹ = (ab)²(a²b²)⁻¹ ∈ R (squares, hsq) and R-normality.

theorem GQ2.isQuadraticFp2_of_mul {G : Type u_1} [CommGroup G] (qm : G → ZMod 2) (h0 : qm 1 = 0) (hbiadd : ∀ (u v w : G), qm (u * v * w) + qm (u * v) + qm w = qm (u * w) + qm u + qm w + (qm (v * w) + qm v + qm w)) : QuadraticFp2.IsQuadraticFp2 fun (v : Additive G) => qm (Additive.toMul v)

Packaging: a ZMod 2-form on a CommGroup G that is normalized (qm 1 = 0) and has a biadditive multiplicative polar form gives an IsQuadraticFp2 form on Additive G.

theorem GQ2.mkK_mul {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] {a b : Y} (ha : a ∈ B.K) (hb : b ∈ B.K) : ↑⟨a, ⋯⟩ * ↑⟨b, ⋯⟩ = ↑⟨a * b, ⋯⟩

⟦a⟧·⟦b⟧ = ⟦ab⟧ on P/S, in the K-membership form (proof term B.hKP (mul_mem …) matches hspec/blockQbar_beta).

theorem GQ2.blockQbar_beta {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (hRN : B.frattiniK.Normal) (hsq : ∀ k ∈ B.K, k * k ∈ B.frattiniK) (lam : ↥B.frattiniK → ZMod 2) (hlam_hom : ∀ (r r' : ↥B.frattiniK), lam (r * r') = lam r + lam r') (hlam_conj : ∀ (y r : Y) (hr : r ∈ B.frattiniK), lam ⟨y * r * y⁻¹, ⋯⟩ = lam ⟨r, hr⟩) (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (hspec : ∀ (k : Y) (hk : k ∈ B.K), lam ⟨k * k, ⋯⟩ = qbar ↑⟨k, ⋯⟩) {a b : Y} (ha : a ∈ B.K) (hb : b ∈ B.K) : qbar (↑⟨a, ⋯⟩ * ↑⟨b, ⋯⟩) + qbar ↑⟨a, ⋯⟩ + qbar ↑⟨b, ⋯⟩ = lam ⟨b * a * b⁻¹ * a⁻¹, ⋯⟩

The polar form is a conjugated commutator character: β(⟦a⟧,⟦b⟧) = qbar(⟦a⟧⟦b⟧) + qbar⟦a⟧ + qbar⟦b⟧ = λ([b,a]) — the linchpin of biadditivity.

theorem GQ2.blockQbar_map_zero {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] : B.frattiniK.Normal → ∀ (hsq : ∀ k ∈ B.K, k * k ∈ B.frattiniK) (lam : ↥B.frattiniK → ZMod 2) (hlam_hom : ∀ (r r' : ↥B.frattiniK), lam (r * r') = lam r + lam r') (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (hspec : ∀ (k : Y) (hk : k ∈ B.K), lam ⟨k * k, ⋯⟩ = qbar ↑⟨k, ⋯⟩), qbar 1 = 0

qbar 1 = 0 (map_zero): from λ 1 = 0.

theorem GQ2.exists_K_rep {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (v : ↥B.P ⧸ B.S.subgroupOf B.P) : ∃ (k : Y) (hk : k ∈ B.K), ↑⟨k, ⋯⟩ = v

Every class of V = P/S has a K-representative (from KS = P, Blk.gen).

theorem GQ2.blockQbar_polar_add {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (hRN : B.frattiniK.Normal) (hsq : ∀ k ∈ B.K, k * k ∈ B.frattiniK) (lam : ↥B.frattiniK → ZMod 2) (hlam_hom : ∀ (r r' : ↥B.frattiniK), lam (r * r') = lam r + lam r') (hlam_conj : ∀ (y r : Y) (hr : r ∈ B.frattiniK), lam ⟨y * r * y⁻¹, ⋯⟩ = lam ⟨r, hr⟩) (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (hspec : ∀ (k : Y) (hk : k ∈ B.K), lam ⟨k * k, ⋯⟩ = qbar ↑⟨k, ⋯⟩) (u v w : ↥B.P ⧸ B.S.subgroupOf B.P) : qbar (u * v * w) + qbar (u * v) + qbar w = qbar (u * w) + qbar u + qbar w + (qbar (v * w) + qbar v + qbar w)

The multiplicative polar form is biadditive (hquad's core polar_add_left): β(u·v, w) = β(u,w) + β(v,w). Via blockQbar_beta (β = λ(commutator)) + the commutator identity [w, uv] = [w,u]·u[w,v]u⁻¹ + λ's additivity/conj-invariance.

hns: the descended form qbar is nonsingular

noncomputable def GQ2.qbP {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (y : Y) : ZMod 2

Total extension of qbar to Y: qbP y = qbar⟦y⟧ for y ∈ P, else 0.

Equations

• GQ2.qbP B qbar y = if h : y ∈ B.P then qbar ↑⟨y, h⟩ else 0

theorem GQ2.mkP_mul {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] {a b : Y} (ha : a ∈ B.P) (hb : b ∈ B.P) : ↑⟨a, ha⟩ * ↑⟨b, hb⟩ = ↑⟨a * b, ⋯⟩

⟦p⟧·⟦q⟧ = ⟦pq⟧ on P/S (the P-membership form).

theorem GQ2.beta_conj {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (hinv : ∀ (y p : Y) (hp : p ∈ B.P), qbar ↑⟨y * p * y⁻¹, ⋯⟩ = qbar ↑⟨p, hp⟩) (g y q : Y) (hy : y ∈ B.P) (hq : q ∈ B.P) : qbP B qbar (g * y * g⁻¹ * (g * q * g⁻¹)) + qbP B qbar (g * y * g⁻¹) + qbP B qbar (g * q * g⁻¹) = qbP B qbar (y * q) + qbP B qbar y + qbP B qbar q

Y-conjugation invariance of the polar form β(g•a, g•b) = β(a,b) (in qbP terms), from qbar's Y-invariance hinv.

noncomputable def GQ2.betaP {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (y q : Y) : ZMod 2

The polar form as a Y-function via qbP (meaningful for y, q ∈ P).

Equations

• GQ2.betaP B qbar y q = GQ2.qbP B qbar (y * q) + GQ2.qbP B qbar y + GQ2.qbP B qbar q

theorem GQ2.betaP_biadd {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (hbiadd : ∀ (u v w : ↥B.P ⧸ B.S.subgroupOf B.P), qbar (u * v * w) + qbar (u * v) + qbar w = qbar (u * w) + qbar u + qbar w + (qbar (v * w) + qbar v + qbar w)) {y y' q : Y} (hy : y ∈ B.P) (hy' : y' ∈ B.P) (hq : q ∈ B.P) : betaP B qbar (y * y') q = betaP B qbar y q + betaP B qbar y' q

betaP is additive in its first argument (from qbar's polar biadditivity).

theorem GQ2.betaP_one {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (h0 : qbar 1 = 0) (q : Y) : betaP B qbar 1 q = 0

betaP 1 q = 0 (⟦1⟧ = 0 in the polar form).

def GQ2.radSub {Y : Type} [Group Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (hbiadd : ∀ (u v w : ↥B.P ⧸ B.S.subgroupOf B.P), qbar (u * v * w) + qbar (u * v) + qbar w = qbar (u * w) + qbar u + qbar w + (qbar (v * w) + qbar v + qbar w)) (h0 : qbar 1 = 0) : Subgroup Y

The polar radical as a subgroup of Y (contained in P): {y ∈ P | ∀ q ∈ P, β(y,q)=0}. A subgroup by biadditivity/normalization of β.

Equations

• GQ2.radSub B qbar hbiadd h0 = { carrier := {y : Y | y ∈ B.P ∧ ∀ q ∈ B.P, GQ2.betaP B qbar y q = 0}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem GQ2.additive_qbar_absurd {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (h0 : qbar 1 = 0) (hadd : ∀ (a b : ↥B.P ⧸ B.S.subgroupOf B.P), qbar (a * b) = qbar a + qbar b) (hqbar_ne : ∃ (a : ↥B.P ⧸ B.S.subgroupOf B.P), qbar a ≠ 0) (hinv : ∀ (y p : Y) (hp : p ∈ B.P), qbar ↑⟨y * p * y⁻¹, ⋯⟩ = qbar ↑⟨p, hp⟩) : False

Endgame: an additive nonzero Y-invariant qbar : V → 𝔽₂ yields a Y-normal index-2 subgroup of K above R (ker of the character k ↦ qbar⟦k⟧), contradicting lemma_7_1_dual.

theorem GQ2.blockQbar_nonsingular_mul {Y : Type} [Group Y] [Finite Y] {L : Subgroup Y} (B : SectionSeven.MinimalBlock L) [(B.S.subgroupOf B.P).Normal] (hRN : B.frattiniK.Normal) (hsq : ∀ k ∈ B.K, k * k ∈ B.frattiniK) (lam : ↥B.frattiniK → ZMod 2) (hlam_hom : ∀ (r r' : ↥B.frattiniK), lam (r * r') = lam r + lam r') (hlam_conj : ∀ (y r : Y) (hr : r ∈ B.frattiniK), lam ⟨y * r * y⁻¹, ⋯⟩ = lam ⟨r, hr⟩) (qbar : ↥B.P ⧸ B.S.subgroupOf B.P → ZMod 2) (hspec : ∀ (k : Y) (hk : k ∈ B.K), lam ⟨k * k, ⋯⟩ = qbar ↑⟨k, ⋯⟩) (hqbar_ne : ∃ (a : ↥B.P ⧸ B.S.subgroupOf B.P), qbar a ≠ 0) (hinv : ∀ (y p : Y) (hp : p ∈ B.P), qbar ↑⟨y * p * y⁻¹, ⋯⟩ = qbar ↑⟨p, hp⟩) (a : ↥B.P ⧸ B.S.subgroupOf B.P) : a ≠ 1 → ∃ (b : ↥B.P ⧸ B.S.subgroupOf B.P), qbar (a * b) + qbar a + qbar b ≠ 0

hns core (multiplicative): the polar form is non-degenerate — every a ≠ 1 in V=P/S pairs nontrivially. If not, radSub is a nonzero Y-normal subgroup between S and P, so = P by chief; then qbar is additive, contradicting lemma_7_1_dual (additive_qbar_absurd).

theorem GQ2.nonsingular_of_mul {G : Type u_1} [CommGroup G] (qm : G → ZMod 2) (hns : ∀ (a : G), a ≠ 1 → ∃ (b : G), qm (a * b) + qm a + qm b ≠ 0) : QuadraticFp2.Nonsingular fun (v : Additive G) => qm (Additive.toMul v)

Packaging: multiplicative non-degeneracy of qm on a CommGroup gives Nonsingular on Additive.