mapIntegralClosure — Mathlib

English

An algebra isomorphism f: A ≃ₐ[R] S yields an isomorphism between integral closures.

Русский

Алгебраическое изоморфизм f: A ≃ₐ[R] S задаёт изоморфизм между интегральными замыканиями.

LaTeX

$$$\text{mapIntegralClosure} : \intClosure R A \simeq_{}^R \intClosure R S$$$

Lean4

/-- An `AlgEquiv` between two rings restrict to an `AlgEquiv` between the integral closures inside
them. -/
def mapIntegralClosure [Algebra R S] (f : A ≃ₐ[R] S) : integralClosure R A ≃ₐ[R] integralClosure R S :=
  AlgEquiv.ofAlgHom (f : A →ₐ[R] S).mapIntegralClosure (f.symm : S →ₐ[R] A).mapIntegralClosure
    (AlgHom.ext fun _ ↦ Subtype.ext (f.right_inv _)) (AlgHom.ext fun _ ↦ Subtype.ext (f.left_inv _))

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