semiRingCatIsoToRingEquiv — Mathlib

English

If R and S are semirings and e: R ≅ S is an isomorphism in the category of semirings, then R.carrier and S.carrier are isomorphic as rings; more precisely there is a RingEquiv between the underlying rings determined by e.

Русский

Пусть R и S — полусерии, и e: R ≅ S — изоморфизм в категории полусерий; тогда подлежащие кольцам R.carrier и S.carrier изоморфны как кольца; существует кольцевое эквивалиентное отображение, полученное из e.

LaTeX

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

Lean4

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

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