toLimit_injective — Mathlib

English

There is an isomorphism in ProfiniteGrp between a profinite group P and its limit object given by toLimit, i.e., P ≅ toLimit P.

Русский

Существует изоморфизм в ProfiniteGrp между P и its пределом via toLimit: P ≅ toLimit P.

LaTeX

$$$P \cong_{\mathrm{ProfiniteGrp}} \mathrm{toLimit}(P)$$$

Lean4

theorem toLimit_injective (P : ProfiniteGrp.{u}) : Function.Injective (toLimit P) :=
  by
  change Function.Injective (toLimit P).hom.toMonoidHom
  rw [← MonoidHom.ker_eq_bot_iff, Subgroup.eq_bot_iff_forall]
  intro x h
  by_contra xne1
  rcases
    exist_openNormalSubgroup_sub_open_nhds_of_one (isOpen_compl_singleton)
      (Set.mem_compl_singleton_iff.mpr fun a => xne1 a.symm) with
    ⟨H, hH⟩
  exact hH ((QuotientGroup.eq_one_iff x).mp (congrFun (Subtype.val_inj.mpr h) H)) rfl

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