Jacobian matrices of polynomial families at a point

For a family of polynomials p : ι → MvPolynomial σ R and a point v : σ → R, the matrix TauCeti.jacobiMatrixAt p v has (i, j) entry ∂(p i)/∂X_j evaluated at v; as a linear map it is (jacobiMatrixAt p v).mulVecLin : (σ → R) →ₗ[R] ι → R. When every p i is homogeneous and v ≠ 0, this is the cone Jacobian J_p(v) of the projective zero locus of p, whose rank at the points of that locus governs its smoothness. Full rank means that (jacobiMatrixAt p v).mulVec is surjective; over a field this says that the rank is the number of equations, by Mathlib's Matrix.mulVec_surjective_iff_rank_eq_card.

This file proves the basic properties of this rank on the cone over the zero locus. Euler's identity puts the radial direction v in the kernel at a zero, so the rank is less than the number of variables, and full rank forces fewer equations than variables. Rescaling the point multiplies each row by a power of the scalar, so the rank depends only on the projective point. In the standard affine chart where coordinate i is one, the Jacobian of the dehomogenized equations is the cone Jacobian with column i deleted. At a zero, Euler's identity writes that column in terms of the others, so the chart Jacobian at the coordinate ratios has the same image and rank as the cone Jacobian at the homogeneous coordinates. In particular full rank can be tested in any standard chart containing the point, and the answer is independent of the chart.

The Jacobian matrix is also the infinitesimal part of evaluation at a dual-number point: evaluating p at v + ε w with ε² = 0 gives p(v) + ε J_p(v) w. This turns the computation of a Jacobian into a computation of values, which is convenient when p is built from matrix products, as the multiplicativity of evaluation then replaces the Leibniz rule.

Main results

• TauCeti.jacobiMatrixAt_mulVec_self: Euler's identity J_p(v) v = (d_i p_i(v))_i.
• TauCeti.jacobiMatrixAt_mulVec_apply_eq_snd_aeval: p(v + ε w) = p(v) + ε J_p(v) w over the dual numbers, from MvPolynomial.aeval_inl_add_inr.
• TauCeti.jacobiMatrixAt_smul: J_p(t • v) = diag(t ^ (d_i - 1)) J_p(v).
• TauCeti.rank_jacobiMatrixAt_eq_of_mk_eq_mk, TauCeti.mulVec_surjective_jacobiMatrixAt_iff_of_mk_eq_mk: the rank, and so whether it is full, depends only on the projective point.
• TauCeti.jacobiMatrixAt_dehomogenize: the chart Jacobian is a submatrix of the cone Jacobian.
• TauCeti.range_mulVecLin_jacobiMatrixAt_dehomogenize, TauCeti.rank_jacobiMatrixAt_dehomogenize_div: at a zero, the chart Jacobian and the cone Jacobian have the same image and the same rank.
• TauCeti.rank_jacobiMatrixAt_lt_card, TauCeti.card_lt_card_of_mulVec_surjective_jacobiMatrixAt: at a nonzero zero, the rank is less than the number of variables, so full rank needs fewer equations than variables.
• TauCeti.mulVec_surjective_jacobiMatrixAt_iff_exists_eval_pderiv_ne_zero: a single equation has full rank exactly where some partial derivative does not vanish.

References

• W. Fulton, Algebraic Curves, Chapter 5, Section 1, for the single-equation chart criterion that the chart comparison here extends to families.
• J. Harris, Algebraic Geometry: A First Course, Lecture 14, for the projective Jacobian criterion.

noncomputable def TauCeti.jacobiMatrixAt {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] (p : ι → MvPolynomial σ R) (v : σ → R) : Matrix ι σ R

The Jacobian matrix of a family of polynomials p at a point v: its (i, j) entry is the partial derivative of p i in the variable X_j, evaluated at v. For homogeneous p and v ≠ 0 this is the cone Jacobian of the projective zero locus of p.

@[simp]

theorem TauCeti.jacobiMatrixAt_apply {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] (p : ι → MvPolynomial σ R) (v : σ → R) (i : ι) (j : σ) : jacobiMatrixAt p v i j = (MvPolynomial.eval v) ((MvPolynomial.pderiv j) (p i))

theorem TauCeti.jacobiMatrixAt_mulVec_self {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] [Fintype σ] {p : ι → MvPolynomial σ R} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) (v : σ → R) : (jacobiMatrixAt p v).mulVec v = fun (i : ι) => d i • (MvPolynomial.eval v) (p i)

Euler's identity for the Jacobian matrix of a family of homogeneous polynomials: applied to the point itself, it returns each equation's value scaled by its degree.

theorem TauCeti.jacobiMatrixAt_mulVec_self_eq_zero {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] [Fintype σ] {p : ι → MvPolynomial σ R} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) {v : σ → R} (hv : ∀ (i : ι), (MvPolynomial.eval v) (p i) = 0) : (jacobiMatrixAt p v).mulVec v = 0

