theorem isGalois_iff_normal_and_separable {k : Type u_4} {L : Type u_5} [Field k] [Field L] [Algebra k L] : IsGalois k L ↔ Normal k L ∧ Algebra.IsSeparable k L

Galois-equivalence formulation matching Definition 4.40: an algebraic extension L/k is Galois iff it is both normal and separable.

def affineSpace (σ : Type u_4) (K : Type u_5) [Field K] : Set (σ → K)

The n-dimensional affine space over K indexed by σ, defined as the full set of σ-tuples of elements of K. This is the underlying set of 𝔸_k^n from Definition 4.41.

@[simp]

theorem affineSpace_eq_univ {K : Type u_2} [Field K] {σ : Type u_3} : affineSpace σ K = Set.univ

Unfolding lemma: affine space is by definition the whole σ → K.

def affineRationalPoints {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (σ : Type u_4) (L : IntermediateField k K) : Set (σ → K)

The set of L-rational points of affine space: tuples whose every coordinate lies in the intermediate field L. This corresponds to 𝔸^n(L) from Definition 4.41.

@[simp]

theorem mem_affineRationalPoints_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} (L : IntermediateField k K) (x : σ → K) : x ∈ affineRationalPoints σ L ↔ ∀ (i : σ), x i ∈ L

A tuple is L-rational iff each of its coordinates lies in L.

def affineGaloisFixedPoints {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] (σ : Type u_4) (L : IntermediateField k K) : Set (σ → K)

Galois-fixed points in affine space: tuples fixed by every element of the Galois group fixing L. By the Galois correspondence (cf. Definition 4.41), these coincide with L-rational points when K/k is Galois.

@[simp]

theorem mem_affineGaloisFixedPoints_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} (L : IntermediateField k K) (x : σ → K) : x ∈ affineGaloisFixedPoints σ L ↔ ∀ φ ∈ L.fixingSubgroup, φ • x = x

Characterization of Galois-fixed points: a tuple x is fixed iff every L-fixing automorphism φ of K acts trivially on x.

theorem affineRationalPoints_subset_galoisFixedPoints {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} (L : IntermediateField k K) : affineRationalPoints σ L ⊆ affineGaloisFixedPoints σ L

Every L-rational point is fixed by the subgroup of automorphisms of K/k fixing L.

theorem galoisFixedPoints_subset_affineRationalPoints {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsGalois k K] (L : IntermediateField k K) : affineGaloisFixedPoints σ L ⊆ affineRationalPoints σ L

Converse of affineRationalPoints_subset_galoisFixedPoints: when K/k is Galois, a tuple fixed by all L-fixing automorphisms must be L-rational.

def zeroLocusOfSet {σ : Type u_3} (K : Type u_4) [Field K] (S : Set (MvPolynomial σ K)) : Set (σ → K)

The zero locus Z_S of a set S of polynomials, defined as the zero locus of the ideal generated by S. This matches Definition 4.42.

@[simp]

theorem mem_zeroLocusOfSet_iff {K : Type u_2} [Field K] {σ : Type u_3} (S : Set (MvPolynomial σ K)) (x : σ → K) : x ∈ zeroLocusOfSet K S ↔ ∀ p ∈ S, (MvPolynomial.aeval x) p = 0

Membership in Z_S is equivalent to all polynomials in S vanishing at the point.

theorem zeroLocusOfSet_eq {K : Type u_2} [Field K] {σ : Type u_3} (S : Set (MvPolynomial σ K)) : zeroLocusOfSet K S = {x : σ → K | ∀ p ∈ S, (MvPolynomial.aeval x) p = 0}

Set-builder form of zeroLocusOfSet.

def lRationalPoints {k : Type u_1} [Field k] {σ : Type u_3} (K : Type u_4) [Field K] [Algebra k K] (S : Set (MvPolynomial σ K)) (L : IntermediateField k K) : Set (σ → K)

The set of L-rational points on the algebraic set cut out by S: points lying in the zero locus and having all coordinates in L. This is Z_S(L) from Definition 4.42.

@[simp]

