English
Let P be a p-subgroup of a group G with normal H such that (|H|) and [G:H] are coprime. Then either P ≤ H or H and P are disjoint.
Русский
Пусть P — p-подгруппа G, и H — нормальная подгруппа так, что |H| и индекс [G:H] взаимно просты. Тогда либо P ⊆ H, либо H ∩ P = {e}.
LaTeX
$$$\text{If } P \text{ is a } p\text{-subgroup and } H \lhd G \text{ with } (|H|, [G:H])=1, \text{ then } P \le H \text{ or } H \cap P = \{e\}.}$$$
Lean4
theorem le_or_disjoint_of_coprime [hp : Fact p.Prime] {P : Subgroup G} (hP : IsPGroup p P) {H : Subgroup G} [H.Normal]
(h_cop : (Nat.card H).Coprime H.index) : P ≤ H ∨ Disjoint H P :=
by
by_cases h1 : Nat.card H = 0
· rw [h1, Nat.coprime_zero_left, Subgroup.index_eq_one] at h_cop
rw [h_cop]
exact Or.inl le_top
by_cases h2 : H.index = 0
· rw [h2, Nat.coprime_zero_right, Subgroup.card_eq_one] at h_cop
rw [h_cop]
exact Or.inr disjoint_bot_left
have : Finite G := by
apply Nat.finite_of_card_ne_zero
rw [← H.card_mul_index]
exact mul_ne_zero h1 h2
have h3 : (Nat.card H).Coprime (Nat.card P) ∨ H.index.Coprime (Nat.card P) :=
by
obtain ⟨k, hk⟩ := hP.exists_card_eq
refine hk ▸ Or.imp hp.out.coprime_pow_of_not_dvd hp.out.coprime_pow_of_not_dvd ?_
contrapose! h_cop
exact Nat.Prime.not_coprime_iff_dvd.mpr ⟨p, hp.out, h_cop⟩
refine h3.symm.imp (fun h4 ↦ ?_) (fun h4 ↦ ?_)
· rw [← Subgroup.relIndex_eq_one]
exact Nat.eq_one_of_dvd_coprimes h4 (H.relIndex_dvd_index_of_normal P) (Subgroup.relIndex_dvd_card H P)
· exact disjoint_iff.mpr (Subgroup.inf_eq_bot_of_coprime h4)
