Integral closures of localizations

If Rₘ is a localization of R at a submonoid M, and S, Sₘ are integral closures of R, Rₘ in the same commutative ring L, then Sₘ is the localization of S at the image of M.

Mathlib's IsLocalization.integralClosure states this for the literal subalgebra integralClosure R L; the version here applies to arbitrary types satisfying IsIntegralClosure.

Main results

• TauCeti.isLocalization_algebraMapSubmonoid_of_isIntegralClosure: an integral closure of a localization is the corresponding localization of an integral closure.

theorem TauCeti.isLocalization_algebraMapSubmonoid_of_isIntegralClosure {R : Type uR} {Rₘ : Type uRm} {S : Type uS} {Sₘ : Type uSm} {L : Type uL} [CommRing R] [CommRing Rₘ] [CommSemiring S] [CommSemiring Sₘ] [CommRing L] {M : Submonoid R} [Algebra R Rₘ] [Algebra R S] [Algebra R L] [Algebra Rₘ L] [Algebra S Sₘ] [Algebra S L] [Algebra Sₘ L] [IsScalarTower R Rₘ L] [IsScalarTower R S L] [IsScalarTower S Sₘ L] [IsIntegralClosure S R L] [IsIntegralClosure Sₘ Rₘ L] [IsLocalization M Rₘ] : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ

If Rₘ is a localization of R, then an integral closure of Rₘ in a commutative ring L is the corresponding localization of an integral closure of R in L. The maps R → Rₘ → L, R → S → L, and S → Sₘ → L must agree with the direct maps to L.

Unlike IsLocalization.integralClosure, this applies when the original integral closure is an arbitrary type satisfying IsIntegralClosure, rather than the literal integralClosure R L.