toAlgEquiv — Mathlib

English

From an isomorphism i: X ≅ Y in AlgCat R, produce an AlgEquiv R X.carrier Y.carrier.

Русский

Из изоморфизма i: X ≅ Y в AlgCat R получаем AlgEquiv R X.carrier Y.carrier.

LaTeX

$$i : X ≅ Y → X.carrier ≃ₐ[R] Y.carrier$$

Lean4

/-- Build a `AlgEquiv` from an isomorphism in the category `AlgCat R`. -/
@[simps]
def toAlgEquiv {X Y : AlgCat R} (i : X ≅ Y) : X ≃ₐ[R] Y :=
  { i.hom.hom with
    toFun := i.hom
    invFun := i.inv
    left_inv := fun x ↦ by simp
    right_inv := fun x ↦ by simp }

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