isoLimittoFiniteQuotientFunctor — Mathlib

English

There is a topological group isomorphism between P and the limit of its finite quotients, realized as an Iso in ProfiniteGrp.

Русский

Существует топологический изоморфизм между P и пределом ее конечных фактор-групп, реализованный как_iso в ProfiniteGrp.

LaTeX

$$$P \cong_{\mathrm{ProfiniteGrp}} \mathrm{limit}(P.toFiniteQuotientFunctor \cdot \mathrm{forget}_{\mathrm{FiniteGrp}\to \mathrm{ProfiniteGrp}})$$$

Lean4

/-- The isomorphism in the category of profinite group between a profinite group and
the projective limit of its quotients by open normal subgroups -/
noncomputable def isoLimittoFiniteQuotientFunctor (P : ProfiniteGrp.{u}) :
    P ≅ (limit (toFiniteQuotientFunctor P ⋙ forget₂ FiniteGrp ProfiniteGrp)) :=
  ContinuousMulEquiv.toProfiniteGrpIso (continuousMulEquivLimittoFiniteQuotientFunctor P)

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