English
The algebra isomorphism mapAlgEquiv restricts an algebra isomorphism e: K ≃+* L to an isomorphism between 𝓞K and 𝓞L, i.e. 𝓞K ≃𝒜[𝓞k] 𝓞L.
Русский
Алгебраическое эквивогентое отображение mapAlgEquiv ограничивает изоморфизм K ≃+* L до изоморфизма 𝓞K ≃𝒜[𝓞k] 𝓞L.
LaTeX
$$$\\mathrm{mapAlgEquiv}(e) : \\mathcal{O}_K \\simeq_{\\mathcal{O}_k} \\mathcal{O}_L$$$
Lean4
/-- The isomorphism of algebras `(𝓞 K) ≃ₐ[𝓞 k] (𝓞 L)` given by restricting
an isomorphism of algebras `e : K ≃ₐ[k] L` to `𝓞 K`. -/
def mapAlgEquiv {k K L E : Type*} [Field k] [Field K] [Field L] [Algebra k K] [Algebra k L] [EquivLike E K L]
[AlgEquivClass E k K L] (e : E) : (𝓞 K) ≃ₐ[𝓞 k] (𝓞 L) :=
AlgEquiv.ofAlgHom (mapAlgHom e) (mapAlgHom (e : K ≃ₐ[k] L).symm) (AlgHom.ext fun x => ext (EquivLike.right_inv e x.1))
(AlgHom.ext fun x => ext (EquivLike.left_inv e x.1))
