The odd Hall lift centralizes the Frattini layer

This file packages the immediate consequence of the previous collapse steps for the actual Frattini layer R = Φ(K) of the ⊆-minimal kernel.

• kernelFrattini_le_lower gives R ≤ S;
• tame_oddHall_lift_centralizes_lower gives an odd Hall lift Ñ centralizing S;
• hence Ñ centralizes R;
• since [K,R] ≤ R, the subgroup [K,R] also centralizes Ñ.

The last statement is one of the two concrete premises for the Hall--Witt / three-subgroup argument that will show [K,Ñ] ≤ C_K(R).

theorem Q2Presentation.Induction.tame_oddHall_lift_centralizes_kernelFrattini {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) : ∃ (Ñ : Subgroup p.fst.Y), Odd (Nat.card ↥Ñ) ∧ ∀ r ∈ kernelFrattini K, ∀ n ∈ Ñ, r * n = n * r

The odd Hall lift from the tame quotient centralizes the Frattini layer R = Φ(K), because R ≤ S = chief.lower.

theorem Q2Presentation.Induction.kernel_commutator_frattini_le_frattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ⁅K.Ksub, kernelFrattini K⁆ ≤ kernelFrattini K

The internal commutator [K,R] lies in the Frattini layer R, since R is normal in the ambient finite target.

theorem Q2Presentation.Induction.kernel_commutator_frattini_centralizes_oddHall {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) : ∃ (Ñ : Subgroup p.fst.Y), Odd (Nat.card ↥Ñ) ∧ ⁅⁅K.Ksub, kernelFrattini K⁆, Ñ⁆ = ⊥

For the odd Hall lift Ñ, the subgroup [K,R] centralizes Ñ. This is the [[K,R],Ñ]=1 side of the forthcoming three-subgroup/Hall-Witt step.