@[reducible, inline]

abbrev AffineSpace_k (k : Type u_1) [Field k] (n : ℕ) : Type u_1

Affine $n$-space over $k$, defined as $\overline{k}^n$, i.e. tuples in the algebraic closure.

def LRationalPoints (k : Type u_1) [Field k] (n : ℕ) (L : IntermediateField k (AlgebraicClosure k)) : Set (AffineSpace_k k n)

The set of $L$-rational points in affine $n$-space: tuples all of whose coordinates lie in the intermediate field $L \subseteq \overline{k}$.

@[implicit_reducible]

noncomputable instance galoisActionAffineSpace (k : Type u_1) [Field k] (n : ℕ) : MulAction Gal(AlgebraicClosure k/k) (AffineSpace_k k n)

The natural action of the absolute Galois group $\mathrm{Gal}(\overline{k}/k)$ on affine $n$-space by coordinate-wise application.

def galoisFixedPoints (k : Type u_1) [Field k] (n : ℕ) (L : IntermediateField k (AlgebraicClosure k)) : Set (AffineSpace_k k n)

The set of points in $\overline{k}^n$ fixed by every element of the Galois group fixing the intermediate field $L$ (the Galois-theoretic characterization of $L$-rational points).

def AlgebraicSet (k : Type u_1) [Field k] (n : ℕ) (S : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) : Set (AffineSpace_k k n)

The algebraic set $V(S)$ in $\overline{k}^n$ cut out by a set $S$ of polynomials over $\overline{k}$, i.e. the common zero locus.

def AlgebraicSetLRational (k : Type u_1) [Field k] (n : ℕ) (S : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) (L : IntermediateField k (AlgebraicClosure k)) : Set (AffineSpace_k k n)

The $L$-rational points of the algebraic set $V(S)$: zeros of $S$ with all coordinates in the intermediate field $L$.

def AlgebraicSetSingleton (k : Type u_1) [Field k] (n : ℕ) (f : MvPolynomial (Fin n) (AlgebraicClosure k)) : Set (AffineSpace_k k n)

The hypersurface $V(f) = \{P : f(P) = 0\}$ cut out by a single polynomial $f$.

theorem eval_eq_aeval_algebraicClosure (k : Type u_1) [Field k] {n : ℕ} (P : AffineSpace_k k n) (f : MvPolynomial (Fin n) (AlgebraicClosure k)) : (MvPolynomial.eval P) f = (MvPolynomial.aeval P) f

For polynomials over $\overline{k}$, the ring-evaluation MvPolynomial.eval agrees with the algebra-evaluation MvPolynomial.aeval.

theorem algebraicSet_ideal_eq_zeroLocus (k : Type u_1) [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) (AlgebraicClosure k))) : AlgebraicSet k n ↑I = MvPolynomial.zeroLocus (AlgebraicClosure k) I

The algebraic set cut out by an ideal $I \subseteq \overline{k}[x_1, \ldots, x_n]$ is the same as the Mathlib zeroLocus of $I$.

theorem weak_nullstellensatz (k : Type u_1) [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) (AlgebraicClosure k))) (hI : I ≠ ⊤) : (AlgebraicSet k n ↑I).Nonempty

Weak Nullstellensatz: every proper ideal $I \subsetneq \overline{k}[x_1, \ldots, x_n]$ has a common zero in $\overline{k}^n$.

theorem Definition1213.radical_eq_setOf_pow_mem {R : Type u_2} [CommRing R] (I : Ideal R) : ↑I.radical = {x : R | ∃ (r : ℕ), 0 < r ∧ x ^ r ∈ I}

The radical $\sqrt{I}$ of an ideal $I$ equals $\{x : R \mid \exists r > 0, x^r \in I\}$, matching the textbook definition.

theorem Lemma1214.radical_is_ideal {R : Type u_2} [CommRing R] (I : Ideal R) : ∃ (J : Ideal R), ↑J = {x : R | ∃ (n : ℕ), x ^ n ∈ I}

Lemma 12.14: the set $\{x : \exists n, x^n \in I\}$ is an ideal (namely $\sqrt{I}$).

def IsAlgebraicSubset (k : Type u_1) [Field k] (n : ℕ) (V : Set (AffineSpace_k k n)) : Prop

A subset $V \subseteq \overline{k}^n$ is an algebraic subset if it equals $V(S)$ for some set $S$ of polynomials.

theorem algebraicSet_isAlgebraicSubset (k : Type u_1) [Field k] {n : ℕ} (S : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) : IsAlgebraicSubset k n (AlgebraicSet k n S)

The zero set $V(S)$ is, trivially, an algebraic subset.

def IsIrreducibleAlgebraicSet (k : Type u_1) [Field k] (n : ℕ) (V : Set (AffineSpace_k k n)) : Prop

An algebraic set $V$ is irreducible if it is nonempty and whenever $V = V_1 \cup V_2$ with each $V_i$ algebraic, one of the $V_i$ equals $V$.

