English
Let f be a morphism in the category of commutative rings. If the underlying map obtained by forgetting the ring structure is an isomorphism in the category of rings, then f is an isomorphism in CommRingCat.
Русский
Пусть f - мороморфизм в категории коммутативных колец. Если забывающий функтор переводит f в изоморфизм в категории колец, то f является изоморфизмом в CommRingCat.
LaTeX
$$$\forall X,Y\; (f:X\to Y),\ IsIso\big((\mathrm{forget\_CommRingCat}).map\,f\big)\Rightarrow IsIso\,f$$$
Lean4
instance forgetReflectIsos : (forget CommRingCat).ReflectsIsomorphisms where
reflects {X Y} f
_ := by
let i := asIso ((forget CommRingCat).map f)
let ff : X →+* Y := f.hom
let e : X ≃+* Y := { ff, i.toEquiv with }
exact e.toCommRingCatIso.isIso_hom
