noncomputable def maxIdealOfPoint_SJC {k : Type u_1} [Field k] {n : ℕ} (x : Fin n → k) : Ideal (MvPolynomial (Fin n) k)

The maximal ideal of k[x₁,…,xₙ] corresponding to a k-rational point x: the kernel of evaluation at x.

instance maxIdealOfPoint_SJC_isMaximal {k : Type u_1} [Field k] {n : ℕ} (x : Fin n → k) : (maxIdealOfPoint_SJC x).IsMaximal

maxIdealOfPoint_SJC x is maximal: evaluation at a rational point gives a ring homomorphism onto the field k.

noncomputable def maxIdealInQuotient_SJC {k : Type u_1} [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) (x : Fin n → k) : I ≤ maxIdealOfPoint_SJC x → Ideal (MvPolynomial (Fin n) k ⧸ I)

Image of the point-maximal-ideal in the quotient k[x]/I: the maximal ideal of the closed point x in the affine variety V(I).

instance maxIdealInQuotient_SJC_isMaximal {k : Type u_1} [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) (x : Fin n → k) (hI : I ≤ maxIdealOfPoint_SJC x) : (maxIdealInQuotient_SJC I x hI).IsMaximal

The image of the point ideal in the quotient is maximal.

instance maxIdealInQuotient_SJC_isPrime {k : Type u_1} [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) (x : Fin n → k) (hI : I ≤ maxIdealOfPoint_SJC x) : (maxIdealInQuotient_SJC I x hI).IsPrime

The image of the point ideal in the quotient is prime (follows from maximal).

@[reducible, inline]

abbrev localRingAtPoint_SJC {k : Type u_1} [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) (x : Fin n → k) (hI : I ≤ maxIdealOfPoint_SJC x) : Type u_1

The local ring at a k-rational point x of an affine variety V(I): the localization of k[x]/I at the maximal ideal of x.

noncomputable def jacobianMatrix_SJC {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (x : Fin n → k) : Matrix (Fin m) (Fin n) k

Jacobian matrix of a finite system f₁,…,fₘ of polynomials in x₁,…,xₙ evaluated at the point x.

theorem cotangentSpace_finrank_eq_n_sub_jacobianRank_SJC {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (x : Fin n → k) (hx : ∀ (i : Fin m), (MvPolynomial.eval x) (f i) = 0) (hI : Ideal.span (Set.range f) ≤ maxIdealOfPoint_SJC x) : Module.finrank (IsLocalRing.ResidueField (localRingAtPoint_SJC (Ideal.span (Set.range f)) x hI)) (IsLocalRing.CotangentSpace (localRingAtPoint_SJC (Ideal.span (Set.range f)) x hI)) = n - (jacobianMatrix_SJC f x).rank

Cotangent dimension formula: at a rational point x of V(f₁,…,fₘ), the dimension of the cotangent space 𝔪/𝔪² equals n − rank J(x), where J is the Jacobian matrix.

theorem corollary23_jacobian_rank_SJC {k : Type u_1} [Field k] {n m : ℕ} (f : Fin m → MvPolynomial (Fin n) k) (x : Fin n → k) (hx : ∀ (i : Fin m), (MvPolynomial.eval x) (f i) = 0) (hI : Ideal.span (Set.range f) ≤ maxIdealOfPoint_SJC x) (hdim : ringKrullDim (localRingAtPoint_SJC (Ideal.span (Set.range f)) x hI) = ↑(n - m)) (hmn : m ≤ n) : (jacobianMatrix_SJC f x).rank = m ↔ IsRegularLocalRing (localRingAtPoint_SJC (Ideal.span (Set.range f)) x hI)

Corollary 23 (Jacobian Criterion for Smoothness): when the Krull dimension of the local ring at x equals n - m, the Jacobian rank is m (full rank) iff the local ring at x is regular, i.e., the variety is smooth at x.

theorem matrix_fin1_rank_eq_one_iff_SJC {k : Type u_1} [Field k] {n : ℕ} (M : Matrix (Fin 1) (Fin n) k) : M.rank = 1 ↔ ∃ (j : Fin n), M 0 j ≠ 0

A 1 × n matrix over a field has rank one iff it is non-zero (equivalently, has a non-zero entry).

theorem corollary23_hypersurface_criterion_SJC {k : Type u_1} [Field k] {n : ℕ} (P : MvPolynomial (Fin n) k) (x : Fin n → k) (_hx : (MvPolynomial.eval x) P = 0) : (∃ (i : Fin n), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) P) ≠ 0) ↔ (jacobianMatrix_SJC (fun (x : Fin 1) => P) x).rank = 1

Hypersurface Jacobian rank criterion: for a single polynomial P vanishing at x, the Jacobian has full rank 1 iff some partial derivative ∂P/∂xᵢ is non-zero at x.

theorem corollary23_jacobian_hypersurface_SJC {k : Type u_1} [Field k] {n : ℕ} (P : MvPolynomial (Fin n) k) (x : Fin n → k) (hx : (MvPolynomial.eval x) P = 0) (hI : Ideal.span (Set.range fun (x : Fin 1) => P) ≤ maxIdealOfPoint_SJC x) (hdim : ringKrullDim (localRingAtPoint_SJC (Ideal.span (Set.range fun (x : Fin 1) => P)) x hI) = ↑(n - 1)) (hn : 1 ≤ n) : (∃ (i : Fin n), (MvPolynomial.eval x) ((MvPolynomial.pderiv i) P) ≠ 0) ↔ IsRegularLocalRing (localRingAtPoint_SJC (Ideal.span (Set.range fun (x : Fin 1) => P)) x hI)

Smoothness criterion for hypersurfaces (Corollary 23): a hypersurface V(P) of dimension n - 1 is smooth at x iff some partial derivative of P is non-zero at x — the classical "gradient is non-zero" criterion.