English
Finite-type can be checked on a standard covering of the source, via expressions of elements and their powers in the submonoid of R.
Русский
Финитость типа может быть проверена на стандартном покрытии источника через элементы и их степени в подмоноиде R.
LaTeX
$$$\text{FiniteType.of_span_eq_top_source}$$$
Lean4
theorem of_span_eq_top_source (s : Set R) (hs : Ideal.span (s : Set R) = ⊤)
(h : ∀ i ∈ s, Algebra.FiniteType (Localization.Away i) (Localization.Away i ⊗[R] S)) : Algebra.FiniteType R S :=
by
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
replace h (i : s) := h i.val (h₁ i.property)
classical
letI := fun r : s => (Localization.awayMap (algebraMap R S) r).toAlgebra
set f := algebraMap R S
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
convert (Algebra.adjoin_attach_biUnion (R := R) sf).trans _
rw [eq_top_iff]
rintro x -
apply (⨆ x : s, Algebra.adjoin R (sf x : Set S)).toSubmodule.mem_of_span_eq_top_of_smul_pow_mem _ hs _ _
intro r
obtain ⟨⟨_, n₁, rfl⟩, hn₁⟩ :=
multiple_mem_adjoin_of_mem_localization_adjoin (Submonoid.powers (r : R)) (Localization.Away (r : R))
(s₁ r : Set (Localization.Away r.val ⊗[R] S)) (algebraMap S _ x) (by rw [s₂ r]; trivial)
rw [Submonoid.smul_def, Algebra.smul_def, IsScalarTower.algebraMap_apply R S, ← map_mul] at hn₁
obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ :=
IsLocalization.lift_mem_adjoin_finsetIntegerMultiple (Submonoid.powers (r : 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 => Algebra.adjoin R (sf x : Set S)) r hn₂
