isoEquivAlgEquiv — Mathlib

English

Algebra equivalences between algebras correspond exactly to isomorphisms in CommAlgCat R.

Русский

Алгебраические эквивалентности между алгебрами эквивалентны изоморфизмам в CommAlgCat R.

LaTeX

$$$(\mathrm{Iso} (\mathrm{CommAlgCat} \; R)) \simeq (\mathrm{AlgEquiv} R X Y)$$$

Lean4

/-- Algebra equivalences between `Algebra`s are the same as isomorphisms in `CommAlgCat`. -/
@[simps]
def isoEquivAlgEquiv : (of R X ≅ of R Y) ≃ (X ≃ₐ[R] Y)
    where
  toFun := algEquivOfIso
  invFun := isoMk

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