Fields of definition of algebraic sets

DefinitionIdeal over \(k\) of a subset of affine space#✓fully proved

Let \(k\) be a field with algebraic closure \(\bar k\), and let \(Z \subseteq \bar k^n\). The ideal \(I_k(Z)\) of \(k[X_1, \dots, X_n]\) consists of the polynomials \(f\) with coefficients in \(k\) whose image in \(\bar k[X_1, \dots, X_n]\) vanishes at every point of \(Z\); that is, \(I_k(Z)\) is the preimage of the vanishing ideal of \(Z\) in \(\bar k[X_1, \dots, X_n]\) under the coefficient map \(k[X_1, \dots, X_n] \to \bar k[X_1, \dots, X_n]\).

noncomputable def idealOverK {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) :
    Ideal (MvPolynomial (Fin n) k) :=
  Ideal.comap (MvPolynomial.map (algebraMap k (AlgebraicClosure k)))
    (MvPolynomial.vanishingIdeal (AlgebraicClosure k) Z)

Used by 6

Used byPolynomials in the ideal over \(k\) vanish on the set · The ideal over \(k\) reverses inclusions · The ideal over \(k\) of the empty set · Sets defined over \(k\) · Defined over \(k\) as an equality of ideals · Membership in the ideal over \(k\)

TheoremMembership in the ideal over \(k\)#✓fully proved

Let \(k\) be a field with algebraic closure \(\bar k\), let \(Z \subseteq \bar k^n\), and let \(f \in k[X_1, \dots, X_n]\). Then \(f\) lies in the ideal \(I_k(Z)\) over \(k\) of \(Z\) if and only if the image of \(f\) in \(\bar k[X_1, \dots, X_n]\) under the coefficient map lies in the vanishing ideal of \(Z\), that is, vanishes at every point of \(Z\).

theorem mem_idealOverK_iff {n : ℕ} {Z : Set (Fin n → AlgebraicClosure k)}
    {f : MvPolynomial (Fin n) k} :
    f ∈ idealOverK Z ↔
      MvPolynomial.map (algebraMap k (AlgebraicClosure k)) f ∈
        MvPolynomial.vanishingIdeal (AlgebraicClosure k) Z

Uses 1 · Used by 1

Statement usesIdeal over \(k\) of a subset of affine space

Used byPolynomials in the ideal over \(k\) vanish on the set

DefinitionSets defined over \(k\)#✓fully proved

Let \(k\) be a field with algebraic closure \(\bar k\), let \(Z \subseteq \bar k^n\), and let \(I_k(Z)\) be the ideal of polynomials in \(k[X_1, \dots, X_n]\) whose image in \(\bar k[X_1, \dots, X_n]\) vanishes at every point of \(Z\). The set \(Z\) is defined over \(k\) if the vanishing ideal of \(Z\) in \(\bar k[X_1, \dots, X_n]\) equals the ideal generated by the image of \(I_k(Z)\) under the coefficient map \(k[X_1, \dots, X_n] \to \bar k[X_1, \dots, X_n]\).

def IsDefinedOver {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) : Prop :=
  MvPolynomial.vanishingIdeal (AlgebraicClosure k) Z =
    Ideal.map (MvPolynomial.map (algebraMap k (AlgebraicClosure k)))
      (idealOverK Z)

Uses 1 · Used by 1

Statement usesIdeal over \(k\) of a subset of affine space

Used byDefined over \(k\) as an equality of ideals

TheoremDefined over \(k\) as an equality of ideals#✓fully proved

Let \(k\) be a field with algebraic closure \(\bar k\) and let \(Z \subseteq \bar k^n\). Then \(Z\) is defined over \(k\) if and only if the vanishing ideal of \(Z\) in \(\bar k[X_1, \dots, X_n]\) equals the ideal generated by the image of \(I_k(Z)\) under the coefficient map \(k[X_1, \dots, X_n] \to \bar k[X_1, \dots, X_n]\).

theorem isDefinedOver_iff {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) :
    IsDefinedOver Z ↔
      MvPolynomial.vanishingIdeal (AlgebraicClosure k) Z =
        Ideal.map (MvPolynomial.map (algebraMap k (AlgebraicClosure k)))
          (idealOverK Z)

Uses 2

Statement usesSets defined over \(k\) · Ideal over \(k\) of a subset of affine space

TheoremPolynomials in the ideal over \(k\) vanish on the set#✓fully proved

Let \(k\) be a field with algebraic closure \(\bar k\), let \(Z \subseteq \bar k^n\), and let \(f \in I_k(Z)\). Then for every point \(P \in Z\), the image of \(f\) in \(\bar k[X_1, \dots, X_n]\) evaluated at \(P\) is \(0\).

theorem eval_of_mem_idealOverK {n : ℕ} {Z : Set (Fin n → AlgebraicClosure k)}
    {f : MvPolynomial (Fin n) k} (hf : f ∈ idealOverK Z)
    {P : Fin n → AlgebraicClosure k} (hP : P ∈ Z) :
    MvPolynomial.eval P
      (MvPolynomial.map (algebraMap k (AlgebraicClosure k)) f) = 0

Uses 2

Statement usesIdeal over \(k\) of a subset of affine space

Proof usesMembership in the ideal over \(k\)

TheoremThe ideal over \(k\) of the empty set#✓fully proved

Let \(k\) be a field with algebraic closure \(\bar k\). For every \(n\), the ideal \(I_k(\emptyset)\) of the empty subset of \(\bar k^n\) is all of \(k[X_1, \dots, X_n]\).

theorem idealOverK_empty (n : ℕ) :
    idealOverK (∅ : Set (Fin n → AlgebraicClosure k)) = ⊤

Uses 1

Statement usesIdeal over \(k\) of a subset of affine space

TheoremThe ideal over \(k\) reverses inclusions#✓fully proved

Let \(k\) be a field with algebraic closure \(\bar k\). If \(Z_1 \subseteq Z_2 \subseteq \bar k^n\), then \(I_k(Z_2) \subseteq I_k(Z_1)\).

theorem idealOverK_anti_mono {n : ℕ} {Z₁ Z₂ : Set (Fin n → AlgebraicClosure k)}
    (h : Z₁ ⊆ Z₂) : idealOverK Z₂ ≤ idealOverK Z₁

Uses 1

Statement usesIdeal over \(k\) of a subset of affine space

7 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.