algEquivIsoAlgebraIso — Mathlib

English

Algebra equivalences between algebras are the same as isomorphisms in AlgCat: there is an isomorphism of the two ways to view isomorphisms.

Русский

Алгебраические эквиваленты между алгебрами эквивалентны изоморфизмам в AlgCat: эквивалентности между двумя представлениями изоморфизмов совпадают.

LaTeX

$${R} AlgEquiv R X Y ≅ AlgCat.of R X ≅ AlgCat.of R Y$$

Lean4

/-- Algebra equivalences between `Algebra`s are the same as (isomorphic to) isomorphisms in
`AlgCat`. -/
@[simps]
def algEquivIsoAlgebraIso {X Y : Type u} [Ring X] [Ring Y] [Algebra R X] [Algebra R Y] :
    (X ≃ₐ[R] Y) ≅ AlgCat.of R X ≅ AlgCat.of R Y
    where
  hom e := e.toAlgebraIso
  inv i := i.toAlgEquiv

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