toLimit_surjective — Mathlib

English

There is a topological group isomorphism between a profinite group P and the limit of its finite quotients, implemented via a continuousMulEquivLimittoFiniteQuotientFunctor.

Русский

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

LaTeX

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

Lean4

theorem toLimit_surjective (P : ProfiniteGrp.{u}) : Function.Surjective (toLimit P) :=
  by
  have : IsClosed (Set.range P.toLimit) := P.toLimit.hom.continuous_toFun.isClosedMap.isClosed_range
  rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr this, Dense.closure_eq (denseRange_toLimit P)]

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