English
If a family of subgroups H_i of G has pairwise commuting elements and pairwise coprime orders, then iSupIndep H holds.
Русский
Если множество подгрупп H_i группы G состоит из взаимно коммутирующих элементов и попарно взаимно простых порядков, то iSupIndep H выполняется.
LaTeX
$$$\\text{independent\_of\_coprime\_order}(hcomm, hcoprime): iSupIndep H$.$$
Lean4
@[to_additive]
theorem independent_range_of_coprime_order
(hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)) [Finite ι] [∀ i, Fintype (H i)]
(hcoprime : Pairwise fun i j => Nat.Coprime (Fintype.card (H i)) (Fintype.card (H j))) :
iSupIndep fun i => (ϕ i).range := by
cases nonempty_fintype ι
letI := Classical.decEq ι
rintro i
rw [disjoint_iff_inf_le]
rintro f ⟨hxi, hxp⟩
dsimp at hxi hxp
rw [iSup_subtype', ← noncommPiCoprod_range] at hxp
rotate_left
· intro _ _ hj
apply hcomm
exact hj ∘ Subtype.ext
obtain ⟨g, hgf⟩ := hxp
obtain ⟨g', hg'f⟩ := hxi
have hxi : orderOf f ∣ Fintype.card (H i) := by
rw [← hg'f]
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card
have hxp : orderOf f ∣ ∏ j : { j // j ≠ i }, Fintype.card (H j) :=
by
rw [← hgf, ← Fintype.card_pi]
exact (orderOf_map_dvd _ _).trans orderOf_dvd_card
change f = 1
rw [← pow_one f, ← orderOf_dvd_iff_pow_eq_one]
obtain ⟨c, hc⟩ := Nat.dvd_gcd hxp hxi
use c
rw [← hc]
symm
rw [← Nat.coprime_iff_gcd_eq_one, Nat.coprime_fintype_prod_left_iff, Subtype.forall]
intro j h
exact hcoprime h
