forget_reflects_isos — Mathlib

English

The forgetful functor from CommGrpCat to Type reflects isomorphisms; in particular, a bijective homomorphism of commutative groups is a group isomorphism.

Русский

Забывающий функтор от CommGrpCat к Type отражает изomорфизмы; биективный гомоморфизм коммутативных групп является изоморфизмом.

LaTeX

$$For all G,H groups and f:G→H Bijective(f) ⇒ f is an isomorphism$$

Lean4

@[to_additive]
instance forget_reflects_isos : (forget CommGrpCat.{u}).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget CommGrpCat).map f)
    let e : X ≃* Y := { i.toEquiv with map_mul' := map_mul _ }
    exact e.toCommGrpIso.isIso_hom

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