instReflectsIsomorphismsForget — Mathlib

English

The forgetful functor forget from ProfiniteGrp to GrpCat reflects isomorphisms; i.e., if a morphism is an isomorphism of underlying groups, it is an isomorphism in ProfiniteGrp.

Русский

Функтор забывания от ProfiniteGrp к GrpCat отражает изоморфизм; если гомоморфизм является изоморфизмом в базовой группе, то он таковым является и внутри ProfiniteGrp.

LaTeX

$$$(\mathrm{forget}\ ProfiniteGrp) \text{ reflects isomorphisms}$$$

Lean4

instance : (forget ProfiniteGrp.{u}).ReflectsIsomorphisms :=
  CategoryTheory.reflectsIsomorphisms_comp (forget₂ ProfiniteGrp Profinite) (forget Profinite)

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