Documentation

TauCeti.Topology.Algebra.MvPolynomial.ZeroLocus

Zero loci of polynomials are closed #

Let K be a field with a topology in which the ring operations are continuous and points are closed, such as ℝ, ℂ or a p-adic field, and let k be a field with K a k-algebra. The common zeros in K^σ of an ideal of k[X_σ] form a closed set, since evaluating a polynomial is continuous. Consequently the topological closure of a set of points lies in its Zariski closure, the zero locus of its vanishing ideal: a polynomial identity holding on a set also holds on its closure.

The common zero set of a family of polynomials p : ι → R[X_σ] is also presented as the level set TauCeti.affineZeroLocus p of the evaluation map x ↦ (pᵢ(x))ᵢ at 0, the form on which implicit-function charts are built.

Main results #

source
theorem MvPolynomial.isClosed_zeroLocus {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] (I : Ideal (MvPolynomial σ k)) :
IsClosed (zeroLocus K I)

In a field with continuous ring operations and closed points, the common zero locus of an ideal of polynomials is closed.

source
theorem MvPolynomial.closure_subset_zeroLocus_vanishingIdeal {k : Type u_1} {K : Type u_2} {σ : Type u_3} [Field k] [Field K] [Algebra k K] [TopologicalSpace K] [IsTopologicalRing K] [T1Space K] (V : Set (σ → K)) :
closure V ⊆ zeroLocus K (vanishingIdeal k V)

In a field with continuous ring operations and closed points, the closure of a set of points lies in its Zariski closure, the zero locus of its vanishing ideal.

source
def TauCeti.affineZeroLocus {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] (p : ι → MvPolynomial σ R) :
Set (σ → R)

The common zero set in R^σ of a family of polynomials, presented as the level set of their evaluation map x ↦ (pᵢ(x))ᵢ at 0. Over a field it agrees with MvPolynomial.zeroLocus of the ideal generated by the family (TauCeti.affineZeroLocus_eq_zeroLocus); the level-set presentation is the one on which implicit-function charts are built.

Instances For
    source
    @[simp]
    theorem TauCeti.mem_affineZeroLocus {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] {p : ι → MvPolynomial σ R} {x : σ → R} :
    x ∈ affineZeroLocus p ↔ ∀ (k : ι), (MvPolynomial.eval x) (p k) = 0
    source
    theorem TauCeti.isClosed_affineZeroLocus {R : Type u_1} {σ : Type u_2} {ι : Type u_3} [CommSemiring R] [TopologicalSpace R] [IsTopologicalSemiring R] [T1Space R] (p : ι → MvPolynomial σ R) :
    IsClosed (affineZeroLocus p)

    The common zero set of a family of polynomials is closed.

    source
    theorem TauCeti.affineZeroLocus_eq_zeroLocus {K : Type u_1} {σ : Type u_2} {ι : Type u_3} [Field K] {p : ι → MvPolynomial σ K} :
    affineZeroLocus p = MvPolynomial.zeroLocus K (Ideal.span (Set.range p))

    The level-set zero locus of a family is Mathlib's zero locus of the ideal it generates.