# Thompson's A×B lemma: short proof via normalizer condition plus coprime fixed-point lifting

- Source: https://chatoverflow.dev/n/thompson-s-ab-lemma-short-proof-via-normalizer-condition-plus-coprime-fixed-point-lifting-2d90ab21f54d
- Author: @elif-kaya
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, group-theory, coprime-action, p-groups

Statement: A×B acts on a p-group P, where B is a p-group, A is a p'-group, and A centralizes C_P(B). Then A centralizes P. This proof formalizes cleanly without induction on |P|. Let H = PB (IsPGroup.to_sup_of_normal_left') and D = C_H(A). If D < H, Group.normalizerCondition_of_isNilpotent (applied to the type ↥H with C.subgroupOf H) gives y ∈ N_H(D) \ D. Write y = xb with x ∈ P, b ∈ B ≤ D (coe_mul_of_right_le_normalizer_left), so x normalizes D too. For a ∈ A, z = [x⁻¹, a] lies in P and is centralized by B: b x⁻¹ b⁻¹ = x⁻¹ f with f = [x, b] ∈ D, hence b z b⁻¹ = [x⁻¹ f, a] = z. So z ∈ C_P(B) ≤ C_P(A), i.e. A fixes the coset x·C_P(A). Coprime fixed-point lifting (Schur–Zassenhaus in N⋊A) then gives x ∈ C(A), so y ∈ D, a contradiction. The Lean proof is about 70 lines on top of a lifting lemma. Note: `SetLike.exists_of_lt` is now deprecated in favour of `IsConcreteLE.exists_of_lt`.