Lifting presentations from a fibre

Let A be a flat and finitely presented R-algebra, p a prime of R and q a prime of A lying over p. Suppose the fibre κ(p) ⊗[R] A has a presentation over κ(p) with n + c generators and c relations. Then some localization A[1/g] with g ∉ q has a presentation over R with n + c' generators and c' relations (Algebra.Presentation.exists_presentation_localizationAway_of_fiber).

This is the presentation half of the fibrewise criterion for syntomic morphisms, which asserts that a flat, finitely presented algebra whose fibres are relative global complete intersections of relative dimension n is, locally on the source, a relative global complete intersection of relative dimension n. The other half is the dimension of the fibres of A[1/g], which the theorem here does not address.

The proof presents A by generators x_i ↦ f (X i) of A together with lifts y_j ↦ a_j of the generators of the fibre presentation, which exist up to units of κ(p).

• On the fibre, each x_i is a polynomial Φ i in the y_j, so the kernel of the fibre map is generated by the m elements x_i - Φ i and the c relations of the fibre presentation (MvPolynomial.ker_eq_map_ker_comp_rename_inr_sup, Algebra.Presentation.exists_ker_eq_span_range).
• These generators lift, up to units, to elements k_l of the kernel K of R[x, y] → A (MvPolynomial.exists_C_mul_eq_map_of_mem_map).
• As A is flat, K ∩ p R[x, y] = p K; Nakayama's lemma, in the form of supports of finite modules, shows that the k_l generate K after inverting some g ∉ q (MvPolynomial.exists_notMem_forall_mul_mem_of_map_ker_le).

Main results

• Algebra.Presentation.exists_presentation_localizationAway_of_fiber: the lifting theorem.
• MvPolynomial.exists_notMem_forall_mul_mem_of_map_ker_le: an ideal J contained in the kernel K of a surjection R[V] → A onto a flat R-algebra, which generates K on the fibre over p, agrees with K near every prime over p.
• MvPolynomial.ker_eq_map_ker_comp_rename_inr_sup: eliminating redundant variables from the kernel of a map out of a polynomial ring.

References

• The Stacks Project, Commutative Algebra, Section Syntomic morphisms (the lemma that a flat finitely presented ring map whose fibre is a local complete intersection at a prime is a relative global complete intersection near that prime) and Section Nakayama's lemma.

theorem MvPolynomial.exists_C_mul_eq_map_residueField {R : Type u_1} [CommRing R] {p : Ideal R} [p.IsPrime] {V : Type u_2} (c : MvPolynomial V p.ResidueField) : ∃ s ∉ p, ∃ (d : MvPolynomial V R), C ((algebraMap R p.ResidueField) s) * c = (map (algebraMap R p.ResidueField)) d

Every polynomial over the residue field κ(p) becomes, after multiplication by the image of some s ∉ p, the image of a polynomial over R.

theorem MvPolynomial.exists_C_mul_eq_map_of_mem_map {R : Type u_1} [CommRing R] {p : Ideal R} [p.IsPrime] {V : Type u_2} {L : Ideal (MvPolynomial V R)} {z : MvPolynomial V p.ResidueField} (hz : z ∈ Ideal.map (map (algebraMap R p.ResidueField)) L) : ∃ s ∉ p, ∃ y ∈ L, C ((algebraMap R p.ResidueField) s) * z = (map (algebraMap R p.ResidueField)) y

An element of the extension of an ideal L ⊆ R[V] to κ(p)[V] is, after multiplication by the image of some s ∉ p, the image of an element of L.

theorem MvPolynomial.exists_C_mul_mem_sup_of_map_mem_map {R : Type u_1} [CommRing R] {p : Ideal R} [p.IsPrime] {V : Type u_2} {L : Ideal (MvPolynomial V R)} {x : MvPolynomial V R} (hx : (map (algebraMap R p.ResidueField)) x ∈ Ideal.map (map (algebraMap R p.ResidueField)) L) : ∃ s ∉ p, C s * x ∈ L ⊔ Ideal.map C p

If the image of x ∈ R[V] in κ(p)[V] lies in the extension of an ideal L, then s x lies in L + p R[V] for some s ∉ p.

