English
If commuting range homomorphisms ϕ_i from finite groups H_i into G have pairwise coprime orders, then the family {range(ϕ_i)} is independent (iSupIndep).
Русский
Если образы образов ϕ_i образованы из конечных групп H_i в G и пары порядков попарно взаимно просты, то семейство образов является независимым (iSupIndep).
LaTeX
$$$ iSupIndep (i \\mapsto (\\varphi_i).range) $ under pairwise coprime orders and commuting ranges.$$
Lean4
@[to_additive]
theorem noncommPiCoprod_range [Fintype ι]
{hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)} :
(noncommPiCoprod ϕ hcomm).range = ⨆ i : ι, (ϕ i).range :=
by
letI := Classical.decEq ι
apply le_antisymm
· rintro x ⟨f, rfl⟩
refine Subgroup.noncommProd_mem _ (fun _ _ _ _ h => hcomm h _ _) ?_
intro i _hi
apply Subgroup.mem_sSup_of_mem
· use i
simp
· refine iSup_le ?_
rintro i x ⟨y, rfl⟩
exact ⟨Pi.mulSingle i y, noncommPiCoprod_mulSingle _ _ _⟩
