theorem gc_zeroLocus_vanishingIdeal (R : Type u_1) [CommSemiring R] : GaloisConnection (fun (I : Ideal R) => PrimeSpectrum.zeroLocus ↑I) fun (t : (Set (PrimeSpectrum R))ᵒᵈ) => PrimeSpectrum.vanishingIdeal t

The fundamental Galois connection (Thm 1.2, Lec 1) between ideals of R and closed subsets of Spec R, given by zeroLocus ⊣ vanishingIdeal.

theorem abstract_nullstellensatz (R : Type u_1) [CommSemiring R] (I : Ideal R) : PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I) = I.radical

Abstract Nullstellensatz on Spec R: the vanishing ideal of the zero locus of I is the radical of I.

theorem vanishingIdeal_zeroLocus_of_isRadical (R : Type u_1) [CommSemiring R] (I : Ideal R) (hI : I.IsRadical) : PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑I) = I

For a radical ideal I, the vanishing ideal of its zero locus recovers I itself — half of the radical-ideal correspondence (Thm 1.2).

theorem zeroLocus_vanishingIdeal_eq_closure (R : Type u_1) [CommSemiring R] (t : Set (PrimeSpectrum R)) : PrimeSpectrum.zeroLocus ↑(PrimeSpectrum.vanishingIdeal t) = closure t

The zero locus of the vanishing ideal of t recovers the closure of t in the Zariski topology of Spec R.

theorem zeroLocus_eq_iff_radical_eq (R : Type u_1) [CommSemiring R] {I J : Ideal R} : PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑J ↔ I.radical = J.radical

Two ideals have the same zero locus iff they share the same radical, the order-theoretic injectivity statement of Thm 1.2.

theorem isRadical_vanishingIdeal (R : Type u_1) [CommSemiring R] (s : Set (PrimeSpectrum R)) : (PrimeSpectrum.vanishingIdeal s).IsRadical

The vanishing ideal of any subset of Spec R is always a radical ideal.

def closedsEmbedding (R : Type u_1) [CommSemiring R] : (TopologicalSpace.Closeds (PrimeSpectrum R))ᵒᵈ ↪o Ideal R

The order-embedding closeds(Spec R) ↪ Ideal R provided by the radical ideal correspondence (Thm 1.2), packaged as an OrderEmbedding.

theorem nullstellensatz_galois_connection {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} : GaloisConnection (MvPolynomial.zeroLocus K) (MvPolynomial.vanishingIdeal k)

The classical Galois connection between ideals of k[X_σ] and subsets of K^σ, given by zeroLocus ⊣ vanishingIdeal.

theorem nullstellensatz {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] (I : Ideal (MvPolynomial σ k)) : MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K I) = I.radical

Hilbert's Nullstellensatz: over an algebraically closed field K and a finite-variable polynomial ring, I(V(I)) = √I.

theorem nullstellensatz_prime {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] (P : Ideal (MvPolynomial σ k)) [hP : P.IsPrime] : MvPolynomial.vanishingIdeal k (MvPolynomial.zeroLocus K P) = P

Specialization of the Nullstellensatz to prime ideals: I(V(P)) = P for any prime ideal P (since prime implies radical).

theorem weak_nullstellensatz {k : Type u_1} {K : Type u_2} [Field k] [Field K] [Algebra k K] {σ : Type u_3} [IsAlgClosed K] [Finite σ] {I : Ideal (MvPolynomial σ k)} (hI : I.IsMaximal) : ∃ (x : σ → K), I = MvPolynomial.vanishingIdeal k {x}

Weak Nullstellensatz: maximal ideals of k[X_σ] correspond to single points in K^σ when K/k is algebraically closed.

theorem irreducible_zeroLocus_iff_prime {R : Type u_1} [CommSemiring R] (I : Ideal R) : IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.radical.IsPrime

The zero locus of I is irreducible iff √I is a prime ideal — the irreducible-closed-subset / prime-ideal correspondence.