theorem mem_lRationalPoints_iff {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} (S : Set (MvPolynomial σ K)) (L : IntermediateField k K) (x : σ → K) : x ∈ lRationalPoints K S L ↔ (∀ f ∈ S, (MvPolynomial.aeval x) f = 0) ∧ ∀ (i : σ), x i ∈ L

Membership in lRationalPoints: vanishing of all polynomials in S plus all coordinates in L.

def IsAffineAlgebraicSet {σ : Type u_3} (K : Type u_4) [Field K] (V : Set (σ → K)) : Prop

An (affine) algebraic set is a set of the form Z(I) for some ideal I ⊆ K[x₁, …, xₙ]. Corresponds to the notion from Definition 4.42.

theorem isAffineAlgebraicSet_zeroLocus {K : Type u_2} [Field K] {σ : Type u_3} (I : Ideal (MvPolynomial σ K)) : IsAffineAlgebraicSet K (MvPolynomial.zeroLocus K I)

The zero locus of any ideal is an algebraic set, by definition.

theorem isAffineAlgebraicSet_empty {K : Type u_2} [Field K] {σ : Type u_3} : IsAffineAlgebraicSet K ∅

The empty set is an algebraic set, realized as the zero locus of the unit ideal.

def IsIrreducibleAffineAlgebraicSet {σ : Type u_3} (K : Type u_4) [Field K] (V : Set (σ → K)) : Prop

An algebraic set is irreducible if it is nonempty and cannot be written as the union of two strictly smaller algebraic sets. This is Definition 4.54.

def IsAffineVariety {σ : Type u_3} (K : Type u_4) [Field K] (V : Set (σ → K)) : Prop

An affine variety is an irreducible affine algebraic set.

def vanishingIdealOfSet {σ : Type u_3} (K : Type u_4) [Field K] (V : Set (σ → K)) : Ideal (MvPolynomial σ K)

The vanishing ideal I(V) of a set of points: all polynomials that vanish identically on V. This is Definition 4.46.

@[simp]

theorem mem_vanishingIdealOfSet_iff {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) (f : MvPolynomial σ K) : f ∈ vanishingIdealOfSet K V ↔ ∀ x ∈ V, (MvPolynomial.aeval x) f = 0

A polynomial lies in I(V) iff it vanishes at every point of V.

theorem vanishingIdealOfSet_eq {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) : ↑(vanishingIdealOfSet K V) = {f : MvPolynomial σ K | ∀ x ∈ V, (MvPolynomial.aeval x) f = 0}

Set-builder form of vanishingIdealOfSet.

@[reducible, inline]

abbrev coordinateRing (K : Type u_4) [Field K] (σ : Type u_5) (V : Set (σ → K)) : Type (max u_4 u_5)

The coordinate ring of an algebraic set V: the quotient of the polynomial ring by the vanishing ideal I(V).

theorem coordinateRing_eq {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) : coordinateRing K σ V = (MvPolynomial σ K ⧸ MvPolynomial.vanishingIdeal K V)

Unfolding the definition of coordinateRing in terms of vanishingIdeal.

noncomputable def coordinateRing.mk {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) : MvPolynomial σ K →+* coordinateRing K σ V

The canonical quotient map K[x₁, …, xₙ] → K[V] from the polynomial ring to the coordinate ring of V.

structure HomogeneousRationalFunction (k : Type u_4) [CommRing k] (f : MvPolynomial (Fin 3) k) : Type u_4

A representation of a homogeneous rational function on the projective curve defined by f: a numerator and denominator, both homogeneous of the same degree, with the denominator not in the ideal (f).

• num : MvPolynomial (Fin 3) k
• den : MvPolynomial (Fin 3) k
• deg : ℕ
• num_homogeneous : self.num.IsHomogeneous self.deg
• den_homogeneous : self.den.IsHomogeneous self.deg
• den_not_in_ideal : self.den ∉ Ideal.span {f}

def HomogeneousRationalFunction.Equiv (k : Type u_4) [CommRing k] (f : MvPolynomial (Fin 3) k) : HomogeneousRationalFunction k f → HomogeneousRationalFunction k f → Prop

The equivalence relation on HomogeneousRationalFunctions used to define the function field of a projective curve: p₁ ∼ p₂ iff p₁.num * p₂.den - p₂.num * p₁.den ∈ (f).

