The Hessian of an element of a local ring

Let P be a local ring whose maximal ideal 𝔪 is generated by finitely many coordinates x : ι → P, and let D : ι → Derivation R P P be dual derivations, Dᵢ xⱼ = δᵢⱼ. For instance P is the local ring at a point of a smooth variety, with étale coordinates centred there and the partial derivatives along them. The Hessian of f ∈ P is the matrix (Dᵢ Dⱼ f).

For a quadratic form f = Σ Qₖₗ xₖ xₗ in the coordinates, the Hessian is, modulo 𝔪, the polar matrix Q + Qᵀ (TauCeti.residue_hessian_sum_mul_mul), so for such f a unit Hessian determinant says that the form is nondegenerate. This file proves a criterion for the Hessian determinant to be a unit in terms of the partial derivatives: for f ∈ 𝔪², the partial derivatives Dⱼ f generate 𝔪 exactly when the Hessian determinant is a unit (TauCeti.span_range_apply_eq_maximalIdeal_iff_isUnit_det_hessian). Consequently the Jacobian ideal (f, D₁ f, …, Dₙ f) is the maximal ideal exactly when f ∈ 𝔪² and the Hessian determinant of f is a unit (TauCeti.span_range_apply_sup_span_singleton_eq_maximalIdeal_iff). For a nonzero f in the local ring at a closed point of a smooth n-dimensional variety, with x local coordinates there, this ideal cuts out the singular locus of the hypersurface f = 0, and the criterion says that this locus is the reduced closed point exactly when f ∈ 𝔪² and the Hessian determinant of f is a unit, that is, the quadratic part of f has nondegenerate polar form. This agrees with the ordinary double point condition except in characteristic 2 with n odd: there the polar matrix Q + Qᵀ is alternating of odd size, hence singular, so that an ordinary double point such as x₁² + x₂ x₃ never has a unit Hessian determinant. For two coordinates, the nondegeneracy of a s² + b s t + c t² is the condition that its discriminant b² - 4ac be a unit (TauCeti.isUnit_det_hessian_iff_isUnit_discrim), in every characteristic; the coordinates s, t need only lie in 𝔪 for this.

Main definitions

• TauCeti.hessian D f: the matrix (Dᵢ (Dⱼ f)).

Main results

• TauCeti.mem_maximalIdeal_sq_iff_forall_apply_mem: an element f ∈ 𝔪 lies in 𝔪² exactly when all its partial derivatives lie in 𝔪.

• TauCeti.map_residue_hessian_mul_transpose_eq_one: if xₖ ≡ Σⱼ Cₖⱼ Dⱼ f modulo 𝔪², then H Cᵀ ≡ 1 modulo 𝔪, for H the Hessian of f.

• TauCeti.sub_sum_inv_hessian_mul_apply_mem_maximalIdeal_sq: conversely, if H is invertible, then xₖ ≡ Σⱼ (H⁻¹)ⱼₖ Dⱼ f modulo 𝔪².

• TauCeti.maximalIdeal_le_span_range_apply_sup_iff_isUnit_det_hessian: for f ∈ 𝔪², the partial derivatives of f span the cotangent space 𝔪/𝔪² exactly when the Hessian determinant is a unit.

• TauCeti.span_range_apply_eq_maximalIdeal_iff_isUnit_det_hessian: the same, in the form (D₁ f, …, Dₙ f) = 𝔪.

• TauCeti.span_range_apply_sup_span_singleton_eq_maximalIdeal_iff: the Jacobian ideal (f, D₁ f, …, Dₙ f) is 𝔪 exactly when f ∈ 𝔪² and the Hessian determinant is a unit.

• TauCeti.residue_hessian_sum_mul_mul: modulo 𝔪, the Hessian of Σ Qₖₗ xₖ xₗ is Q + Qᵀ.

• TauCeti.isUnit_det_hessian_iff_isUnit_discrim: the Hessian of a s² + b s t + c t² has unit determinant exactly when b² - 4ac is a unit.

• TauCeti.exists_eq_unit_mul_quadratic_of_isUnit_discrim: over a local ring, a binary quadratic form with unit discriminant is, after a change of generators, a unit multiple of a' x² + b' x y + y², with b'² - 4a' a unit.

• TauCeti.algebraMap_residueField_det_hessian_ne_zero_iff: the same at a prime Q of a ring that need not be local, for coordinates s, t ∈ Q, with nonvanishing in κ(Q) in place of being a unit; it follows by localizing at Q.

References

• Stacks Project, Section 53.19, Tag 0C46: nodes of curves, defined by a nondegenerate quadratic form in two variables.

def TauCeti.hessian {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] (D : ι → Derivation R P P) (f : P) : Matrix ι ι P

