English
If R → S is an integral extension and M is a submonoid, the induced map between localizations is integral.
Русский
Если R → S интегрально, то локализация R_M → S_M также интегральна.
LaTeX
$$$\text{IsIntegral}((map S_m (algebraMap R S) ...))$$$
Lean4
/-- If `R → S` is an integral extension, `M` is a submonoid of `R`,
`Rₘ` is the localization of `R` at `M`,
and `Sₘ` is the localization of `S` at the image of `M` under the extension map,
then the induced map `Rₘ → Sₘ` is also an integral extension -/
theorem isIntegral_localization [Algebra.IsIntegral R S] :
(map Sₘ (algebraMap R S) (show _ ≤ (Algebra.algebraMapSubmonoid S M).comap _ from M.le_comap_map) :
Rₘ →+* _).IsIntegral :=
by
intro x
obtain ⟨⟨s, ⟨u, hu⟩⟩, hx⟩ := surj (Algebra.algebraMapSubmonoid S M) x
obtain ⟨v, hv⟩ := hu
obtain ⟨v', hv'⟩ := isUnit_iff_exists_inv'.1 (map_units Rₘ ⟨v, hv.1⟩)
refine @IsIntegral.of_mul_unit Rₘ _ _ _ (localizationAlgebra M S) x (algebraMap S Sₘ u) v' ?_ ?_
· replace hv' := congr_arg (@algebraMap Rₘ Sₘ _ _ (localizationAlgebra M S)) hv'
rw [RingHom.map_mul, RingHom.map_one, localizationAlgebraMap_def, IsLocalization.map_eq] at hv'
exact hv.2 ▸ hv'
· obtain ⟨p, hp⟩ := Algebra.IsIntegral.isIntegral (R := R) s
exact hx.symm ▸ is_integral_localization_at_leadingCoeff p hp.2 (hp.1.symm ▸ M.one_mem)
