monCatIsoToMulEquiv — Mathlib

English

From an isomorphism i: X ≅ Y in MonCat between MonCat objects, construct a MulEquiv X ≃* Y between their carriers.

Русский

Изоморфизм i: X ≅ Y в MonCat даёт MulEquiv между каррирами X и Y.

LaTeX

$$$\text{Given } i: X \cong Y,\; X \equiv_* Y.$$$

Lean4

/-- Build a `MulEquiv` from an isomorphism in the category `MonCat`. -/
@[to_additive addMonCatIsoToAddEquiv /-- Build an `AddEquiv` from an isomorphism in the category
    `AddMonCat`. -/
    ]
def monCatIsoToMulEquiv {X Y : MonCat} (i : X ≅ Y) : X ≃* Y :=
  MonoidHom.toMulEquiv i.hom.hom i.inv.hom (by ext; simp) (by ext; simp)

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