English
Finite type/presentation can be checked by a standard spanning source: if the source is FP and its localizations cover the target, the target is FP.
Русский
Финитый тип/представление можно проверить по стандартному охвату источника: если исходник FP и локализации покрывают целевой объект, целевой объект FP.
LaTeX
$$$\text{OfSpanTopSource }\operatorname{FiniteType}$$$
Lean4
/-- Finite-type can be checked on a standard covering of the target. -/
theorem of_span_eq_top_target (s : Set S) (hs : Ideal.span (s : Set S) = ⊤)
(h : ∀ x ∈ s, Algebra.FiniteType R (Localization.Away x)) : Algebra.FiniteType R S :=
by
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
replace h (i : s) : Algebra.FiniteType R (Localization.Away i.val) := h i (h₁ i.property)
classical
-- Suppose `s : Finset S` spans `S`, and each `Sᵣ` is finitely generated as an `R`-algebra.
-- Say `t r : Finset Sᵣ` generates `Sᵣ`. By assumption, we may find `lᵢ` such that
-- `∑ lᵢ * sᵢ = 1`. I claim that all `s` and `l` and the numerators of `t` and generates `S`.
replace h := fun r => (h r).1
choose t ht using h
obtain ⟨l, hl⟩ :=
(Finsupp.mem_span_iff_linearCombination S (s : Set S) 1).mp
(show (1 : S) ∈ Ideal.span (s : Set S) by rw [hs]; trivial)
let sf := fun x : s => IsLocalization.finsetIntegerMultiple (Submonoid.powers (x : S)) (t x)
use s.attach.biUnion sf ∪ s ∪ l.support.image l
rw [_root_.eq_top_iff]
-- We need to show that every `x` falls in the subalgebra generated by those elements.
-- Since all `s` and `l` are in the subalgebra, it suffices to check that `sᵢ ^ nᵢ • x` falls in
-- the algebra for each `sᵢ` and some `nᵢ`.
rintro x -
apply Subalgebra.mem_of_span_eq_top_of_smul_pow_mem _ (s : Set S) l hl _ _ x _
· intro x hx
apply Algebra.subset_adjoin
rw [Finset.coe_union, Finset.coe_union]
exact Or.inl (Or.inr hx)
· intro i
by_cases h : l i = 0; · rw [h]; exact zero_mem _
apply Algebra.subset_adjoin
rw [Finset.coe_union, Finset.coe_image]
exact Or.inr (Set.mem_image_of_mem _ (Finsupp.mem_support_iff.mpr h))
· intro r
rw [Finset.coe_union, Finset.coe_union, Finset.coe_biUnion]
-- Since all `sᵢ` and numerators of `t r` are in the algebra, it suffices to show that the
-- image of `x` in `Sᵣ` falls in the `R`-adjoin of `t r`, which is of course true.
-- Porting note: The following `obtain` fails because Lean wants to know right away what the
-- placeholders are, so we need to provide a little more guidance
-- obtain ⟨⟨_, n₂, rfl⟩, hn₂⟩ := IsLocalization.exists_smul_mem_of_mem_adjoin
-- (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) _ _ _
rw [show
∀ A : Set S,
(∃ n, (r : S) ^ n • x ∈ Algebra.adjoin R A) ↔
(∃ m : (Submonoid.powers (r : S)), (m : S) • x ∈ Algebra.adjoin R A)
by { exact fun _ => by simp [Submonoid.mem_powers_iff]
}]
refine IsLocalization.exists_smul_mem_of_mem_adjoin (Submonoid.powers (r : S)) x (t r) (Algebra.adjoin R _) ?_ ?_ ?_
· intro x hx
apply Algebra.subset_adjoin
exact Or.inl (Or.inl ⟨_, ⟨r, rfl⟩, _, ⟨s.mem_attach r, rfl⟩, hx⟩)
· rw [Submonoid.powers_eq_closure, Submonoid.closure_le, Set.singleton_subset_iff]
apply Algebra.subset_adjoin
exact Or.inl (Or.inr r.2)
· rw [ht]; trivial
