English
If f: R ≃+* S is a ring equivalence and R is integrally closed, then S is integrally closed.
Русский
Если f: R ≃+* S — кольцевое эквивалент, и R интегрально замкнуто, то S интегрально замкнуто.
LaTeX
$$$IsIntegrallyClosed R \Rightarrow IsIntegrallyClosed S$ under RingEquiv f.$$
Lean4
theorem of_equiv (f : R ≃+* S) [h : IsIntegrallyClosed R] : IsIntegrallyClosed S :=
by
let _ : Algebra S R := f.symm.toRingHom.toAlgebra
let f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv fun _ ↦ rfl
let g : FractionRing S ≃ₐ[S] FractionRing R := IsFractionRing.algEquivOfAlgEquiv f
refine (isIntegrallyClosed_iff (FractionRing S)).mpr (fun hx ↦ ?_)
rcases (isIntegrallyClosed_iff _).mp h ((isIntegral_algEquiv g).mpr hx).tower_top with ⟨z, hz⟩
exact
⟨f.symm z, (IsFractionRing.algEquivOfAlgEquiv_algebraMap f.symm z).symm.trans <| (AlgEquiv.symm_apply_eq g).mpr hz⟩
