ringCatIsoToRingEquiv — Mathlib

English

From an isomorphism e: R ≅ S in RingCat (the category of rings), one obtains a RingEquiv between the underlying rings R.carrier and S.carrier.

Русский

Из изоморфизма e: R ≅ S в категории RingCat следует кольцевое эквивалентное отображение между базовыми кольцами R.carrier и S.carrier.

LaTeX

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

Lean4

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

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