The chief-dichotomy branch for the Frattini centralizer

This file proves the formal branch split used in lem:collapse after the Hall--Witt step. For the normal closure D of [K,Ñ], the subgroup D ⊔ S lies between S and P, hence chief-ness gives D ⊔ S = S or D ⊔ S = P.

The = P branch is already enough to force K ∩ C_Y(R) = K by the ⊆-minimality of K, hence [K,R]=1. The other branch, D ≤ S, is the remaining representation-theoretic contradiction branch.

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

The normal closure of the Hall commutator [K,Ñ].

Equations

• Q2Presentation.Induction.kernelOddHallCommutatorClosure K Ñ = Subgroup.normalClosure ↑⁅K.Ksub, Ñ⁆

theorem Q2Presentation.Induction.kernelOddHallCommutatorClosure_normal {p : FramedPair} {chief : FirstNonScalarChiefFactor p} (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) : (kernelOddHallCommutatorClosure K Ñ).Normal

The Hall-commutator closure is normal.

theorem Q2Presentation.Induction.kernelOddHallCommutatorClosure_le_upper {p : FramedPair} {chief : FirstNonScalarChiefFactor p} (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) : kernelOddHallCommutatorClosure K Ñ ≤ chief.upper

The Hall-commutator closure lies in the chief upper term.

theorem Q2Presentation.Induction.kernelOddHallCommutatorClosure_sup_lower_eq_lower_or_upper {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) : kernelOddHallCommutatorClosure K Ñ ⊔ chief.lower = chief.lower ∨ kernelOddHallCommutatorClosure K Ñ ⊔ chief.lower = chief.upper

Chief-ness gives the two branches for normalClosure([K,Ñ]) ⊔ S.

theorem Q2Presentation.Induction.kernelFrattiniCentralizerInKernel_eq_kernel_of_hallClosure_sup_lower_eq_upper {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hcent : kernelOddHallCommutatorClosure K Ñ ≤ kernelFrattiniCentralizerInKernel K) (hjoin : kernelOddHallCommutatorClosure K Ñ ⊔ chief.lower = chief.upper) : kernelFrattiniCentralizerInKernel K = K.Ksub

If the Hall-commutator closure maps onto the chief factor, then the Frattini centralizer inside K is all of K.

theorem Q2Presentation.Induction.kernel_commutator_frattini_eq_bot_of_hallClosure_sup_lower_eq_upper {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hcent : kernelOddHallCommutatorClosure K Ñ ≤ kernelFrattiniCentralizerInKernel K) (hjoin : kernelOddHallCommutatorClosure K Ñ ⊔ chief.lower = chief.upper) : ⁅K.Ksub, kernelFrattini K⁆ = ⊥

The onto-chief branch forces the Frattini layer R = Φ(K) to centralize K.

theorem Q2Presentation.Induction.hallCommutatorClosure_le_lower_or_kernelFrattini_central {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hcent : kernelOddHallCommutatorClosure K Ñ ≤ kernelFrattiniCentralizerInKernel K) : kernelOddHallCommutatorClosure K Ñ ≤ chief.lower ∨ ⁅K.Ksub, kernelFrattini K⁆ = ⊥

The dichotomy after Hall--Witt: either the Hall commutator already lies below S, or R is central in K.