The Hessian matrix (Dᵢ (Dⱼ f)) of f with respect to a family of derivations D.

@[simp]

theorem TauCeti.hessian_apply {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] (D : ι → Derivation R P P) (f : P) (i j : ι) : hessian D f i j = (D i) ((D j) f)

theorem TauCeti.sub_sum_apply_mul_mem_maximalIdeal_sq {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] [DecidableEq ι] {x : ι → P} {D : ι → Derivation R P P} [Fintype ι] (hx : IsLocalRing.maximalIdeal P = Ideal.span (Set.range x)) (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) {g : P} (hg : g ∈ IsLocalRing.maximalIdeal P) : g - ∑ i : ι, (D i) g * x i ∈ IsLocalRing.maximalIdeal P ^ 2

First-order Taylor expansion. An element g ∈ 𝔪 agrees with Σ (Dᵢ g) xᵢ modulo 𝔪².

theorem TauCeti.mem_maximalIdeal_sq_iff_forall_apply_mem {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] [DecidableEq ι] {x : ι → P} {D : ι → Derivation R P P} (hx : IsLocalRing.maximalIdeal P = Ideal.span (Set.range x)) (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) {f : P} (hf : f ∈ IsLocalRing.maximalIdeal P) : f ∈ IsLocalRing.maximalIdeal P ^ 2 ↔ ∀ (i : ι), (D i) f ∈ IsLocalRing.maximalIdeal P

An element f ∈ 𝔪 lies in 𝔪² exactly when all its partial derivatives Dᵢ f lie in 𝔪.

theorem TauCeti.map_residue_hessian_mul_transpose_eq_one {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] [DecidableEq ι] {x : ι → P} {D : ι → Derivation R P P} [Fintype ι] (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) {f : P} (hDf : ∀ (j : ι), (D j) f ∈ IsLocalRing.maximalIdeal P) {C : Matrix ι ι P} (hC : ∀ (k : ι), x k - ∑ j : ι, C k j * (D j) f ∈ IsLocalRing.maximalIdeal P ^ 2) : (hessian D f * C.transpose).map ⇑(IsLocalRing.residue P) = 1

If xₖ ≡ Σⱼ Cₖⱼ Dⱼ f modulo 𝔪² for every k, and the partial derivatives of f lie in 𝔪, then H Cᵀ ≡ 1 modulo 𝔪, where H is the Hessian of f.

theorem TauCeti.sub_sum_inv_hessian_mul_apply_mem_maximalIdeal_sq {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] [DecidableEq ι] {x : ι → P} {D : ι → Derivation R P P} [Fintype ι] (hx : IsLocalRing.maximalIdeal P = Ideal.span (Set.range x)) (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) {f : P} (hDf : ∀ (j : ι), (D j) f ∈ IsLocalRing.maximalIdeal P) (hdet : IsUnit (hessian D f).det) (k : ι) : x k - ∑ j : ι, (hessian D f)⁻¹ j k * (D j) f ∈ IsLocalRing.maximalIdeal P ^ 2

If the Hessian determinant of f is a unit and the partial derivatives of f lie in 𝔪, then each coordinate is xₖ ≡ Σⱼ (H⁻¹)ⱼₖ Dⱼ f modulo 𝔪², where H is the Hessian of f.

theorem TauCeti.maximalIdeal_le_span_range_apply_sup_iff_isUnit_det_hessian {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] [DecidableEq ι] {x : ι → P} {D : ι → Derivation R P P} [Fintype ι] (hx : IsLocalRing.maximalIdeal P = Ideal.span (Set.range x)) (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) {f : P} (hf : f ∈ IsLocalRing.maximalIdeal P ^ 2) : IsLocalRing.maximalIdeal P ≤ Ideal.span (Set.range fun (j : ι) => (D j) f) ⊔ IsLocalRing.maximalIdeal P ^ 2 ↔ IsUnit (hessian D f).det

The Hessian criterion for a nondegenerate quadratic part. For f ∈ 𝔪², the partial derivatives Dⱼ f span the cotangent space 𝔪/𝔪² exactly when the Hessian determinant is a unit.

theorem TauCeti.span_range_apply_eq_maximalIdeal_iff_isUnit_det_hessian {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] [DecidableEq ι] {x : ι → P} {D : ι → Derivation R P P} [Fintype ι] (hx : IsLocalRing.maximalIdeal P = Ideal.span (Set.range x)) (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) {f : P} (hf : f ∈ IsLocalRing.maximalIdeal P ^ 2) : Ideal.span (Set.range fun (j : ι) => (D j) f) = IsLocalRing.maximalIdeal P ↔ IsUnit (hessian D f).det

