integralClosure_map_algEquiv — Mathlib

English

Let f be an algebra isomorphism between rings A and S over R. The integral closure of A maps isomorphically to the integral closure of S under f.

Русский

Пусть f — алгебраическое изоморфизм между кольцами A и S над R. Интегральное замыкание A отображается изоморфно в интегральное замыкание S через f.

LaTeX

$$$(integralClosure R A).map (f : A \toₐ[R] S) = integralClosure R S$$$

Lean4

/-- Mapping an integral closure along an `AlgEquiv` gives the integral closure. -/
theorem integralClosure_map_algEquiv [Algebra R S] (f : A ≃ₐ[R] S) :
    (integralClosure R A).map (f : A →ₐ[R] S) = integralClosure R S :=
  by
  ext y
  rw [Subalgebra.mem_map]
  constructor
  · rintro ⟨x, hx, rfl⟩
    exact hx.map f
  · intro hy
    use f.symm y, hy.map (f.symm : S →ₐ[R] A)
    simp

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