English
The map toLimit_fun: P → limit(...) is continuous with respect to the induced topology.
Русский
Функтор toLimit_fun: P → limit(...) непрерывен по индукцированному топологическому пространству.
LaTeX
$$$\mathrm{Continuous}(\mathrm{toLimit\_fun}\;P)$$$
Lean4
theorem toLimit_fun_continuous (P : ProfiniteGrp.{u}) : Continuous (toLimit_fun P) :=
by
apply continuous_induced_rng.mpr (continuous_pi _)
intro H
dsimp only [Functor.comp_obj, CompHausLike.coe_of, Functor.comp_map, CompHausLike.toCompHausLike_map,
CompHausLike.compHausLikeToTop_map, Set.mem_setOf_eq, toLimit_fun, MonoidHom.coe_mk, OneHom.coe_mk,
Function.comp_apply]
apply Continuous.mk
intro s _
rw [← (Set.biUnion_preimage_singleton QuotientGroup.mk s)]
refine isOpen_iUnion (fun i ↦ isOpen_iUnion (fun _ ↦ ?_))
convert IsOpen.leftCoset H.toOpenSubgroup.isOpen' (Quotient.out i)
ext x
simp only [Set.mem_preimage, Set.mem_singleton_iff]
nth_rw 1 [← QuotientGroup.out_eq' i, eq_comm, QuotientGroup.eq]
exact Iff.symm (Set.mem_smul_set_iff_inv_smul_mem)
