English
If A is a finitely presented R-algebra and f: A → S is surjective, with a finite set t whose images generate the unit ideal in S, and for every g ∈ t the localization of A away from f(g) is finitely presented, then S is finitely presented over R.
Русский
Пусть A — конечно-презентованный R-алгебра, и существует сюръективный гомоморфизм f: A → S. Пусть t — конечный набор элементов A так, что образы f(t) порождают единичный идеал в S, и для каждого g ∈ t локализация A по f(g) является конечно-презентованной над R. Тогда S также конечно-презентована над R.
LaTeX
$$$\forall f:\ A \to_R S\ (\text{существует сюрьективный } f),\ t\subset A\text{ Finite},\ \operatorname{span}(t)=R,\ (\forall g\in t)\ Algebra.FinitePresentation\ R(\operatorname{Localization.Away}(f(g)))\ \Rightarrow\ Algebra.FinitePresentation\ R\ S$$$
Lean4
/-- If `S` is an `R`-algebra with a surjection from a finitely-presented `R`-algebra `A`, such that
localized at a spanning set `{ r }` of elements of `A`, `Sᵣ` is finitely-presented, then
`S` is finitely presented.
This is almost `finitePresentation_ofLocalizationSpanTarget`. The difference is,
that here the set `t` generates the unit ideal of `A`, while in the general version,
it only generates a quotient of `A`.
-/
theorem of_span_eq_top_target_aux {A : Type*} [CommRing A] [Algebra R A] [Algebra.FinitePresentation R A]
(f : A →ₐ[R] S) (hf : Function.Surjective f) (t : Finset A) (ht : Ideal.span (t : Set A) = ⊤)
(H : ∀ g : t, Algebra.FinitePresentation R (Localization.Away (f g))) : Algebra.FinitePresentation R S :=
by
apply Algebra.FinitePresentation.of_surjective hf
apply RingHom.ker_fg_of_localizationSpan t ht
intro g
let f' : Localization.Away g.val →ₐ[R] Localization.Away (f g) := Localization.awayMapₐ f g.val
have (g : t) : Algebra.FinitePresentation R (Localization.Away g.val) :=
haveI : Algebra.FinitePresentation A (Localization.Away g.val) := IsLocalization.Away.finitePresentation g.val
Algebra.FinitePresentation.trans R A (Localization.Away g.val)
apply Algebra.FinitePresentation.ker_fG_of_surjective f'
exact IsLocalization.Away.mapₐ_surjective_of_surjective _ hf
