English
The forgetful functor from CommSemiRingCat to SemiRingCat reflects isomorphisms; i.e., if a morphism becomes an isomorphism after forgetting extra structure, then the original morphism was already an isomorphism in CommSemiRingCat.
Русский
Забывающий функтор от CommSemiRingCat к SemiRingCat отражает изоморфизмы: если морфизм становится изоморфизмом после забывания, то исходный морфизм уже является изоморфизмом в CommSemiRingCat.
LaTeX
$$$\forall f:\, X \to Y,\ (\text{forget}(f)\text{ isIso in SemiRingCat}) \Rightarrow f\text{ isIso in CommSemiRingCat}$$$
Lean4
instance forgetReflectIsos : (forget CommSemiRingCat).ReflectsIsomorphisms where
reflects {X Y} f
_ := by
let i := asIso ((forget CommSemiRingCat).map f)
let ff : X →+* Y := f.hom
let e : X ≃+* Y := { ff, i.toEquiv with }
exact e.toCommSemiRingCatIso.isIso_hom
