toAlgebraIso — Mathlib

English

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

Русский

Из изоморфизма i: X ≅ Y в AlgCat R строим AlgEquiv R X.carrier Y.carrier.

LaTeX

$${i}: X ≅ Y → X ≃ₐ[R] Y$$

Lean4

/-- Build an isomorphism in the category `AlgCat R` from a `AlgEquiv` between `Algebra`s. -/
@[simps]
def toAlgebraIso {g₁ : Ring X₁} {g₂ : Ring X₂} {m₁ : Algebra R X₁} {m₂ : Algebra R X₂} (e : X₁ ≃ₐ[R] X₂) :
    AlgCat.of R X₁ ≅ AlgCat.of R X₂ where
  hom := AlgCat.ofHom (e : X₁ →ₐ[R] X₂)
  inv := AlgCat.ofHom (e.symm : X₂ →ₐ[R] X₁)

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