Infinitude of Primes - Fürstenberg's proof

Let us have a look at Fürstenberg’s proof of the infinitude of primes. This is a fun one, deriving a contradiction from the assumption that there are only finitely many primes by defining a topology on the integers. The proof as written down by Aigner and Ziegler is slightly longer, so let us split it up into three parts.

Proof. Consider the following curious topology on the set \(\mathbb{Z}\) of integers. For \(a, b \in \mathbb{Z} \), \(b > 0\), we set \[N_{a,b} = \{a + n \, b \mid n \in \mathbb{Z} \}.\] Each set \(N_{a,b}\) is a two-way infinite arithmetic progression. Now call a set \(O ⊆ \mathbb{Z}\) open if either \(O\) is empty, or if to every \(a \in O\) there exists some \(b > 0\) with \(N_{a,b} \subseteq O\). Clearly, the union of open sets is open again. If \(O_1, O_2\) are open, and \(a \in O_1 \cap O_2\) with \(N_{a,b_1} \subseteq O_1\) and \(N_{a,b_2} \subseteq O_2\), then \(a \in N_{a, b_1 b_2}\). So we conclude that any finite intersection of open sets is again open. So, this family of open sets induces a bona fide topology on \(\mathbb{Z}\).

Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 5.

The definition of \(N_{a,b}\) is taken care of easily.

def N (a b : ℤ) : Set ℤ := { a + b * n | n : ℤ}

Before continuing and defining the topology on \(\mathbb{Z}\), let us establish some trivial but important properties of \(N_{a,b}\) that will implicitly be used later in the proof. The first states that the sets \(N_{a,b}\) are infinite and is easily proven through an injective map \(f : \mathbb{Z} \hookrightarrow N_{a,b}\).

lemma N_infinite (a b : ℤ) (h : b ≠ 0) : (N a b).Infinite := by let f (n : ℤ) : N a b := ⟨a + b * n, by simp [N]⟩ have f_inj : Function.Injective f := λ a₁ a₂ f_eq ↦ by simp [f, h] at f_eq; exact f_eq exact Set.infinite_coe_iff.mp (Infinite.of_injective f f_inj)

Next is a small but crucial statement in the form of el_N_of_dvd, that will make many arguments a lot easier: \(n\) is an element of \(N_{a,b}\) if and only if \(b ∣ (n - a)\). Note that for Lean \(0 \mid 0\). One immediate consequence of this (N_sub) states that \(N_{a, b \, m} \subseteq N_{a,b}\) for any integer \(m\).

lemma el_N_of_dvd (a b n : ℤ) : n ∈ N a b ↔ b ∣ (n - a) := by constructor <;> {intro ⟨c, _⟩; use c; linarith } lemma N_sub (a b m: ℤ) : N a (b * m) ⊆ N a b := by intro n h rw [el_N_of_dvd] at * exact Int.dvd_trans (Exists.intro m rfl) h

Let us now tackle the specified topology on \(\mathbb{Z}\). We will talk in more detail about type categories in a future post, but let us already spoil that in order to give \(\mathbb{Z}\) a topology, we need to establish that ℤ is an instance of TopologicalSpace. That means that to any lemmas that require a topological structure we will simply pass ℤ and the notion of open and closed sets will be automatically inferred from int_topology. Note that this behavior is quite similar to how we inferred the information that some natural number p is primed from a Fact; in a sense a Fact behaves like a type class with a single property.

The first thing any topological space needs is a notion of open sets, which we deliver in the form of IsOpen. The fact that ℤ itself needs to be open (isOpen_univ) was skimmed over by Aigner and Ziegler, but thankfully Lean makes relatively easy work of this.

instance int_topology : TopologicalSpace ℤ where IsOpen O := O = ∅ ∨ (∀ a : O, ∃ b, b ≠ 0 ∧ N a b ⊆ O) isOpen_univ := by simp; exact exists_ne 0

The first non-trivial property of a topological space requires that the (not necessarily finite) union of open sets is again open (isOpen_sUnion). Aigner and Ziegler take care of this through “Clearly, the union of open sets is open again”, but we don’t have that luxury. Using by_cases, we need to distinguish whether all sets are empty (which is take care of easily) or if there exists some nonempty U₀ from which we can take the set \(N_{a,b}\).

isOpen_sUnion U := by simp; intro sets_open by_cases h: ∀ s ∈ U, s = ∅ · exact Or.inl h · rw [or_iff_right h] intro a U₀ U₀_in_U a_in_U₀ specialize sets_open U₀ U₀_in_U simp [or_iff_right (Set.Nonempty.ne_empty (Exists.intro a a_in_U₀))] at sets_open obtain ⟨b, b_ne_zero, N_contained⟩ := sets_open a a_in_U₀ exact ⟨b, b_ne_zero, λ _ a ↦ Set.subset_sUnion_of_mem U₀_in_U (N_contained a)⟩

