instReflectsIsomorphismsProfiniteForget₂

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

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