English
Finite presentation of S over R can be checked by a local covering of the target S using a finite family of localizations.
Русский
Конечное презентование кольца S над R можно проверить по локальным локализациям целевого кольца S, используя конечное семейство локализаций.
LaTeX
$$$\forall S,\text{ покрывающий набор } s,\forall i\in s,\ Algebra.FinitePresentation(R,\operatorname{Localization.Away}(i))\Rightarrow \ Algebra.FinitePresentation(R,S)$$$
Lean4
/-- Finite-presentation 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 : ∀ i ∈ s, Algebra.FinitePresentation R (Localization.Away i)) : Algebra.FinitePresentation R S :=
by
obtain ⟨s, h₁, hs⟩ := (Ideal.span_eq_top_iff_finite s).mp hs
replace h (i : s) : Algebra.FinitePresentation R (Localization.Away i.val) := h i (h₁ i.property)
classical
/-
We already know that `S` is of finite type over `R`, so we have a surjection
`MvPolynomial (Fin n) R →ₐ[R] S`. To reason about the kernel, we want to check it on the stalks
of preimages of `s`. But the preimages do not necessarily span `MvPolynomial (Fin n) R`, so
we quotient out by an ideal and apply `finitePresentation_ofLocalizationSpanTarget_aux`.
-/
have hfintype : Algebra.FiniteType R S :=
by
apply Algebra.FiniteType.of_span_eq_top_target s hs
intro x hx
have := h ⟨x, hx⟩
infer_instance
obtain ⟨n, f, hf⟩ := Algebra.FiniteType.iff_quotient_mvPolynomial''.mp hfintype
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)
choose g' hg' using (fun g : s ↦ hf g)
choose h' hh' using (fun g : s ↦ hf (l g))
let I : Ideal (MvPolynomial (Fin n) R) := Ideal.span {∑ g : s, g' g * h' g - 1}
let A := MvPolynomial (Fin n) R ⧸ I
have hfI : ∀ a ∈ I, f a = 0 := by
intro p hp
simp only [Finset.univ_eq_attach, I, Ideal.mem_span_singleton] at hp
obtain ⟨q, rfl⟩ := hp
simp only [map_mul, map_sub, map_sum, map_one, hg', hh']
rw [Finsupp.linearCombination_apply_of_mem_supported (α := (s : Set S)) S (s := s.attach)] at hl
· rw [← hl]
simp only [Finset.coe_sort_coe, smul_eq_mul, mul_comm, sub_self, zero_mul]
· rintro a -
simp
let f' : A →ₐ[R] S := Ideal.Quotient.liftₐ I f hfI
have hf' : Function.Surjective f' := Ideal.Quotient.lift_surjective_of_surjective I hfI hf
let t : Finset A := Finset.image (fun g ↦ g' g) Finset.univ
have ht : Ideal.span (t : Set A) = ⊤ := by
rw [Ideal.eq_top_iff_one]
have : ∑ g : { x // x ∈ s }, g' g * h' g = (1 : A) :=
by
apply eq_of_sub_eq_zero
rw [← map_one (Ideal.Quotient.mk I), ← map_sub, Ideal.Quotient.eq_zero_iff_mem]
apply Ideal.subset_span
simp
simp_rw [← this, Finset.univ_eq_attach, map_sum, map_mul]
refine Ideal.sum_mem _ (fun g _ ↦ Ideal.mul_mem_right _ _ <| Ideal.subset_span ?_)
simp [t]
have : Algebra.FinitePresentation R A :=
by
apply Algebra.FinitePresentation.quotient
simp only [Finset.univ_eq_attach, I]
exact ⟨{∑ g ∈ s.attach, g' g * h' g - 1}, by simp⟩
have Ht (g : t) : Algebra.FinitePresentation R (Localization.Away (f' g)) :=
by
have : ∃ (a : S) (hb : a ∈ s), (Ideal.Quotient.mk I) (g' ⟨a, hb⟩) = g.val :=
by
obtain ⟨g, hg⟩ := g
convert hg
simp [A, t]
obtain ⟨r, hr, hrr⟩ := this
simp only [f']
rw [← hrr, Ideal.Quotient.liftₐ_apply, Ideal.Quotient.lift_mk]
simp_rw [RingHom.coe_coe]
rw [hg']
apply h
exact of_span_eq_top_target_aux f' hf' t ht Ht