Next, a topological space requires that any intersection of two open sets is again open (isOpen_inte). Aigner and Ziegler state the following: “If \(O_1, O_2\) are open, and \(a \in O_1 \cap O_2\) with \(N_{a,b_1} \subseteq O_1\) and \(N_{a,b_2} \subseteq O_2\), then \(a \in N_{a, b_1 b_2}\).” The case where the intersection is empty was again skipped, but otherwise we proceed very much the same way by using the set \(N_{a, b_1 \, b_2}\).

isOpen_inter O₁ O₂ h₁ h₂ := by simp at * by_cases h: O₁ ∩ O₂ = ∅ · exact Or.inl h · simp [h] intro a a_in_O₁ a_in_O₂ simp [Set.Nonempty.ne_empty (Exists.intro a a_in_O₁)] at h₁ simp [Set.Nonempty.ne_empty (Exists.intro a a_in_O₂)] at h₂ obtain ⟨b₁, b₁_ne_zero, N₁_contained⟩ := h₁ a a_in_O₁ obtain ⟨b₂, b₂_ne_zero, N₂_contained⟩ := h₂ a a_in_O₂ use b₁ * b₂ have Nab1b2_su_Nab1 := N_sub a b₁ b₂ have Nab1b2_su_Nab2 := N_sub a b₂ b₁ rw [mul_comm] at Nab1b2_su_Nab2 exact ⟨mul_ne_zero b₁_ne_zero b₂_ne_zero, λ _ a => N₁_contained (Nab1b2_su_Nab1 a), λ _ a => N₂_contained (Nab1b2_su_Nab2 a)⟩

Before continuing, let es establish another trivial little fact about \(N_{a,b}\) likewise used implicitly later on, namely that it is obviously open (N_open).

lemma N_open (a b : ℤ) (h : b ≠ 0): IsOpen (N a b) := by simp [IsOpen, TopologicalSpace.IsOpen, N] apply Or.inr exact λ a' ↦ (by use b; exact ⟨h, λ a'' ↦ by use a' + a''; ring_nf⟩)

We are now ready to proceed with the second part of the proof.