At a common zero of a family of homogeneous polynomials, the radial direction lies in the kernel of the Jacobian matrix.

theorem TauCeti.jacobiMatrixAt_smul_apply {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] {p : ι → MvPolynomial σ R} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) (t : R) (v : σ → R) (i : ι) (j : σ) : jacobiMatrixAt p (t • v) i j = t ^ (d i - 1) * jacobiMatrixAt p v i j

Rescaling the point multiplies the row of a homogeneous equation of degree d by the (d - 1)-st power of the scalar.

theorem TauCeti.jacobiMatrixAt_smul {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] [Fintype ι] [DecidableEq ι] {p : ι → MvPolynomial σ R} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) (t : R) (v : σ → R) : jacobiMatrixAt p (t • v) = (Matrix.diagonal fun (i : ι) => t ^ (d i - 1)) * jacobiMatrixAt p v

Rescaling the point multiplies the Jacobian matrix of a family of homogeneous equations on the left by the diagonal matrix of the powers t ^ (d i - 1).

theorem TauCeti.jacobiMatrixAt_dehomogenize {R : Type u_1} {ι : Type u_3} [CommSemiring R] {n : ℕ} (i : Fin (n + 1)) (p : ι → MvPolynomial (Fin (n + 1)) R) (a : Fin n → R) : jacobiMatrixAt (fun (k : ι) => (dehomogenize i) (p k)) a = (jacobiMatrixAt p (i.insertNth 1 a)).submatrix id i.succAbove

In the standard affine chart where coordinate i is one, the Jacobian matrix of the dehomogenized equations is the Jacobian matrix of the homogeneous equations with column i deleted.

theorem TauCeti.jacobiMatrixAt_mulVec_apply_eq_snd_aeval {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] [Fintype σ] (p : ι → MvPolynomial σ R) (v w : σ → R) (i : ι) : (jacobiMatrixAt p v).mulVec w i = ((MvPolynomial.aeval fun (j : σ) => TrivSqZeroExt.inl (v j) + TrivSqZeroExt.inr (w j)) (p i)).snd

The Jacobian matrix as the infinitesimal part of a dual-number evaluation. The Jacobian matrix of p at v, applied to w, is the ε-coefficient of p(v + ε w).

theorem TauCeti.rank_jacobiMatrixAt_smul {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommRing R] [Finite ι] [Fintype σ] {p : ι → MvPolynomial σ R} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) {t : R} (ht : IsUnit t) (v : σ → R) : (jacobiMatrixAt p (t • v)).rank = (jacobiMatrixAt p v).rank

Rescaling the point by a unit does not change the rank of the Jacobian matrix of a family of homogeneous equations.

theorem TauCeti.col_jacobiMatrixAt_insertNth {R : Type u_1} {ι : Type u_3} [CommRing R] {n : ℕ} (i : Fin (n + 1)) {p : ι → MvPolynomial (Fin (n + 1)) R} {d : ι → ℕ} (hp : ∀ (k : ι), (p k).IsHomogeneous (d k)) {a : Fin n → R} (ha : ∀ (k : ι), (MvPolynomial.eval a) ((dehomogenize i) (p k)) = 0) : (jacobiMatrixAt p (i.insertNth 1 a)).col i = -∑ j : Fin n, a j • (jacobiMatrixAt p (i.insertNth 1 a)).col (i.succAbove j)

At a zero in the standard affine chart where coordinate i is one, Euler's identity expresses column i of the Jacobian matrix of homogeneous equations through the other columns, weighted by the affine coordinates.

theorem TauCeti.range_mulVecLin_jacobiMatrixAt_dehomogenize {R : Type u_1} {ι : Type u_3} [CommRing R] {n : ℕ} (i : Fin (n + 1)) {p : ι → MvPolynomial (Fin (n + 1)) R} {d : ι → ℕ} (hp : ∀ (k : ι), (p k).IsHomogeneous (d k)) {a : Fin n → R} (ha : ∀ (k : ι), (MvPolynomial.eval a) ((dehomogenize i) (p k)) = 0) : (jacobiMatrixAt (fun (k : ι) => (dehomogenize i) (p k)) a).mulVecLin.range = (jacobiMatrixAt p (i.insertNth 1 a)).mulVecLin.range

At a zero in the standard affine chart where coordinate i is one, the Jacobian matrix of the dehomogenized equations has the same image as the Jacobian matrix of the homogeneous equations.

