The lower branch makes the odd Hall lift trivial on the chief factor #
This file starts the remaining branch of lem:collapse.
If the normal closure of [K,Ñ] lies below S, then [K,Ñ] ≤ S. Since the
odd Hall lift Ñ centralizes S, and K ⊔ S = P, it follows that
[P,Ñ] ≤ S: the odd Hall lift acts trivially on the chief factor P/S.
theorem
Q2Presentation.Induction.kernel_oddHall_commutator_le_lower_of_closure_le_lower
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(Ñ : Subgroup p.fst.Y)
(hDle : kernelOddHallCommutatorClosure K Ñ ≤ chief.lower)
:
In the lower branch, the raw Hall commutator [K,Ñ] lies below S.
theorem
Q2Presentation.Induction.chief_upper_oddHall_commutator_le_lower_of_closure_le_lower
{p : FramedPair}
(chief : FirstNonScalarChiefFactor p)
(K : KernelMinimal chief.toNonScalarChiefFactor)
(Ñ : Subgroup p.fst.Y)
(hÑodd : Odd (Nat.card ↥Ñ))
(hDle : kernelOddHallCommutatorClosure K Ñ ≤ chief.lower)
:
Lower branch consequence. If the normal closure of [K,Ñ] is below
S, then the odd Hall lift acts trivially on the chief factor P/S:
[P,Ñ] ≤ S.