injective_noncommPiCoprod_of_iSupIndep

English

If the family {H_i} is iSupIndep (a strong independence condition), then the canonical homomorphism from the product of subgroups to G is injective.

Русский

Если семейство {H_i} удовлетворяет условию iSupIndep (сильная независимость), то канонический копродуктовый гомоморфизм инъективен.

LaTeX

$$$\ker(\text{noncommPiCoprod } hcomm) = \{1\}$ under hind$$

Lean4

@[to_additive]
theorem injective_noncommPiCoprod_of_iSupIndep
    {hcomm : Pairwise fun i j : ι => ∀ x y : G, x ∈ H i → y ∈ H j → Commute x y} (hind : iSupIndep H) :
    Function.Injective (noncommPiCoprod hcomm) :=
  by
  apply MonoidHom.injective_noncommPiCoprod_of_iSupIndep
  · simpa using hind
  · intro i
    exact Subtype.coe_injective

Похожие утверждения