theorem TauCeti.rank_jacobiMatrixAt_dehomogenize {R : Type u_1} {ι : Type u_3} [CommRing R] {n : ℕ} (i : Fin (n + 1)) {p : ι → MvPolynomial (Fin (n + 1)) R} {d : ι → ℕ} (hp : ∀ (k : ι), (p k).IsHomogeneous (d k)) {a : Fin n → R} (ha : ∀ (k : ι), (MvPolynomial.eval a) ((dehomogenize i) (p k)) = 0) : (jacobiMatrixAt (fun (k : ι) => (dehomogenize i) (p k)) a).rank = (jacobiMatrixAt p (i.insertNth 1 a)).rank

At a zero in the standard affine chart where coordinate i is one, the Jacobian matrix of the dehomogenized equations has the same rank as the Jacobian matrix of the homogeneous equations.

theorem TauCeti.rank_jacobiMatrixAt_eq_of_mk_eq_mk {σ : Type u_2} {ι : Type u_3} {K : Type u_4} [Field K] [Finite ι] [Fintype σ] {p : ι → MvPolynomial σ K} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) {v w : σ → K} (hv : v ≠ 0) (hw : w ≠ 0) (h : Projectivization.mk K v hv = Projectivization.mk K w hw) : (jacobiMatrixAt p v).rank = (jacobiMatrixAt p w).rank

The rank of the Jacobian matrix of a family of homogeneous equations at a nonzero point depends only on the projective point it represents.

theorem TauCeti.mulVec_surjective_jacobiMatrixAt_iff_of_mk_eq_mk {σ : Type u_2} {ι : Type u_3} {K : Type u_4} [Field K] [Fintype σ] {p : ι → MvPolynomial σ K} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) {v w : σ → K} (hv : v ≠ 0) (hw : w ≠ 0) (h : Projectivization.mk K v hv = Projectivization.mk K w hw) : Function.Surjective (jacobiMatrixAt p v).mulVec ↔ Function.Surjective (jacobiMatrixAt p w).mulVec

Whether the Jacobian matrix of a family of homogeneous equations at a nonzero point is onto depends only on the projective point it represents.

theorem TauCeti.rank_jacobiMatrixAt_dehomogenize_div {ι : Type u_3} {K : Type u_4} [Field K] [Finite ι] {n : ℕ} (i : Fin (n + 1)) {p : ι → MvPolynomial (Fin (n + 1)) K} {d : ι → ℕ} (hp : ∀ (k : ι), (p k).IsHomogeneous (d k)) {b : Fin (n + 1) → K} (hi : b i ≠ 0) (hb : ∀ (k : ι), (MvPolynomial.eval b) (p k) = 0) : (jacobiMatrixAt (fun (k : ι) => (dehomogenize i) (p k)) fun (j : Fin n) => b (i.succAbove j) / b i).rank = (jacobiMatrixAt p b).rank

The Jacobian criterion in a ratio chart: at a common zero b of a family of homogeneous equations with b i ≠ 0, the Jacobian matrix of the dehomogenized equations at the coordinate ratios b (i.succAbove j) / b i has the same rank as the Jacobian matrix of the homogeneous equations at b.

theorem TauCeti.rank_jacobiMatrixAt_lt_card {σ : Type u_2} {ι : Type u_3} {K : Type u_4} [Field K] [Fintype σ] {p : ι → MvPolynomial σ K} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) {v : σ → K} (hv : v ≠ 0) (hpv : ∀ (i : ι), (MvPolynomial.eval v) (p i) = 0) : (jacobiMatrixAt p v).rank < Fintype.card σ

At a nonzero common zero of a family of homogeneous equations, the rank of the Jacobian matrix is less than the number of variables, since the radial direction lies in its kernel.

theorem TauCeti.card_lt_card_of_mulVec_surjective_jacobiMatrixAt {σ : Type u_2} {ι : Type u_3} {K : Type u_4} [Field K] [Fintype ι] [Fintype σ] {p : ι → MvPolynomial σ K} {d : ι → ℕ} (hp : ∀ (i : ι), (p i).IsHomogeneous (d i)) {v : σ → K} (hv : v ≠ 0) (hpv : ∀ (i : ι), (MvPolynomial.eval v) (p i) = 0) (hJ : Function.Surjective (jacobiMatrixAt p v).mulVec) : Fintype.card ι < Fintype.card σ

At a nonzero common zero of a family of homogeneous equations where the Jacobian matrix has full rank, there are fewer equations than variables.

theorem TauCeti.mulVec_surjective_jacobiMatrixAt_iff_exists_eval_pderiv_ne_zero {σ : Type u_2} {ι : Type u_3} {K : Type u_4} [Field K] [Unique ι] [Fintype σ] {p : ι → MvPolynomial σ K} {v : σ → K} : Function.Surjective (jacobiMatrixAt p v).mulVec ↔ ∃ (j : σ), (MvPolynomial.eval v) ((MvPolynomial.pderiv j) (p default)) ≠ 0

The Jacobian criterion for a single equation: the Jacobian matrix of a hypersurface equation has full rank at a point exactly when some partial derivative of the equation is nonzero there.