theorem irreducible_zeroLocus_iff_prime_of_radical {R : Type u_1} [CommSemiring R] (I : Ideal R) (hI : I.IsRadical) : IsIrreducible (PrimeSpectrum.zeroLocus ↑I) ↔ I.IsPrime

For a radical ideal I, irreducibility of V(I) is equivalent to I being prime.

theorem isIrreducible_iff_vanishingIdeal_isPrime {R : Type u_1} [CommSemiring R] {s : Set (PrimeSpectrum R)} : IsIrreducible s ↔ (PrimeSpectrum.vanishingIdeal s).IsPrime

A subset of Spec R is irreducible iff its vanishing ideal is prime.

theorem vanishingIdeal_irreducible_eq_primes {R : Type u_1} [CommSemiring R] : PrimeSpectrum.vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsIrreducible s} = {P : Ideal R | P.IsPrime}

The image of irreducible subsets of Spec R under the vanishing-ideal map is exactly the set of prime ideals.

theorem vanishingIdeal_closed_irreducible_eq_primes {R : Type u_1} [CommSemiring R] : PrimeSpectrum.vanishingIdeal '' {s : Set (PrimeSpectrum R) | IsClosed s ∧ IsIrreducible s} = {P : Ideal R | P.IsPrime}

The vanishing-ideal map restricted to closed irreducible subsets gives a bijection onto the prime ideals (a refinement of Thm 1.2 to irreducibles).

theorem specIrreducible_iff_isPrime_nilradical {R : Type u_1} [CommSemiring R] : IrreducibleSpace (PrimeSpectrum R) ↔ (nilradical R).IsPrime

Spec R is irreducible iff the nilradical of R is prime — equivalent to having a unique minimal prime.

theorem specIrreducible_iff_isDomain {R : Type u_1} [CommRing R] [IsReduced R] : IrreducibleSpace (PrimeSpectrum R) ↔ IsDomain R

For a reduced ring, Spec R is irreducible iff R is an integral domain.

theorem specIrreducible_of_isDomain {R : Type u_1} [CommRing R] [IsDomain R] : IrreducibleSpace (PrimeSpectrum R)

For an integral domain R, the prime spectrum Spec R is irreducible.

theorem radical_eq_sInf_primes {R : Type u_1} [CommSemiring R] (I : Ideal R) : I.radical = sInf {J : Ideal R | I ≤ J ∧ J.IsPrime}

The radical of I equals the infimum of all primes containing I.

theorem radical_eq_sInf_minimalPrimes {R : Type u_1} [CommSemiring R] (I : Ideal R) : I.radical = sInf I.minimalPrimes

Sharper form: the radical equals the infimum of I.minimalPrimes.

theorem finite_minimalPrimes_of_noetherian {R : Type u_1} [CommSemiring R] [IsNoetherianRing R] (I : Ideal R) : I.minimalPrimes.Finite

In a Noetherian ring, every ideal has only finitely many minimal primes.

theorem radical_eq_finite_iInf_primes {R : Type u_1} [CommSemiring R] [IsNoetherianRing R] (I : Ideal R) : ∃ (S : Finset (Ideal R)), (∀ J ∈ S, J.IsPrime) ∧ I.radical = S.inf id

In a Noetherian ring, the radical of any ideal is a finite intersection of prime ideals — the basis of primary decomposition.

theorem isRadical_eq_finite_iInf_primes {R : Type u_1} [CommSemiring R] [IsNoetherianRing R] (I : Ideal R) (hI : I.IsRadical) : ∃ (S : Finset (Ideal R)), (∀ J ∈ S, J.IsPrime) ∧ I = S.inf id

In a Noetherian ring, a radical ideal is itself a finite intersection of primes, recovering its primary decomposition with no embedded components.

theorem finite_minimalPrimes_of_noetherian_ring {R : Type u_1} [CommSemiring R] [IsNoetherianRing R] : (minimalPrimes R).Finite

In a Noetherian ring, the set of global minimal primes is finite.