forgetReflectsIsos — Mathlib

English

The forgetful functor from Semigrp to Type reflects isomorphisms: if the underlying function is bijective, then the morphism is an isomorphism in Semigrp.

Русский

Функтор забывания из Semigrp в Type отражает изоморфизмы: если соответствующая функция биективна, то морфизм в Semigrp — изоморфизм.

LaTeX

$$$(\\text{forget Semigrp}).ReflectsIsomorphisms$$$

Lean4

@[to_additive]
instance forgetReflectsIsos : (forget Semigrp.{u}).ReflectsIsomorphisms where
  reflects {X Y} f
    _ := by
    let i := asIso ((forget Semigrp).map f)
    let e : X ≃* Y := { f.hom, i.toEquiv with }
    exact e.toSemigrpIso.isIso_hom

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