For f ∈ 𝔪², the partial derivatives Dⱼ f generate the maximal ideal exactly when the Hessian determinant of f is a unit.

theorem TauCeti.span_range_apply_sup_span_singleton_eq_maximalIdeal_iff {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] [DecidableEq ι] {x : ι → P} {D : ι → Derivation R P P} [Fintype ι] (hx : IsLocalRing.maximalIdeal P = Ideal.span (Set.range x)) (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) {f : P} : Ideal.span (Set.range fun (j : ι) => (D j) f) ⊔ Ideal.span {f} = IsLocalRing.maximalIdeal P ↔ f ∈ IsLocalRing.maximalIdeal P ^ 2 ∧ IsUnit (hessian D f).det

The Jacobian ideal of a nondegenerate quadratic singularity. The ideal (f, D₁ f, …, Dₙ f) is the maximal ideal exactly when f ∈ 𝔪² and the Hessian determinant of f is a unit.

theorem TauCeti.residue_hessian_sum_mul_mul {R : Type u_1} {P : Type u_2} {ι : Type u_3} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] [DecidableEq ι] {x : ι → P} {D : ι → Derivation R P P} [Fintype ι] (hx : ∀ (i : ι), x i ∈ IsLocalRing.maximalIdeal P) (hD : ∀ (i j : ι), (D i) (x j) = if i = j then 1 else 0) (Q : Matrix ι ι P) (i j : ι) : (IsLocalRing.residue P) (hessian D (∑ k : ι, ∑ l : ι, Q k l * x k * x l) i j) = (IsLocalRing.residue P) (Q i j + Q j i)

The Hessian of a quadratic form is its polar matrix. Modulo the maximal ideal, the Hessian of Σₖ Σₗ Qₖₗ xₖ xₗ is Q + Qᵀ.

theorem TauCeti.isUnit_det_hessian_iff_isUnit_discrim {R : Type u_1} {P : Type u_2} [CommSemiring R] [CommRing P] [Algebra R P] [IsLocalRing P] {x : Fin 2 → P} {D : Fin 2 → Derivation R P P} (hx : ∀ (i : Fin 2), x i ∈ IsLocalRing.maximalIdeal P) (hD : ∀ (i j : Fin 2), (D i) (x j) = if i = j then 1 else 0) (a b c : P) : IsUnit (hessian D (a * x 0 ^ 2 + b * x 0 * x 1 + c * x 1 ^ 2)).det ↔ IsUnit (discrim a b c)

The node condition in two variables. For s = x 0, t = x 1 in 𝔪 with dual derivations D, the Hessian of a s² + b s t + c t² has unit determinant exactly when the discriminant b² - 4ac is a unit.

theorem TauCeti.exists_eq_unit_mul_quadratic_of_isUnit_discrim {P : Type u_2} [CommRing P] [IsLocalRing P] {u v a b c : P} (hd : IsUnit (discrim a b c)) : ∃ (x : P) (y : P) (a' : P) (b' : P) (e : P), IsUnit e ∧ Ideal.span {x, y} = Ideal.span {u, v} ∧ a * u ^ 2 + b * u * v + c * v ^ 2 = e * (a' * x ^ 2 + b' * x * y + y ^ 2) ∧ IsUnit (discrim a' b' 1)

Normal form of a binary quadratic form with unit discriminant. Over a local ring, if b² - 4ac is a unit, then after replacing the generators u, v of the ideal (u, v) by suitable generators x, y, the form a u² + b u v + c v² becomes e (a' x² + b' x y + y²) for a unit e, with b'² - 4a' a unit.

theorem TauCeti.algebraMap_residueField_det_hessian_ne_zero_iff {R : Type u_1} {P : Type u_2} [CommRing R] [CommRing P] [Algebra R P] {Q : Ideal P} [Q.IsPrime] {x : Fin 2 → P} {D : Fin 2 → Derivation R P P} (hx : ∀ (i : Fin 2), x i ∈ Q) (hD : ∀ (i j : Fin 2), (D i) (x j) = if i = j then 1 else 0) (a b c : P) : (algebraMap P Q.ResidueField) (hessian D (a * x 0 ^ 2 + b * x 0 * x 1 + c * x 1 ^ 2)).det ≠ 0 ↔ (algebraMap P Q.ResidueField) (discrim a b c) ≠ 0

Nondegeneracy of a binary quadratic form at a prime. Let D₀, D₁ be derivations of P dual to elements x₀, x₁ of a prime Q, so Dᵢ xⱼ = δᵢⱼ. The Hessian of a x₀² + b x₀ x₁ + c x₁² has determinant nonzero in the residue field κ(Q) exactly when the discriminant b² - 4ac is nonzero in κ(Q).