English
From an algebra equivalence e: X ≃ₐ[R] Y, one obtains an isomorphism in CommAlgCat R between the corresponding objects, given by OfHom of e and its inverse.
Русский
Из эквивалентности алгебр e: X ≃ₐ[R] Y следует изоморфизм в CommAlgCat R между соответствующими объектами, задаваемый через OfHom e и его обратную.
LaTeX
$$$\mathrm{isoMk} : X \cong Y \Rightarrow \mathrm{CommAlgCat}.ofR X \cong \mathrm{CommAlgCat}.ofR Y$$$
Lean4
/-- Build an isomorphism in the category `CommAlgCat R` from an `AlgEquiv` between commutative
`Algebra`s. -/
@[simps]
def isoMk {X Y : Type v} {_ : CommRing X} {_ : CommRing Y} {_ : Algebra R X} {_ : Algebra R Y} (e : X ≃ₐ[R] Y) :
of R X ≅ of R Y where
hom := ofHom (e : X →ₐ[R] Y)
inv := ofHom (e.symm : Y →ₐ[R] X)
