Class-two algebra for the Section 7 fourth-power step

Once R = Phi(K) centralizes K, the commutators of elements of K are central inside K. Together with the fact that squares of K lie in R, this gives the pointwise exponent-two statement for commutators. These are local algebraic ingredients for the manuscript's fourth-power map k |-> k^4.

theorem Q2Presentation.Induction.commutator_square_eq_one_of_square_central_and_commutator_central {G : Type u_1} [Group G] (a b : G) (hsq : a ^ 2 * b = b * a ^ 2) (hca : ⁅a, b⁆ * a = a * ⁅a, b⁆) : ⁅a, b⁆ ^ 2 = 1

A group-theoretic calculation used in the class-two part of the fourth-power step.

theorem Q2Presentation.Induction.kernel_commutator_square_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (a b : p.fst.Y) (ha : a ∈ K.Ksub) (hb : b ∈ K.Ksub) : ⁅a, b⁆ ^ 2 = 1

Commutators of elements of the minimal kernel have square one.