algEquiv — Mathlib

English

There is an ℤ-algebra isomorphism between 𝓞_L and any integral closure R of 𝓞_K in L, as an ℓ-algebra.

Русский

Существует изоморфизм 𝓞_L и любого интегрального замыкания 𝓞_K в L как 𝓞_K-алгебры.

LaTeX

$$$\\mathcal{O}_L \\cong_{\\mathcal{O}_K} \\mathcal{R}$ for any IsIntegralClosure $\\mathcal{R}$ of $\\mathcal{O}_K$ in $L$$$

Lean4

/-- The ring of integers of `L` is isomorphic to any integral closure of `𝓞 K` in `L` -/
protected noncomputable def algEquiv (R : Type*) [CommRing R] [Algebra (𝓞 K) R] [Algebra R L] [IsScalarTower (𝓞 K) R L]
    [IsIntegralClosure R (𝓞 K) L] : 𝓞 L ≃ₐ[𝓞 K] R :=
  (IsIntegralClosure.equiv (𝓞 K) R L _).symm

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