def projectiveFunctionFieldSetoid {k : Type u_4} [Field k] (f : MvPolynomial (Fin 3) k) [Fact (Irreducible f)] : Setoid (HomogeneousRationalFunction k f)

The setoid on HomogeneousRationalFunctions built from Equiv. Reflexivity, symmetry, and transitivity use that (f) is a prime ideal (since f is irreducible), so denominators behave well.

def functionField (k : Type u_4) [Field k] (f : MvPolynomial (Fin 3) k) [Fact (Irreducible f)] : Type u_4

The function field of the projective curve cut out by an irreducible f ∈ k[x, y, z]: the quotient of homogeneous rational functions by the equivalence relation projectiveFunctionFieldSetoid f.

def functionField.mk {k : Type u_4} [Field k] {f : MvPolynomial (Fin 3) k} [Fact (Irreducible f)] (p : HomogeneousRationalFunction k f) : functionField k f

The canonical map sending a homogeneous rational function to its class in the function field.

instance homogeneousIdeal_isPrime {k : Type u_4} [Field k] (f : MvPolynomial (Fin 3) k) [Fact (Irreducible f)] : (Ideal.span {f}).IsPrime

The ideal (f) generated by an irreducible polynomial f ∈ k[x, y, z] is prime.

@[reducible, inline]

abbrev functionFieldFrac (k : Type u_4) [Field k] (f : MvPolynomial (Fin 3) k) [Fact (Irreducible f)] : Type u_4

An alternative model of the function field of Z(f) as the fraction field of the quotient ring k[x, y, z] / (f).

@[reducible, inline]

abbrev affineFunctionField (K : Type u_4) [Field K] (σ : Type u_5) (V : Set (σ → K)) : Type (max u_5 u_4)

The affine function field of an affine algebraic set V: the fraction field of its coordinate ring K[V].

instance coordinateRing.isDomain_of_prime {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) [(vanishingIdealOfSet K V).IsPrime] : IsDomain (coordinateRing K σ V)

When I(V) is prime, the coordinate ring K[V] is an integral domain.

@[implicit_reducible]

noncomputable instance affineFunctionField.field_of_prime {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) [(vanishingIdealOfSet K V).IsPrime] : Field (affineFunctionField K σ V)

When I(V) is prime, the affine function field of V is genuinely a field (it is the fraction field of an integral domain).

noncomputable def affineFunctionField.ofCoordinateRing {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) : coordinateRing K σ V →+* affineFunctionField K σ V

The canonical embedding of the coordinate ring K[V] into its fraction field, the affine function field of V.

noncomputable def varietyDimension (k : Type u_4) [Field k] (K : Type u_5) [Field K] [Algebra k K] (σ : Type u_6) (V : Set (σ → K)) [(vanishingIdealOfSet K V).IsPrime] : Cardinal.{max u_6 u_5}

The dimension of an affine variety V over k: the transcendence degree over k of its affine function field. This realizes Definition 4.35 specialized to affine varieties.

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

A ring is noetherian iff every ideal is finitely generated. Matches Definition 4.44.

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

Hilbert's basis theorem (Theorem 4.45): if R is noetherian, so is R[x].

theorem radical_eq_setOf {R : Type u_4} [CommSemiring R] (I : Ideal R) : ↑I.radical = {f : R | ∃ (n : ℕ), 0 < n ∧ f ^ n ∈ I}

Explicit set-theoretic description of the radical √I of an ideal I: those f such that some positive power f^n lies in I. Matches Definition 4.47.

theorem radical_is_ideal {R : Type u_4} [CommSemiring R] (I : Ideal R) : ∃ (J : Ideal R), ↑J = {f : R | ∃ (n : ℕ), f ^ n ∈ I}

Lemma 4.48: √I is an ideal — exhibited here by giving the witness ideal I.radical.

theorem vanishingIdealOfSet_isRadical {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) : (vanishingIdealOfSet K V).IsRadical

The vanishing ideal I(V) of any set V ⊆ 𝔸^n is radical.

