English
Another formulation of finite-span localization result.
Русский
Еще одно формулирование результата о конечном спане локализации.
LaTeX
$$$\\operatorname{Finite}\\;\\operatorname{Localization}\\;\\operatorname{Span}$$$
Lean4
/-- `S` is a finite `R`-algebra if there exists a set `{ r }` that
spans `R` such that `Sᵣ` is a finite `Rᵣ`-algebra. -/
theorem finite_ofLocalizationSpan : RingHom.OfLocalizationSpan @RingHom.Finite := by
classical
rw [RingHom.ofLocalizationSpan_iff_finite]
introv R hs H
letI := f.toAlgebra
letI := fun r : s => (Localization.awayMap f r).toAlgebra
have : ∀ r : s, IsLocalization ((Submonoid.powers (r : R)).map (algebraMap R S)) (Localization.Away (f r)) := by
intro r; rw [Submonoid.map_powers]; exact Localization.isLocalization
haveI : ∀ r : s, IsScalarTower R (Localization.Away (r : R)) (Localization.Away (f r)) := fun r =>
IsScalarTower.of_algebraMap_eq' (IsLocalization.map_comp (Submonoid.powers (r : R)).le_comap_map).symm
constructor
replace H := fun r => (H r).1
choose s₁ s₂ using H
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (f x)) (s₁ x)
use s.attach.biUnion sf
rw [Submodule.span_attach_biUnion, eq_top_iff]
-- It suffices to show that `r ^ n • x ∈ span T` for each `r : s`, since `{ r ^ n }` spans `R`.
-- This then follows from the fact that each `x : R` is a linear combination of the generating set
-- of `Sᵣ`. By multiplying a sufficiently large power of `r`, we can cancel out the `r`s in the
-- denominators of both the generating set and the coefficients.
rintro x -
apply Submodule.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set R) hs _ _
intro r
obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
multiple_mem_span_of_mem_localization_span (Submonoid.powers (r : R)) (Localization.Away (r : R))
(s₁ r : Set (Localization.Away (f r))) (algebraMap S _ x) (by rw [s₂ r]; trivial)
dsimp only at hn₁
rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
IsLocalization.smul_mem_finsetIntegerMultiple_span (Submonoid.powers (r : R)) (Localization.Away (f r)) _ (s₁ r) hn₁
rw [Submonoid.smul_def, ← Algebra.smul_def, smul_smul, ← pow_add] at hn₂
simp_rw [Submonoid.map_powers] at hn₂
use n₂ + n₁
exact le_iSup (fun x : s => Submodule.span R (sf x : Set S)) r hn₂