theorem IsIrreducibleAlgebraicSet.nonempty (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (h : IsIrreducibleAlgebraicSet k n V) : V.Nonempty

An irreducible algebraic set is nonempty by definition.

theorem isNoetherianRing_iff_every_ideal_fg (R : Type u_2) [CommRing R] : IsNoetherianRing R ↔ ∀ (I : Ideal R), I.FG

A ring is Noetherian iff every ideal is finitely generated.

theorem isNoetherianRing_iff_ideal_acc (R : Type u_2) [CommRing R] : IsNoetherianRing R ↔ ∀ (f : ℕ →o Ideal R), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m

A ring is Noetherian iff every ascending chain of ideals stabilizes.

theorem noetherian_fg_iff_acc (R : Type u_2) [CommRing R] : (∀ (I : Ideal R), I.FG) ↔ ∀ (f : ℕ →o Ideal R), ∃ (n : ℕ), ∀ (m : ℕ), n ≤ m → f n = f m

Combining the previous two: every ideal is finitely generated iff every ascending chain stabilizes.

theorem hilbert_basis_theorem (R : Type u_2) [CommRing R] [IsNoetherianRing R] : IsNoetherianRing (Polynomial R)

Hilbert basis theorem: if $R$ is Noetherian, then $R[X]$ is Noetherian.

def idealOfAlgebraicSet {k : Type u_1} [Field k] {σ : Type u_2} (Z : Set (σ → k)) : Ideal (MvPolynomial σ k)

The vanishing ideal $I(Z)$ of a subset $Z \subseteq k^\sigma$: polynomials in $k[x_\sigma]$ that vanish on every point of $Z$.

@[simp]

theorem mem_idealOfAlgebraicSet_iff {k : Type u_1} [Field k] {σ : Type u_2} {Z : Set (σ → k)} {f : MvPolynomial σ k} : f ∈ idealOfAlgebraicSet Z ↔ ∀ P ∈ Z, (MvPolynomial.eval P) f = 0

Membership in $I(Z)$ unfolds to vanishing of $f$ at every point of $Z$.

theorem idealOfAlgebraicSet_eq_vanishingIdeal {k : Type u_1} [Field k] {σ : Type u_2} (Z : Set (σ → k)) : idealOfAlgebraicSet Z = MvPolynomial.vanishingIdeal k Z

The textbook vanishing ideal idealOfAlgebraicSet matches Mathlib's MvPolynomial.vanishingIdeal.

theorem idealOfAlgebraicSet_anti_mono {k : Type u_1} [Field k] {σ : Type u_2} {Y Z : Set (σ → k)} (h : Y ⊆ Z) : idealOfAlgebraicSet Z ≤ idealOfAlgebraicSet Y

Antitone: $Y \subseteq Z$ implies $I(Z) \subseteq I(Y)$.

theorem idealOfAlgebraicSet_union {k : Type u_1} [Field k] {σ : Type u_2} (Y Z : Set (σ → k)) : idealOfAlgebraicSet (Y ∪ Z) = idealOfAlgebraicSet Y ⊓ idealOfAlgebraicSet Z

$I(Y \cup Z) = I(Y) \cap I(Z)$.

theorem hilbert_nullstellensatz (k : Type u_1) [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) (AlgebraicClosure k))) : idealOfAlgebraicSet (AlgebraicSet k n ↑I) = I.radical

Hilbert's Nullstellensatz: for any ideal $I$ in $\overline{k}[x_1, \ldots, x_n]$, $I(V(I)) = \sqrt{I}$.

theorem eval_surjective_algebraicClosure (k : Type u_1) [Field k] {n : ℕ} (P : Fin n → AlgebraicClosure k) : Function.Surjective ⇑(MvPolynomial.eval P)

Evaluation at a point $P$ is a surjective ring homomorphism $\overline{k}[x_1, \ldots, x_n] \to \overline{k}$.

theorem ker_eval_eq_vanishingIdeal_singleton (k : Type u_1) [Field k] {n : ℕ} (P : Fin n → AlgebraicClosure k) : RingHom.ker (MvPolynomial.eval P) = MvPolynomial.vanishingIdeal (AlgebraicClosure k) {P}

The kernel of evaluation at $P$ equals the vanishing ideal of the singleton $\{P\}$.

theorem vanishingIdeal_singleton_isMaximal (k : Type u_1) [Field k] {n : ℕ} (P : Fin n → AlgebraicClosure k) : (MvPolynomial.vanishingIdeal (AlgebraicClosure k) {P}).IsMaximal

The vanishing ideal $I(\{P\})$ of a single point in $\overline{k}^n$ is maximal.

theorem maximal_ideal_eq_vanishingIdeal_singleton (k : Type u_1) [Field k] {n : ℕ} (m : Ideal (MvPolynomial (Fin n) (AlgebraicClosure k))) (hm : m.IsMaximal) : ∃ (P : Fin n → AlgebraicClosure k), m = MvPolynomial.vanishingIdeal (AlgebraicClosure k) {P}

Every maximal ideal of $\overline{k}[x_1, \ldots, x_n]$ has the form $I(\{P\})$ for some $P \in \overline{k}^n$ (one direction of Corollary 12.17).