theorem isAffineAlgebraicSet_union {K : Type u_2} [Field K] {σ : Type u_3} {V₁ V₂ : Set (σ → K)} (h₁ : IsAffineAlgebraicSet K V₁) (h₂ : IsAffineAlgebraicSet K V₂) : IsAffineAlgebraicSet K (V₁ ∪ V₂)

The union of two algebraic sets is algebraic, realized via the intersection of their defining ideals.

theorem isAffineAlgebraicSet_sInter {K : Type u_2} [Field K] {σ : Type u_3} (A : Set (Set (σ → K))) (hA : ∀ V ∈ A, IsAffineAlgebraicSet K V) : IsAffineAlgebraicSet K (⋂₀ A)

An arbitrary intersection of algebraic sets is algebraic, realized via the supremum of the corresponding ideals.

@[reducible]

def zariskiTopology (K : Type u_4) [Field K] (σ : Type u_5) : TopologicalSpace (σ → K)

The Zariski topology on σ → K: closed sets are exactly the affine algebraic sets, with closure under empty, arbitrary intersection, and finite unions.

theorem hilberts_nullstellensatz {K : Type u_4} [Field K] [IsAlgClosed K] {σ : Type u_5} [Finite σ] (I : Ideal (MvPolynomial σ K)) : vanishingIdealOfSet K (MvPolynomial.zeroLocus K I) = I.radical

Hilbert's Nullstellensatz (Theorem 4.49): over an algebraically closed field K, for every ideal I ⊆ K[x₁, …, xₙ] we have I(Z(I)) = √I.

theorem vanishingIdealOfSet_zeroLocus_of_radical {K : Type u_4} [Field K] [IsAlgClosed K] {σ : Type u_5} [Finite σ] (I : Ideal (MvPolynomial σ K)) (hI : I.IsRadical) : vanishingIdealOfSet K (MvPolynomial.zeroLocus K I) = I

For radical ideals I, the Nullstellensatz simplifies to I(Z(I)) = I.

theorem zeroLocus_vanishingIdealOfSet_of_algebraicSet {K : Type u_4} [Field K] [IsAlgClosed K] {σ : Type u_5} [Finite σ] (V : Set (σ → K)) (hV : IsAffineAlgebraicSet K V) : MvPolynomial.zeroLocus K (vanishingIdealOfSet K V) = V

For algebraic sets V, the Nullstellensatz says Z(I(V)) = V.

theorem ideal_variety_injective_sets {K : Type u_4} [Field K] [IsAlgClosed K] {σ : Type u_5} [Finite σ] {V W : Set (σ → K)} (hV : IsAffineAlgebraicSet K V) (hW : IsAffineAlgebraicSet K W) (h : vanishingIdealOfSet K V = vanishingIdealOfSet K W) : V = W

Injectivity half of the algebraic-set / radical-ideal correspondence (Corollary 4.52): two algebraic sets with the same vanishing ideal are equal.

theorem weak_nullstellensatz_iff {K : Type u_4} [Field K] [IsAlgClosed K] {σ : Type u_5} [Finite σ] (I : Ideal (MvPolynomial σ K)) : MvPolynomial.zeroLocus K I = ∅ ↔ I = ⊤

Iff-form of the weak Nullstellensatz: the zero locus of I is empty iff I is the unit ideal.

theorem weak_nullstellensatz {K : Type u_4} [Field K] [IsAlgClosed K] {σ : Type u_5} [Finite σ] (I : Ideal (MvPolynomial σ K)) (hI : I ≠ ⊤) : (MvPolynomial.zeroLocus K I).Nonempty

Theorem 4.50 (weak Nullstellensatz): a proper ideal of K[x₁, …, xₙ] over an algebraically closed K has nonempty zero locus.

theorem vanishingIdealOfSet_union {K : Type u_2} [Field K] {σ : Type u_3} (V₁ V₂ : Set (σ → K)) : vanishingIdealOfSet K (V₁ ∪ V₂) = vanishingIdealOfSet K V₁ ⊓ vanishingIdealOfSet K V₂

The vanishing ideal of a union of two sets equals the intersection of their vanishing ideals.

