English
If an R-algebra S is integral after localization at a spanning set of R (i.e., for each localization R_t, S_t is integral over R_t), then S is integral over R.
Русский
Если базовые локализации S_t над R_t делают S_t интегралом над R_t для некоторого набора t, которым порождает единичную идеал, то S является интегралом над R.
LaTeX
$$$\exists \text{set }\,{r_i}\subset R\text{ spanning }R\text{ with }\forall i, IsIntegral( Localization.map R R_{r_i} ),$ что эквивалентно $IsIntegral( algebraMap R S)$.$$
Lean4
/-- `S` is an integral `R`-algebra if there exists a set `{ r }` that
spans `R` such that each `Sᵣ` is an integral `Rᵣ`-algebra. -/
theorem isIntegral_ofLocalizationSpan : OfLocalizationSpan (RingHom.IsIntegral ·) :=
by
introv R hs H r
letI := f.toAlgebra
change r ∈ (integralClosure R S).toSubmodule
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ s hs
rintro ⟨t, ht⟩
letI := (Localization.awayMap f t).toAlgebra
haveI : IsScalarTower R (Localization.Away t) (Localization.Away (f t)) :=
.of_algebraMap_eq' (IsLocalization.lift_comp _).symm
have : _root_.IsIntegral (Localization.Away t) (algebraMap S (Localization.Away (f t)) r) :=
H ⟨t, ht⟩ (algebraMap _ _ r)
obtain ⟨⟨_, n, rfl⟩, p, hp, hp'⟩ := this.exists_multiple_integral_of_isLocalization (.powers t)
rw [IsScalarTower.algebraMap_eq R S, Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ←
map_mul, ← hom_eval₂, IsLocalization.map_eq_zero_iff (.powers (f t))] at hp'
obtain ⟨⟨x, m, (rfl : algebraMap R S t ^ m = x)⟩, e⟩ := hp'
by_cases hp' : 1 ≤ p.natDegree; swap
· obtain rfl : p = 1 := eq_one_of_monic_natDegree_zero hp (by cutsat)
exact ⟨m, by simp [Algebra.smul_def, show algebraMap R S t ^ m = 0 by simpa using e]⟩
refine ⟨m + n, p.scaleRoots (t ^ m), (monic_scaleRoots_iff _).mpr hp, ?_⟩
have := p.scaleRoots_eval₂_mul (algebraMap R S) (t ^ n • r) (t ^ m)
simp only [pow_add, ← Algebra.smul_def, mul_smul, ← map_pow] at e this ⊢
rw [this, ← tsub_add_cancel_of_le hp', pow_succ, mul_smul, e, smul_zero]