theorem corollary_12_17 (k : Type u_1) [Field k] {n : ℕ} {m : Ideal (MvPolynomial (Fin n) (AlgebraicClosure k))} : m.IsMaximal ↔ ∃ (P : Fin n → AlgebraicClosure k), m = MvPolynomial.vanishingIdeal (AlgebraicClosure k) {P}

Corollary 12.17: an ideal of $\overline{k}[x_1, \ldots, x_n]$ is maximal iff it is the vanishing ideal of a single point.

noncomputable def idealOverK {k : Type u_1} [Field k] {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) : Ideal (MvPolynomial (Fin n) k)

The ideal $I_k(Z) \subseteq k[x_1, \ldots, x_n]$ of polynomials over $k$ vanishing on $Z$, obtained by pulling back $I(Z)$ along the scalar extension map.

theorem mem_idealOverK_iff {k : Type u_1} [Field k] {n : ℕ} {Z : Set (Fin n → AlgebraicClosure k)} {f : MvPolynomial (Fin n) k} : f ∈ idealOverK Z ↔ (MvPolynomial.map (algebraMap k (AlgebraicClosure k))) f ∈ idealOfAlgebraicSet Z

$f \in I_k(Z)$ iff its image in $\overline{k}[x_1, \ldots, x_n]$ vanishes on $Z$.

def IsDefinedOver {k : Type u_1} [Field k] {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) : Prop

A subset $Z \subseteq \overline{k}^n$ is defined over $k$ if its vanishing ideal $I(Z)$ is the extension to $\overline{k}$ of $I_k(Z)$.

noncomputable def AffineCoordinateRing {k : Type u_1} [Field k] {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) : Type u_1

The affine coordinate ring $k[Z] = k[x_1, \ldots, x_n] / I_k(Z)$ over the base field.

def AffineCoordinateRingBar {k : Type u_1} [Field k] {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) : Type u_1

The affine coordinate ring $\overline{k}[Z] = \overline{k}[x_1, \ldots, x_n] / I(Z)$ over the algebraic closure.

@[implicit_reducible]

noncomputable instance instCommRingAffineCoordinateRing {k : Type u_1} [Field k] {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) : CommRing (AffineCoordinateRing Z)

The affine coordinate ring $k[Z]$ inherits a commutative ring structure from the quotient.

@[implicit_reducible]

noncomputable instance instCommRingAffineCoordinateRingBar {k : Type u_1} [Field k] {n : ℕ} (Z : Set (Fin n → AlgebraicClosure k)) : CommRing (AffineCoordinateRingBar Z)

The affine coordinate ring $\overline{k}[Z]$ inherits a commutative ring structure from the quotient.

theorem algebraicSet_idealOfAlgebraicSet_eq (k : Type u_1) [Field k] {n : ℕ} (S : Set (MvPolynomial (Fin n) (AlgebraicClosure k))) : AlgebraicSet k n ↑(idealOfAlgebraicSet (AlgebraicSet k n S)) = AlgebraicSet k n S

Closure-like idempotence: $V(I(V(S))) = V(S)$ for any set of polynomials $S$.

theorem algebraicSet_idealOfAlgebraicSet_of_isAlgebraicSubset (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (hV : IsAlgebraicSubset k n V) : AlgebraicSet k n ↑(idealOfAlgebraicSet V) = V

For an algebraic subset $V$, $V(I(V)) = V$.

theorem isIrreducibleAlgebraicSet_iff_isPrime (k : Type u_1) [Field k] {n : ℕ} {V : Set (AffineSpace_k k n)} (hV : IsAlgebraicSubset k n V) : IsIrreducibleAlgebraicSet k n V ↔ (idealOfAlgebraicSet V).IsPrime

Theorem 12.21: an algebraic subset $V$ is irreducible iff $I(V)$ is a prime ideal.

theorem idealOfAlgebraicSet_isRadical (k : Type u_1) [Field k] {n : ℕ} (V : Set (AffineSpace_k k n)) : (idealOfAlgebraicSet V).IsRadical

The vanishing ideal $I(V)$ of any subset $V$ is always a radical ideal.

theorem idealOfAlgebraicSet_algebraicSet_of_isRadical (k : Type u_1) [Field k] {n : ℕ} (I : Ideal (MvPolynomial (Fin n) (AlgebraicClosure k))) (hI : I.IsRadical) : idealOfAlgebraicSet (AlgebraicSet k n ↑I) = I

If $I$ is radical, then $I(V(I)) = I$ (consequence of the Nullstellensatz).

noncomputable def radicalIdealAlgebraicSetEquiv (k : Type u_1) [Field k] {n : ℕ} : { I : Ideal (MvPolynomial (Fin n) (AlgebraicClosure k)) // I.IsRadical } ≃ { V : Set (AffineSpace_k k n) // IsAlgebraicSubset k n V }

Corollary 12.18: the Nullstellensatz bijection between radical ideals of $\overline{k}[x_1, \ldots, x_n]$ and algebraic subsets of $\overline{k}^n$.