English
If the iSupIndep of the ranges holds and each ϕ_i is injective, then the noncommPiCoprod map is injective.
Русский
Если выполняется независимость iSupIndep диапазонов и каждый ϕ_i инъективен, то noncommPiCoprod инъективен.
LaTeX
$$$\\text{injective}(\\text{noncommPiCoprod } ϕ) \\iff \\forall i, \\text{injective}(ϕ_i)$ (under iSupIndep and pairwise commuting).$$
Lean4
@[to_additive]
theorem injective_noncommPiCoprod_of_iSupIndep [Fintype ι]
{hcomm : Pairwise fun i j : ι => ∀ (x : H i) (y : H j), Commute (ϕ i x) (ϕ j y)}
(hind : iSupIndep fun i => (ϕ i).range) (hinj : ∀ i, Function.Injective (ϕ i)) :
Function.Injective (noncommPiCoprod ϕ hcomm) := by
classical
apply (MonoidHom.ker_eq_bot_iff _).mp
rw [eq_bot_iff]
intro f heq1
have : ∀ i, i ∈ Finset.univ → ϕ i (f i) = 1 :=
Subgroup.eq_one_of_noncommProd_eq_one_of_iSupIndep _ _ (fun _ _ _ _ h => hcomm h _ _) _ hind (by simp) heq1
ext i
apply hinj
simp [this i (Finset.mem_univ i)]
