continuousMulEquivLimittoFiniteQuotientFunctor

English

There is a topological group isomorphism between P and the limit of its quotients, provided by continuousMulEquivLimittoFiniteQuotientFunctor.

Русский

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

LaTeX

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

Lean4

/-- The topological group isomorphism between a profinite group and the projective limit of
its quotients by open normal subgroups -/
noncomputable def continuousMulEquivLimittoFiniteQuotientFunctor (P : ProfiniteGrp.{u}) :
    P ≃ₜ* (limit (toFiniteQuotientFunctor P ⋙ forget₂ FiniteGrp ProfiniteGrp)) :=
  {
    (Continuous.homeoOfEquivCompactToT2 (f := Equiv.ofBijective _ ⟨toLimit_injective P, toLimit_surjective P⟩)
      P.toLimit.hom.continuous_toFun) with
    map_mul' := (toLimit P).hom.map_mul' }

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