Hilbert's Nullstellensatz

TheoremVanishing ideal of a point#✓fully proved

For a point \(a \in \mathbb{C}^n\), the ideal of polynomials in \(\mathbb{C}[x_1, \ldots, x_n]\) that vanish on \(\{a\}\) equals the kernel of the evaluation homomorphism \(\mathbb{C}[x_1, \ldots, x_n] \to \mathbb{C}\), \(f \mapsto f(a)\).

theorem vanishingIdeal_singleton_eq_ker_aeval (n : ℕ) (a : Fin n → ℂ) :
    (vanishingIdeal ℂ {a} : Ideal (MvPolynomial (Fin n) ℂ)) =
      RingHom.ker (aeval a : MvPolynomial (Fin n) ℂ →ₐ[ℂ] ℂ)

Used by 1

Used byWeak Nullstellensatz, kernel form

TheoremWeak Nullstellensatz, kernel form#✓fully proved

Let \(n\) be a natural number. An ideal \(I\) of the polynomial ring \(\mathbb{C}[x_1, \ldots, x_n]\) is maximal if and only if there is a point \(a \in \mathbb{C}^n\) such that \(I\) is the kernel of the evaluation homomorphism \(\mathbb{C}[x_1, \ldots, x_n] \to \mathbb{C}\), \(f \mapsto f(a)\).

theorem isMaximal_iff_eq_ker_aeval (n : ℕ) (I : Ideal (MvPolynomial (Fin n) ℂ)) :
    I.IsMaximal ↔
      ∃ a : Fin n → ℂ, I = RingHom.ker (aeval a : MvPolynomial (Fin n) ℂ →ₐ[ℂ] ℂ)

Uses 1

Proof usesVanishing ideal of a point

TheoremWeak Nullstellensatz, quotient form#✓fully proved

Let \(P_1, \ldots, P_m\) be polynomials in \(\mathbb{C}[x_1, \ldots, x_n]\) and let \(A = \mathbb{C}[x_1, \ldots, x_n]/(P_1, \ldots, P_m)\). An ideal \(J\) of \(A\) is maximal if and only if there is a common zero \(a \in \mathbb{C}^n\) of \(P_1, \ldots, P_m\) such that \(J\) is the image in \(A\) of the ideal of polynomials vanishing at \(a\).

theorem isMaximal_quotient_iff_exists_common_zero (n m : ℕ)
    (P : Fin m → MvPolynomial (Fin n) ℂ)
    (J : Ideal (MvPolynomial (Fin n) ℂ ⧸ Ideal.span (Set.range P))) :
    J.IsMaximal ↔
      ∃ a : Fin n → ℂ, (∀ i, MvPolynomial.aeval a (P i) = 0) ∧
        J = Ideal.map (Ideal.Quotient.mk (Ideal.span (Set.range P))) (vanishingIdeal ℂ {a})

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.