MvPolynomial.vanishingIdeal_zeroLocus_eq_radical
theorem MvPolynomial.vanishingIdeal_zeroLocus_eq_radical :
∀ {k : Type u_1} [inst : Field k] {σ : Type u_2} [inst_1 : IsAlgClosed k] [inst_2 : Finite σ]
(I : Ideal (MvPolynomial σ k)), MvPolynomial.vanishingIdeal (MvPolynomial.zeroLocus I) = I.radical
This theorem is a formalization of the main statement of Hilbert's Nullstellensatz for multivariate polynomials. It states that for any field `k` that is algebraically closed and any finite type `σ`, given an ideal `I` of multivariate polynomials with coefficients in `k` and variables indexed by `σ`, the vanishing ideal of the zero locus of `I` is equal to the radical of `I`. In other words, the set of common zeros of all polynomials in `I` perfectly determines the radical of `I`, which consists of all polynomials whose all powers are in `I`. This is a deep result linking algebra and geometry, underpinning many aspects of algebraic geometry.
More concisely: For any algebraically closed field `k` and finite type `σ`, the radical of an ideal `I` of multivariate polynomials with coefficients in `k` equals the ideal of polynomials vanishing on the zero locus of `I`.
|
MvPolynomial.le_vanishingIdeal_zeroLocus
theorem MvPolynomial.le_vanishingIdeal_zeroLocus :
∀ {k : Type u_1} [inst : Field k] {σ : Type u_2} (I : Ideal (MvPolynomial σ k)),
I ≤ MvPolynomial.vanishingIdeal (MvPolynomial.zeroLocus I)
This theorem states that for any field `k` and any type `σ`, given an ideal `I` in the ring of multivariate polynomials with coefficients in `k` and variables indexed by `σ`, `I` is a subset of the vanishing ideal of the zero locus of `I`. In plain terms, every polynomial in the ideal `I` vanishes at all points of the set, which is the zero locus of `I`. The zero locus of `I` is the set of all points where every polynomial in `I` evaluates to zero. The vanishing ideal of a set, on the other hand, is the ideal consisting of all polynomials that vanish at every point of the set.
More concisely: For any field `k` and type `σ`, the ideal `I` of multivariate polynomials with coefficients in `k` and variables indexed by `σ` is contained in the vanishing ideal of its zero locus.
|
MvPolynomial.vanishingIdeal_anti_mono
theorem MvPolynomial.vanishingIdeal_anti_mono :
∀ {k : Type u_1} [inst : Field k] {σ : Type u_2} {A B : Set (σ → k)},
A ≤ B → MvPolynomial.vanishingIdeal B ≤ MvPolynomial.vanishingIdeal A
This theorem states that for any field `k` and any type `σ`, given two sets `A` and `B` of functions from `σ` to `k`, if `A` is a subset of `B` then the vanishing ideal of `B` is a subset of the vanishing ideal of `A`. In terms of mathematical language, if all elements of `A` are also in `B` then all polynomials that vanish at every point in `B` also vanish at every point in `A`. This is a statement about the anti-monotonicity of the vanishing ideal operation: increasing the set of zeroes decreases the set of polynomials that vanish at those points.
More concisely: If `A` is a subset of `B` in the category of sets of functions from a type `σ` to a field `k`, then the vanishing ideal of `B` is contained in the vanishing ideal of `A`.
|