English
The forgetful functor from ProfiniteGrp to Profinite (via forget₂ to Profinite) reflects isomorphisms; i.e., if a map becomes an isomorphism after forgetting, it was an isomorphism to begin with.
Русский
Функтор забывания через forget₂ между ProfiniteGrp и Profinite отражает изоморфизмы; если после забывания карта является изоморфизмом, то она была изоморфизмом изначально.
LaTeX
$$$\text{forget₂}\;\mathrm{ProfiniteGrp}\;\mathrm{Profinite}$ reflects isomorphisms$$
Lean4
instance : (forget₂ ProfiniteGrp Profinite).ReflectsIsomorphisms where
reflects {X Y} f
_ := by
let i := asIso ((forget₂ ProfiniteGrp Profinite).map f)
let e : X ≃ₜ* Y := { CompHausLike.homeoOfIso i with map_mul' := map_mul f.hom }
exact (ContinuousMulEquiv.toProfiniteGrpIso e).isIso_hom