The Jacobian criterion for hypersurfaces

Let f ∈ A, and let P be a prime of the hypersurface ring A ⧸ (f) lying over a prime Q of A at which A is regular, i.e. A_Q is a regular local ring. If some derivation D of A has D f ∉ Q, then the local ring (A ⧸ (f))_P is regular: f lies outside the square of the maximal ideal of the regular local ring A_Q, so it is a regular parameter there, and (A ⧸ (f))_P is A_Q ⧸ (f).

For A = k[X, Y] over a field k and the partial derivatives ∂f/∂X and ∂f/∂Y, this is the Jacobian criterion for plane curves: if f is irreducible and f, ∂f/∂X, ∂f/∂Y generate the unit ideal, so that the affine curve f = 0 has no singular point over any extension of k, then the local ring of k[X, Y] ⧸ (f) at every nonzero prime is a discrete valuation ring and k[X, Y] ⧸ (f) is a Dedekind domain. In particular the coordinate ring of a smooth affine plane curve is integrally closed in the function field of the curve; this is what identifies it with the integral closure of k[x] when y is integral over k[x], the setting in which differents of the function field over k(x) are computed from ∂f/∂Y.

Main results

• Ideal.isRegularLocalRing_localization_of_derivation_notMem: the localization of A ⧸ (f) at a prime over Q is a regular local ring when A_Q is regular and D f ∉ Q.
• MvPolynomial.isDedekindDomain_quotient_span_singleton: the coordinate ring of a smooth irreducible affine plane curve over a field is a Dedekind domain.
• MvPolynomial.isIntegrallyClosed_adjoin_singleton: if the minimal polynomial of y over k[X] is the equation of a smooth affine plane curve, then k[X][y] is integrally closed.

References

• Stacks Project, Lemma 10.106.3: the quotient of a regular local ring by a regular parameter is regular.
• W. Fulton, Algebraic Curves, Section 3.2, Theorem 1: a point of a plane curve is simple exactly when its local ring is a discrete valuation ring.

theorem Ideal.isRegularLocalRing_localization_of_derivation_notMem {R : Type u_1} {A : Type u_2} [CommRing R] [CommRing A] [Algebra R A] {f : A} (P : Ideal (A ⧸ span {f})) [P.IsPrime] [IsRegularLocalRing (Localization.AtPrime (comap (Quotient.mk (span {f})) P))] {D : Derivation R A A} (hD : D f ∉ comap (Quotient.mk (span {f})) P) : IsRegularLocalRing (Localization.AtPrime P)

The Jacobian criterion for a hypersurface. Let f ∈ A and let P be a prime of A ⧸ (f) lying over the prime Q of A, with A_Q a regular local ring. If some derivation D of A maps f outside Q, then the localization of A ⧸ (f) at P is a regular local ring.

theorem MvPolynomial.isDedekindDomain_quotient_span_singleton {k : Type u_1} [Field k] {f : MvPolynomial (Fin 2) k} (hf : Irreducible f) (hsm : Ideal.span {f, (pderiv 0) f, (pderiv 1) f} = ⊤) : IsDedekindDomain (MvPolynomial (Fin 2) k ⧸ Ideal.span {f})

The coordinate ring of a smooth affine plane curve is a Dedekind domain. If f ∈ k[X, Y] is irreducible and f, ∂f/∂X, ∂f/∂Y generate the unit ideal, that is the curve f = 0 has no singular point, then k[X, Y] ⧸ (f) is a Dedekind domain.

theorem MvPolynomial.isIntegrallyClosed_adjoin_singleton {k : Type u_1} [Field k] {S : Type u_2} [CommRing S] [IsDomain S] [Algebra (Polynomial k) S] [Module.IsTorsionFree (Polynomial k) S] {f : MvPolynomial (Fin 2) k} {y : S} (hy : IsIntegral (Polynomial k) y) (hf : (Polynomial.Bivariate.equivMvPolynomial k) (minpoly (Polynomial k) y) = f) (hsm : Ideal.span {f, (pderiv 0) f, (pderiv 1) f} = ⊤) : IsIntegrallyClosed ↥(Polynomial k)[y]

The coordinate ring k[x][y] of a smooth affine plane curve is integrally closed. Let y be integral over k[X], and suppose its minimal polynomial, read as a polynomial f ∈ k[X, Y], has f, ∂f/∂X, ∂f/∂Y generating the unit ideal. Then k[X][y] ≅ k[X, Y] ⧸ (f) is integrally closed.