Presentations of away localizations from generic generation of the kernel

Let ϕ : R[V] → A be a surjection of R-algebras and k a family in its kernel which generates the kernel after inverting some g ∈ R[V]. Then A[1/ϕ g] is presented over R by the variables V and one more variable inverting g, subject to the relations k and one more relation.

Main results

• Algebra.Presentation.nonempty_presentation_localizationAway: such a presentation of A[1/ϕ g] exists.

theorem Algebra.Presentation.nonempty_presentation_localizationAway {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {V : Type u_3} {τ : Type u_4} {ϕ : MvPolynomial V R →ₐ[R] A} (hϕ : Function.Surjective ⇑ϕ) {k : τ → MvPolynomial V R} (hk : ∀ (l : τ), k l ∈ RingHom.ker ϕ) {g : MvPolynomial V R} (hg : ∀ x ∈ RingHom.ker ϕ, g * x ∈ Ideal.span (Set.range k)) : Nonempty (Presentation R (Localization.Away (ϕ g)) (Unit ⊕ V) (Unit ⊕ τ))

If the kernel of a surjection ϕ : R[V] → A is generated by a family k after inverting g, then A[1/ϕ g] has a presentation over R with one more generator than R[V] and one more relation than k.