English
Let P be a cyclic p-subgroup and K ≤ N_G(P) with |P| coprime to |K|. Then [K,P] is either trivial or equals P.
Русский
Пусть P — циклическая подгруппа p, и K ≤ N_G(P) с тем, что |P| и |K| взаимно просты. Тогда [K,P] либо тривиален, либо равен P.
LaTeX
$$$[K,P] = \\{e\\} \\quad\\lor\\quad [K,P] = P$$$
Lean4
/-- If a cyclic `p`-subgroup `P` acts by conjugation on a subgroup `K` of coprime order, then
either `⁅K, P⁆ = ⊥` or `⁅K, P⁆ = P`. -/
theorem commutator_eq_bot_or_commutator_eq_self {P K : Subgroup G} [IsCyclic P] (hP : IsPGroup p P)
(hKP : K ≤ P.normalizer) (hPK : (Nat.card P).Coprime (Nat.card K)) : ⁅K, P⁆ = ⊥ ∨ ⁅K, P⁆ = P :=
by
let _ := MulDistribMulAction.compHom P (P.normalizerMonoidHom.comp (Subgroup.inclusion hKP))
refine (smul_mul_inv_trivial_or_surjective hP hPK).imp (fun h ↦ ?_) fun h ↦ ?_
· rw [eq_bot_iff, Subgroup.commutator_le]
exact fun k hk g hg ↦ Subtype.ext_iff.mp (h ⟨g, hg⟩ ⟨k, hk⟩)
· rw [le_antisymm_iff, Subgroup.commutator_le]
refine ⟨fun k hk g hg ↦ P.mul_mem ((hKP hk g).mp hg) (P.inv_mem hg), fun g hg ↦ ?_⟩
obtain ⟨k, q, hkq⟩ := h ⟨g, hg⟩
rw [← Subtype.coe_mk g hg, ← hkq]
exact Subgroup.commutator_mem_commutator k.2 q.2
