Documentation

Q2Presentation.Induction.Section7CentralizerCarrier

The centralizer carrier for the Frattini-collapse step #

This file packages the normal subgroup that appears after the Hall--Witt / three-subgroup step of lem:collapse.

For the odd Hall lift Ñ, the previous file proves [K,Ñ] ≤ C_Y(R), where R = Φ(K). Since K and C_Y(R) are both normal in Y, the normal closure of [K,Ñ] is contained in K ∩ C_Y(R).

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

The centralizer of the Frattini layer inside the minimal kernel.

Equations
Instances For
    source
    theorem Q2Presentation.Induction.kernelFrattiniCentralizerInKernel_normal {p : FramedPair} {chief : FirstNonScalarChiefFactor p} (K : KernelMinimal chief.toNonScalarChiefFactor) :
    (kernelFrattiniCentralizerInKernel K).Normal

    The centralizer carrier K ∩ C_Y(R) is normal in the ambient finite target.

    source
    theorem Q2Presentation.Induction.kernel_oddHall_commutator_le_kernel {p : FramedPair} {chief : FirstNonScalarChiefFactor p} (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) :
    ⁅K.Ksub, Ñ⁆ ≤ K.Ksub

    The raw Hall commutator [K,Ñ] lies inside K.

    source
    theorem Q2Presentation.Induction.kernel_oddHall_commutator_normalClosure_le_kernel {p : FramedPair} {chief : FirstNonScalarChiefFactor p} (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) :
    Subgroup.normalClosure ↑⁅K.Ksub, Ñ⁆ ≤ K.Ksub

    The normal closure of the Hall commutator lies inside K.

    source
    theorem Q2Presentation.Induction.kernel_oddHall_commutator_normalClosure_le_frattini_centralizer {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 ↥Ñ) ∧ Subgroup.normalClosure ↑⁅K.Ksub, Ñ⁆ ≤ Subgroup.centralizer ↑(kernelFrattini K)

    The normal closure of [K,Ñ] lies inside the Frattini centralizer.

    source
    theorem Q2Presentation.Induction.kernel_oddHall_commutator_normalClosure_le_centralizerInKernel {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 ↥Ñ) ∧ Subgroup.normalClosure ↑⁅K.Ksub, Ñ⁆ ≤ kernelFrattiniCentralizerInKernel K

    The normal closure of [K,Ñ] lies inside the normal carrier K ∩ C_Y(R).