Section 7 fourth-power map kernel

This file continues the manuscript proof of lem:collapse at the literal fourth-power map k ↦ k^4. Once the Frattini layer R = Phi(K) centralizes K, the fourth-power map is multiplicative on K. For the odd Hall witness Ñ, the lower-scalar centralizer result makes f([k,n]) = 1, so [K,Ñ] lies inside the fourth-power kernel.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernel_fourth_mem_frattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (k : p.fst.Y) (hk : k ∈ K.Ksub) : k ^ 4 ∈ kernelFrattini K

Fourth powers of elements of K lie in the literal Frattini layer R = Phi(K).

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernel_mul_four_eq_mul_four {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (a b : p.fst.Y) (ha : a ∈ K.Ksub) (hb : b ∈ K.Ksub) : (a * b) ^ 4 = a ^ 4 * b ^ 4

On K, the fourth-power map is multiplicative.

def Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelFourthPowerKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Subgroup p.fst.Y

The kernel of the fourth-power map on K, viewed as an ambient subgroup of Y.

Equations

• Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelFourthPowerKernel chief K = { carrier := {x : p.fst.Y | x ∈ K.Ksub ∧ x ^ 4 = 1}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelFourthPowerKernel_normal {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : (kernelFourthPowerKernel chief K).Normal

The fourth-power kernel is normal in the ambient target Y.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernel_fourth_commute_oddHall {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hÑodd : Odd (Nat.card ↥Ñ)) (k n : p.fst.Y) (hk : k ∈ K.Ksub) (hn : n ∈ Ñ) : k ^ 4 * n = n * k ^ 4

An odd Hall element commutes with the fourth power of any kernel element.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernel_oddHall_commutator_fourth_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hÑodd : Odd (Nat.card ↥Ñ)) (k n : p.fst.Y) (hk : k ∈ K.Ksub) (hn : n ∈ Ñ) : ⁅k, n⁆ ^ 4 = 1

The manuscript calculation f([k,n]) = 1 for the fourth-power map f(k)=k^4.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernel_oddHall_commutatorSub_le_fourthPowerKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hÑodd : Odd (Nat.card ↥Ñ)) : ⁅K.Ksub, Ñ⁆ ≤ kernelFourthPowerKernel chief K

The raw Hall-commutator subgroup [K,Ñ] lies in the fourth-power kernel.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalFourthPowerForWitnessData_of_oddHall {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hÑodd : Odd (Nat.card ↥Ñ)) : Nonempty (KernelMinimalFourthPowerForWitnessData chief K Ñ)

Witness-specific fourth-power kernel data for the odd Hall witness.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalFourthPowerMapKernelData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s t : p.fst.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : Nonempty (KernelMinimalFourthPowerMapKernelData chief K)

The full lowered fourth-power map-kernel datum from the tame relation.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalFourthPowerCandidateData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s t : p.fst.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : Nonempty (KernelMinimalFourthPowerCandidateData chief K)

Immediate candidate-level corollary of the map-kernel datum.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimal_K_fourth_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s t : p.fst.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1

The final K^4 = 1 conclusion over the corrected manuscript kernel.