theorem isAffineAlgebraicSet_inter_zeroLocus_singleton {K : Type u_2} [Field K] {σ : Type u_3} (V : Set (σ → K)) (f : MvPolynomial σ K) (hV : IsAffineAlgebraicSet K V) : IsAffineAlgebraicSet K (V ∩ {x : σ → K | (MvPolynomial.aeval x) f = 0})

The intersection of an algebraic set V with the zero locus of a single polynomial f is again an algebraic set, realized by the ideal I + (f).

theorem zeroLocus_vanishingIdealOfSet_zeroLocus {K : Type u_2} [Field K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] (J : Ideal (MvPolynomial σ K)) : MvPolynomial.zeroLocus K (vanishingIdealOfSet K (MvPolynomial.zeroLocus K J)) = MvPolynomial.zeroLocus K J

Idempotence of the Z ∘ I operation on zero loci: Z(I(Z(J))) = Z(J). This follows from the Nullstellensatz applied to the radical of J.

theorem IsIrreducibleAffineAlgebraicSet.vanishingIdeal_isPrime {K : Type u_2} [Field K] {σ : Type u_3} {V : Set (σ → K)} (hIrr : IsIrreducibleAffineAlgebraicSet K V) : (vanishingIdealOfSet K V).IsPrime

One direction of Theorem 4.55: if V is an irreducible algebraic set, then its vanishing ideal I(V) is prime.

theorem prime_vanishingIdeal_implies_irreducible {K : Type u_2} [Field K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] {V : Set (σ → K)} (hAlg : IsAffineAlgebraicSet K V) (hPrime : (vanishingIdealOfSet K V).IsPrime) : IsIrreducibleAffineAlgebraicSet K V

Other direction of Theorem 4.55: an algebraic set whose vanishing ideal is prime is irreducible.

theorem algebraicSet_irreducible_iff_prime {K : Type u_2} [Field K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] {V : Set (σ → K)} (hAlg : IsAffineAlgebraicSet K V) : IsIrreducibleAffineAlgebraicSet K V ↔ (vanishingIdealOfSet K V).IsPrime

Theorem 4.55 (combined form): for an algebraic set V, irreducibility is equivalent to primality of its vanishing ideal.

def IsPoint {σ : Type u_3} (K : Type u_4) [Field K] (V : Set (σ → K)) : Prop

Predicate saying that an algebraic set consists of a single point.

theorem isAffineAlgebraicSet_singleton {K : Type u_2} [Field K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] (P : σ → K) : IsAffineAlgebraicSet K {P}

Every singleton {P} ⊆ 𝔸^n over an algebraically closed field is an algebraic set, realized as the zero locus of its vanishing ideal (generated by x_i - P_i).

theorem vanishingIdealOfSet_singleton_isMaximal {K : Type u_2} [Field K] {σ : Type u_3} (P : σ → K) : (vanishingIdealOfSet K {P}).IsMaximal

The vanishing ideal of a single point P is maximal: it is the maximal ideal m_P = (x_1 - P_1, …, x_n - P_n) from Corollary 4.51.

theorem maximal_iff_vanishingIdealOfSet_singleton {K : Type u_2} [Field K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] (I : Ideal (MvPolynomial σ K)) : I.IsMaximal ↔ ∃ (P : σ → K), I = vanishingIdealOfSet K {P}

Corollary 4.51: over an algebraically closed field with finitely many variables, every maximal ideal of K[x₁, …, xₙ] is of the form m_P for a unique point P.

theorem transcendence_bases_same_cardinality {k : Type u} {L : Type v} [Field k] [Field L] [Algebra k L] {ι ι' : Type w} {x : ι → L} {y : ι' → L} (hx : IsTranscendenceBasis k x) (hy : IsTranscendenceBasis k y) : Cardinal.mk ι = Cardinal.mk ι'

Theorem 4.34: any two transcendence bases of a field extension L/k have the same cardinality.

theorem perfectField_iff_perfectRing (k : Type u_1) [Field k] (p : ℕ) [ExpChar k p] : PerfectField k ↔ PerfectRing k p

For a field k of exponential characteristic p, being a perfect field (Definition 4.38) is equivalent to being a perfect ring with respect to p.