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

The maximal ideal of polynomials in k[X_1, ..., X_n] vanishing at the point x.

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

The maximal ideal at a point is genuinely maximal.

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

The image of the maximal ideal at x in the quotient k[X]/I, for I contained in that maximal ideal.

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

The image maximal ideal in the quotient is maximal.

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

The image maximal ideal in the quotient is prime.

@[reducible, inline]

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

The local ring of the variety V(I) at the point x.

noncomputable def jacobianMatrix_P31 {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

The Jacobian matrix of f_1, ..., f_m ∈ k[X_1, ..., X_n] at the point x ∈ k^n.

theorem cotangentSpace_finrank_eq_n_sub_jacobianRank_P31 {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_P31 x) : Module.finrank (IsLocalRing.ResidueField (localRingAtPoint_P31 (Ideal.span (Set.range f)) x hI)) (IsLocalRing.CotangentSpace (localRingAtPoint_P31 (Ideal.span (Set.range f)) x hI)) = n - (jacobianMatrix_P31 f x).rank

For a variety cut out by f_1, ..., f_m at a point x where all f_i vanish, the cotangent space dimension equals n − rank(Jacobian).

theorem proposition31_forward {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_P31 x) (hdim : ringKrullDim (localRingAtPoint_P31 (Ideal.span (Set.range f)) x hI) = ↑(n - m)) (_hmn : m ≤ n) (hrank : (jacobianMatrix_P31 f x).rank = m) : IsRegularLocalRing (localRingAtPoint_P31 (Ideal.span (Set.range f)) x hI)

Forward direction of Proposition 31 (Jacobian criterion): if m local generators with m × n Jacobian of maximal rank m cut out a V of dimension n − m at x, then the local ring at x is regular.

theorem proposition31_converse_aux {k : Type u_1} [Field k] {n m : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) (x : Fin n → k) (hI : I ≤ maxIdealOfPoint_P31 x) (hdim : ringKrullDim (localRingAtPoint_P31 I x hI) = ↑(n - m)) (hmn : m ≤ n) (hreg : IsRegularLocalRing (localRingAtPoint_P31 I x hI)) : ∃ (f : Fin m → MvPolynomial (Fin n) k), (∀ (i : Fin m), f i ∈ I) ∧ (∀ (i : Fin m), (MvPolynomial.eval x) (f i) = 0) ∧ (jacobianMatrix_P31 f x).rank = m ∧ Ideal.span (Set.range f) = I

Converse direction of Proposition 31: if the local ring is regular and of dimension n − m, then I is locally generated by m polynomials with linearly independent differentials.

theorem proposition31_smooth_iff_local_generators {k : Type u_1} [Field k] {n m : ℕ} (I : Ideal (MvPolynomial (Fin n) k)) (x : Fin n → k) (hI : I ≤ maxIdealOfPoint_P31 x) (hdim : ringKrullDim (localRingAtPoint_P31 I x hI) = ↑(n - m)) (hmn : m ≤ n) : IsRegularLocalRing (localRingAtPoint_P31 I x hI) ↔ ∃ (f : Fin m → MvPolynomial (Fin n) k), (∀ (i : Fin m), f i ∈ I) ∧ (∀ (i : Fin m), (MvPolynomial.eval x) (f i) = 0) ∧ (jacobianMatrix_P31 f x).rank = m ∧ Ideal.span (Set.range f) = I

Proposition 31 (Jacobian criterion): smoothness at x is equivalent to existence of m local generators of I with linearly independent differentials at x.