Computing the prime ideals in the ring of complex polynomials in two variables

Long winded title, couldn’t figure out how to make appear in the title. That’s the ring for which I’m going to compute all of the prime ideals. That’s useful to know because that computation gives the points of the affine scheme , the “complex affine 2-space”.

First of all, is an integral domain, hence is a prime ideal. Also, this ring is a unique factorization domain (UFD), so any irreducible polynomial is also prime, whence is a prime ideal. Finally, for any two , the ideal is maximal so a fortiori it’s prime. Intuitively, the zero is a “two-dimensional point”, the ’s are “one-dimensional points”, and the should be thought at “standard, zero-dimensional points” (i.e. closed points).

I claim that there are no prime ideals other than those I just enumerated. First, the easy case. Suppose is a principal prime ideal, i.e. it has a single generator and . Because is not the zero ideal, the element is prime, and so it is an irreducible polynomial.

Now the harder case: suppose is a prime ideal that is not principal. We want to show it is of the form for some complex numbers and . A daunting task! In fact, not so daunting. Here’s a fact that will get us started: there necessarily exists two relatively prime polynomials and in . “Relatively prime” means that any element that divides both and must be a unit, i.e. a complex number. The proof idea for this factoid is the following: choose to be any non-unit, non-zero polynomial in . Since our ring is a UFD, we may decompose into a product of irreducibles, one of which will be in . Define to be this irreducible factor lying in . Because is not principal, there must be some other polynomial in the non-empty set . Then and are relatively prime. If my proof sketch is not convincing your, here’s a proof of it in Lean 4, leveraging Mathlib; feel free to judge my programming skills.

import Mathlib.Algebra.Group.Units.Basic
import Mathlib.Algebra.Polynomial.Basic
import Mathlib.Algebra.Polynomial.Bivariate
import Mathlib.Algebra.Prime.Defs
import Mathlib.Data.Complex.Basic
import Mathlib.RingTheory.Ideal.Basic
import Mathlib.RingTheory.Ideal.IsPrincipal
import Mathlib.RingTheory.Polynomial.UniqueFactorization
import Mathlib.RingTheory.UniqueFactorizationDomain.Basic

open Polynomial Bivariate Submodule UniqueFactorizationMonoid

abbrev A := ℂ[X][Y]

lemma exists_rel_prime {I : Ideal A} (hI : I.IsPrime) (hI₂ : ¬I.IsPrincipal) : ∃ f g, f ∈ I ∧ g ∈ I ∧ IsRelPrime f g := by
  have hI₃ : I ≠ ⊥ := by
    intro h
    rw [<- Ideal.span_zero] at h
    exact hI₂ <| IsPrincipal.mk ⟨_, h⟩
  obtain ⟨f : A, hf : f ∈ I, hf₂ : Prime f⟩ := hI.exists_mem_prime_of_ne_bot hI₃
  have compl_nonempty : ((I : Set A) \ (Ideal.span { f } : Set A)).Nonempty := by
    rw [Set.nonempty_iff_ne_empty]
    intro h
    rw [Set.diff_eq_empty] at h ; norm_cast at h
    replace h : I = Ideal.span { f } := by
      apply le_antisymm h
      rwa [Ideal.span_le, Set.singleton_subset_iff]
    exact hI₂ <| IsPrincipal.mk ⟨_, h⟩
  let g : A := compl_nonempty.some
  obtain ⟨hg : g ∈ I, hg₂ : g ∉ Ideal.span { f }⟩ := compl_nonempty.some_mem
  use f, g, hf, hg
  intro d hdf hdg
  replace hf₂ : Irreducible f := irreducible_iff_prime.mpr hf₂
  by_contra h
  rw [dvd_iff_exists_eq_mul_right] at hdf
  rcases hdf with ⟨c, hc⟩
  rcases Irreducible.isUnit_or_isUnit hf₂ hc with d_unit | c_unit
  . contradiction
  have hfg : f ∣ g := by
    refine dvd_trans ?_ hdg
    rw [dvd_iff_exists_eq_mul_right, hc]
    obtain ⟨c_inv, hc_inv⟩ := c_unit.exists_right_inv
    use c_inv
    rw [mul_assoc, hc_inv, mul_one]
  rw [<- Ideal.mem_span_singleton] at hfg
  exact hg₂ hfg

Let’s continue. We have two polynomials and which are relatively prime members of , and these two polynomials continue to be relatively prime when interpreted in the larger ring , by some other post I made. It is advantageous to work in this larger setting because is an Euclidean domain, hence we may compute the greatest common divisor (GCD) of and in it. Moreover, Bézout’s Identity is verified in this setting: we have the equality of ideals , since the GCD of and is a unit by relative primality. In particular, there exists two polynomials such that . In this expression, and may contain monomials terms for which the coefficient is a fraction with some polynomial in as the denominator. We may rewrite the left hand side to put all these monomials on a common denominator, and multiply both sides by an appropriate polynomial to lift that equation to in .

The previous equation shows that lies in the ideal generated by and . In particular, lies in . Because is a non-constant, non-zero polynomial in a single variable with coefficients in , it admits at least one root such that .

We can repeat the same argument but in to find some polynomial . Therefore . But since is a maximal ideal, we must have equality!