Proof (Cont'd). Let us note two facts:

• (A) Any nonempty open set is infinite.
• (B) Any set \(N_{a,b}\) is closed as well.

Indeed, the first fact follows from the definition. For the second we observe \[N_{a,b} = \mathbb{Z} \setminus \bigcup_{i=1}^{b-1} N_{a+i,b},\] which proves that \(N_{a,b}\) is the complement of an open set and hence closed.

Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 5.

We will have to be slightly more explicit than “the first fact follows from the definition” when establishing our proof of (A), but we can still keep it reasonably short. Note that Set.Nonempty O is generally prefered over O ≠ ∅, but we’ll keep the later notation to make the code slightly nicer to read.

lemma A (O : Set ℤ) (h₁ : IsOpen O) (h₂ : O ≠ ∅) : O.Infinite := by simp [IsOpen, TopologicalSpace.IsOpen, h₂] at h₁ obtain ⟨a, a_in_O⟩ := (by push_neg at h₂; exact h₂) obtain ⟨b, b_ne_zero, N_su_O⟩ := h₁ a a_in_O exact Set.Infinite.mono N_su_O (N_infinite a b b_ne_zero)

Regarding statement (B), we first “observe \(N_{a,b} = \mathbb{Z} \setminus \bigcup_{i=1}^{b-1} N_{a+i,b}\) …” in the form of N_eq_Ubc; this requires a surprising amount of work. Using compl_unique we split the argument into two parts, first establishing that \(N_{a,b}\) does not intersect \(\bigcup_{i=1}^{b-1} N_{a+i,b}\) (N_disjoint) and then that together they make up \(\mathbb{Z}\) (N_covers).

lemma B (a : ℤ) (b : ℕ) (h : b > 0) : IsClosed (N a b) := by let Ub := (⋃ i : {x : ℕ // 1 ≤ x ∧ x < b}, N (a + i) b) have N_eq_Ubc : N a b = Ubᶜ := by have N_disjoint : Ub ∩ N a b = ∅ := by rw [Set.iUnion_inter]; simp intro idx idx_lw idx_up apply Set.disjoint_iff_inter_eq_empty.mp apply Set.disjoint_right.mpr intro n b_dvd b_dvd' simp [el_N_of_dvd] at b_dvd b_dvd' have b_dvd_idx : b ∣ idx := by have := Int.dvd_sub b_dvd' b_dvd; simp [Int.ofNat_dvd] at this; exact this exact (Nat.not_dvd_of_pos_of_lt idx_lw idx_up) b_dvd_idx have N_covers : Ub ∪ N a b = Set.univ := by apply Set.Subset.antisymm_iff.mpr constructor · exact λ _ _ ↦ trivial · intro n _ simp [el_N_of_dvd, Ub] let i := (n - a) % (b : ℤ) by_cases i_cases : i = 0 · exact Or.inr (Int.modEq_zero_iff_dvd.mp (i_cases)) · apply Or.inl use Int.toNat i have i_ge_0 : i ≥ 0 := Int.emod_nonneg (n - a) (Int.coe_nat_ne_zero_iff_pos.mpr h) have nat_i_ge_0 := Int.lt_toNat.mpr (Ne.lt_of_le' i_cases i_ge_0) have nat_i_lt_b := (Int.toNat_lt i_ge_0).mpr (Int.emod_lt_of_pos (n - a) (Int.ofNat_pos.mpr h)) have minus_i_dvd: (b : ℤ) ∣ (n - (a + i)) := Int.sub_sub n a i ▸ Int.dvd_sub_of_emod_eq rfl exact ⟨ ⟨nat_i_ge_0, nat_i_lt_b⟩, Int.toNat_of_nonneg i_ge_0 ▸ minus_i_dvd⟩ exact (compl_unique N_disjoint N_covers).symm

Using this, the rest of the proof is straightforward and in fact almost shorter than stating that the just established N_eq_Ubc “proves that \(N_{a,b}\) is the complement of an open set and hence closed.”

rw [N_eq_Ubc] apply isClosed_compl_iff.mpr apply isOpen_iUnion exact λ i ↦ N_open (a + i) b (Int.coe_nat_ne_zero_iff_pos.mpr h)

Finally, let’s look at the actual proof of the infinitude of primes using what we just established.

Proof (Cont'd). So far the primes have not yet entered the picture - but here they come. Since any number \(n \ne 1, −1\) has a prime divisor \(p\), and hence is contained in \(N_{0,p}\), we conclude \[\mathbb{Z} \setminus \{1, -1\} = \bigcup_{p \in \mathbb{P}} N_{0,p}.\] Now if \(\mathbb{P}\) were finite, then \(\bigcup_{p \in \mathbb{P}} N_{0,p}\) would be a finite union of closed sets (by (B)), and hence closed. Consequently, \(\{1, −1\}\) would be an open set, in violation of (A).

Aigner, M., & Ziegler, G. M. (5th ed.). Proofs from THE BOOK, p. 5.

The main goal is to establish that “\(\mathbb{Z} \setminus \{1, -1\} = \bigcup_{p \in \mathbb{P}} N_{0,p}\)”, which we do through Z_as_U. The constructor splits the equality of the two sets up into establishing that each is contained in the other. For the direction \(\subseteq\), “any number \(n \ne 1, −1\) has a prime divisor \(p\)” is taken care of by Nat.exists_prime_and_dvd.

theorem infinitude_primes : { p : ℕ | Nat.Prime p }.Infinite := by have Z_as_U : {1, -1}ᶜ = (⋃ p ∈ {p : ℕ | Nat.Prime p}, N 0 p) := by apply Set.ext; intro n constructor <;> intro n_el · obtain ⟨p, p_prime, p_dvd_n⟩ := Nat.exists_prime_and_dvd (λ c ↦ n_el (Int.natAbs_eq_iff.mp c)) have n_in_Np : n ∈ N 0 p := by simp [el_N_of_dvd]; exact Int.ofNat_dvd_left.mpr p_dvd_n simp; exact ⟨p, p_prime, n_in_Np⟩ · simp [el_N_of_dvd] at * obtain ⟨p, p_prime, p_dvd_n⟩ := n_el have p_ndvd_one := Int.ofNat_dvd.not.mpr (Prime.not_dvd_one (Nat.prime_iff.mp p_prime)) push_neg; constructor all_goals {by_contra c; rw [c, ←Nat.cast_one] at p_dvd_n ; simp [Int.dvd_neg.mpr] at p_dvd_n; exact p_ndvd_one p_dvd_n} by_contra h

Having established Z_as_U, the rest of the proof is a rather neat proof by contradiction. “if \(\mathbb{P}\) were finite, then \(\bigcup_{p \in \mathbb{P}} N_{0,p}\) would be a finite union of closed sets (by (B)), and hence closed” is taken care of by U_close and “\(\{1, −1\}\) would be an open set” by one_open. The violation of (A) comes in the form of one_infinite, which states that \(\{1, -1\}\) would need to be infinite, which is obviously not true.

by_contra h have U_close : IsClosed (⋃ p ∈ {p : ℕ | Nat.Prime p}, N 0 p) := by have (p : ℕ) (p_prime : p ∈ {p : ℕ | Nat.Prime p}) : IsClosed (N 0 p) := by simp at p_prime; exact B 0 p (Nat.Prime.pos p_prime) exact Set.Finite.isClosed_biUnion (Set.not_infinite.mp h) this have one_open : IsOpen {1, -1} := isClosed_compl_iff.mp (Z_as_U ▸ U_close) have one_infinite := A {1, -1} one_open (Set.Nonempty.ne_empty (Set.insert_nonempty 1 {-1})) exact one_infinite (Set.toFinite {1, -1})

This concludes the proof. 🎉