commSemiRingCatIsoToRingEquiv — Mathlib

English

For any isomorphism e in the category CommSemiRingCat, there is a RingEquiv between the underlying rings of the two objects.

Русский

Для любого изоморфизма e в категории CommSemiRingCat существует RingEquiv между соответствующими базовыми кольцами объектов.

LaTeX

$$$\forall R,S:\text{CommSemiRingCat},\; e:R\cong S \Rightarrow R.carrier \cong_{\mathsf{Ring}} S.carrier$$

Lean4

/-- Build a `RingEquiv` from an isomorphism in the category `CommSemiRingCat`. -/
def commSemiRingCatIsoToRingEquiv {R S : CommSemiRingCat.{u}} (e : R ≅ S) : R ≃+* S :=
  RingEquiv.ofHomInv e.hom.hom e.inv.hom (by ext; simp) (by ext; simp)

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