English
The forgetful functor from RingCat to Type reflects isomorphisms: if the underlying function is an isomorphism, then the original ring homomorphism is an isomorphism in RingCat.
Русский
Забывающий функтор из RingCat в Type отражает изоморфизмы: если тождественная функция является изоморфизмом, то исходный кольцевой гомоморфизм является изоморфизмом в RingCat.
LaTeX
$$$\text{forget₂}.\Text{ReflectsIsomorphisms}$, i.e., if $f$ is iso after forgetful functor, then $f$ is iso in RingCat.$$
Lean4
instance forgetReflectIsos : (forget RingCat).ReflectsIsomorphisms where
reflects {X Y} f
_ := by
let i := asIso ((forget RingCat).map f)
let ff : X →+* Y := f.hom
let e : X ≃+* Y := { ff, i.toEquiv with }
exact e.toRingCatIso.isIso_hom