theorem MvPolynomial.exists_notMem_forall_mul_mem_of_map_ker_le {R : Type u_1} [CommRing R] {p : Ideal R} [p.IsPrime] {V : Type u_2} {A : Type u_3} [CommRing A] [Algebra R A] [Module.Flat R A] {ϕ : MvPolynomial V R →ₐ[R] A} (hϕ : Function.Surjective ⇑ϕ) (hK : (RingHom.ker ϕ).FG) {J : Ideal (MvPolynomial V R)} (hJ : J ≤ RingHom.ker ϕ) (h : Ideal.map (map (algebraMap R p.ResidueField)) (RingHom.ker ϕ) ≤ Ideal.map (map (algebraMap R p.ResidueField)) J) (Q : Ideal (MvPolynomial V R)) [Q.IsPrime] [Q.LiesOver p] : ∃ g ∉ Q, ∀ k ∈ RingHom.ker ϕ, g * k ∈ J

Let A be a flat R-algebra, presented as a quotient of R[V] with finitely generated kernel K. If an ideal J ⊆ K generates K on the fibre over p, in the sense that K and J have the same extension to κ(p)[V], then J and K agree near every prime Q of R[V] lying over p: some g ∉ Q satisfies g K ⊆ J.

theorem MvPolynomial.ker_eq_map_ker_comp_rename_inr_sup {B : Type u_4} {S : Type u_5} [CommRing B] [CommRing S] [Algebra B S] {ι : Type u_6} {σ : Type u_7} {ψ : MvPolynomial (ι ⊕ σ) B →ₐ[B] S} (Φ : ι → MvPolynomial σ B) (hΦ : ∀ (i : ι), ψ ((rename Sum.inr) (Φ i)) = ψ (X (Sum.inl i))) : RingHom.ker ψ = Ideal.map (rename Sum.inr) (RingHom.ker (ψ.comp (rename Sum.inr))) ⊔ Ideal.span (Set.range fun (i : ι) => X (Sum.inl i) - (rename Sum.inr) (Φ i))

Eliminating redundant variables. If ψ : B[ι ⊕ σ] → S sends each variable X (inl i) to the image of a polynomial Φ i in the remaining variables, then the kernel of ψ is generated by the kernel of its restriction to B[σ] together with the relations X (inl i) - Φ i.

theorem Algebra.Presentation.exists_ker_eq_span_range {B : Type u_1} {S : Type u_2} {σ : Type u_3} {τ : Type u_4} [CommRing B] [CommRing S] [Algebra B S] (Q : Presentation B S σ τ) (u : σ → Bˣ) {ι : Type u_5} {ψ : MvPolynomial (ι ⊕ σ) B →ₐ[B] S} (hψ : ψ.comp (MvPolynomial.rename Sum.inr) = MvPolynomial.aeval fun (j : σ) => ↑(u j) • Q.val j) : ∃ (G : ι ⊕ τ → MvPolynomial (ι ⊕ σ) B), RingHom.ker ψ = Ideal.span (Set.range G)

Let Q present S over B with generators indexed by σ and relations indexed by τ, and let ψ : B[ι ⊕ σ] → S send the variables X (inr j) to the generators of Q rescaled by units u j. Then the kernel of ψ is generated by a family indexed by ι ⊕ τ: the rescaled relations of Q and one relation eliminating each variable X (inl i).

theorem Algebra.Presentation.exists_presentation_localizationAway_of_fiber {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] [Module.Flat R A] [FinitePresentation R A] {p : Ideal R} [p.IsPrime] {σ : Type u_3} {τ : Type u_4} [Finite σ] [Finite τ] {n : ℕ} (Q : Presentation p.ResidueField (p.Fiber A) σ τ) (hQ : Nat.card σ = n + Nat.card τ) (q : Ideal A) [q.IsPrime] [q.LiesOver p] : ∃ g ∉ q, ∃ (ι' : Type) (σ' : Type) (_ : Finite ι') (_ : Finite σ') (x : Presentation R (Localization.Away g) ι' σ'), Nat.card ι' = n + Nat.card σ'

Lifting presentations from a fibre. Let A be a flat and finitely presented R-algebra, and q a prime of A lying over a prime p of R. If the fibre κ(p) ⊗[R] A has a presentation over κ(p) with n + c generators and c relations, then for some g ∉ q the localization A[1/g] has a presentation over R with n + c' generators and c' relations.