Exercise 1.16 (Scott 1981, PRG-19, §1) — cofinite subsets of ℕ

Δ = ℕ, 𝒟 = the cofinite subsets (Xᶜ finite). This is a neighbourhood system (cofiniteSystem), closed under all finite intersections. Scott asks to show |𝒟| ≅ (𝒫(ℕ), ⊆).

The order-isomorphism cofiniteIso : |𝒟| ≃o Set ℕ sends a filter x to its set of excluded points toExcluded x = {n ∣ {n}ᶜ ∈ x}, with inverse ofExcluded E = {Y cofinite ∣ Yᶜ ⊆ E} (a filter for every E ⊆ ℕ). The key reconstruction lemma is mem_compl_of_finite: ⋂_{n∈F} {n}ᶜ = Fᶜ ∈ x for finite F of points whose single-point deletions are in x.

We also record ofExcluded_univ_isTotal / le_ofExcluded_univ — the unique total element is the ⊑-top ofExcluded ℕ (= all of 𝒟), matching the greatest element ℕ ∈ 𝒫(ℕ) — and fullSystem, a second system (all subsets) closed under finite intersection.

mem_compl_of_finite uses Set.Finite.induction_on (and Set.Finite is classical), so the classification lemmas are not choice-free; the constructions (ofExcluded, cofiniteSystem) are [propext, Quot.sound].

def Domain.Neighborhood.Cofinite.cofiniteSystem : NeighborhoodSystem ℕ

Exercise 1.16 — the cofinite neighbourhood system on ℕ. X ∈ 𝒟 iff Xᶜ finite; closed under finite intersection since (X∩Y)ᶜ = Xᶜ ∪ Yᶜ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Domain.Neighborhood.Cofinite.cofiniteSystem_mem {X : Set ℕ} : cofiniteSystem.mem X ↔ Xᶜ.Finite

def Domain.Neighborhood.Cofinite.ofExcluded (E : Set ℕ) : cofiniteSystem.Element

The filter generated by an arbitrary set E ⊆ ℕ of "excluded points": ofExcluded E = {Y cofinite ∣ Yᶜ ⊆ E}. This is a filter for every E.

Equations

• Domain.Neighborhood.Cofinite.ofExcluded E = { mem := fun (Y : Set ℕ) => Yᶜ.Finite ∧ Yᶜ ⊆ E, sub := ⋯, master_mem := ⋯, inter_mem := ⋯, up_mem := ⋯ }

@[simp]

theorem Domain.Neighborhood.Cofinite.mem_ofExcluded {E Y : Set ℕ} : (ofExcluded E).mem Y ↔ Yᶜ.Finite ∧ Yᶜ ⊆ E

def Domain.Neighborhood.Cofinite.toExcluded (x : cofiniteSystem.Element) : Set ℕ

The set of points excluded by a filter x: toExcluded x = {n ∣ {n}ᶜ ∈ x}.

Equations

• Domain.Neighborhood.Cofinite.toExcluded x = {n : ℕ | x.mem {n}ᶜ}

@[simp]

theorem Domain.Neighborhood.Cofinite.mem_toExcluded {x : cofiniteSystem.Element} {n : ℕ} : n ∈ toExcluded x ↔ x.mem {n}ᶜ

theorem Domain.Neighborhood.Cofinite.mem_compl_singleton (n : ℕ) : cofiniteSystem.mem {n}ᶜ

Each {n}ᶜ is a neighbourhood (its complement {n} is finite).

theorem Domain.Neighborhood.Cofinite.mem_compl_of_finite (x : cofiniteSystem.Element) {F : Set ℕ} (hF : F.Finite) : (∀ n ∈ F, x.mem {n}ᶜ) → x.mem Fᶜ

Reconstruction lemma. For finite F of points each of whose single-deletion {n}ᶜ is in the filter x, the intersection ⋂_{n∈F} {n}ᶜ = Fᶜ is also in x.

theorem Domain.Neighborhood.Cofinite.subset_compl_singleton {Y : Set ℕ} {n : ℕ} (hn : n ∈ Yᶜ) : Y ⊆ {n}ᶜ

For n ∉ Y, the neighbourhood Y is contained in {n}ᶜ.

theorem Domain.Neighborhood.Cofinite.toExcluded_ofExcluded (E : Set ℕ) : toExcluded (ofExcluded E) = E

theorem Domain.Neighborhood.Cofinite.ofExcluded_toExcluded (x : cofiniteSystem.Element) : ofExcluded (toExcluded x) = x

def Domain.Neighborhood.Cofinite.cofiniteIso : cofiniteSystem.Element ≃o Set ℕ

Exercise 1.16 — |𝒟| ≅ (𝒫(ℕ), ⊆). The filter x corresponds to its excluded-point set toExcluded x; inclusion of filters matches inclusion of excluded sets.

Equations

• One or more equations did not get rendered due to their size.

Total elements.

theorem Domain.Neighborhood.Cofinite.le_ofExcluded_univ (x : cofiniteSystem.Element) : x ≤ ofExcluded Set.univ

Every filter is ⊑ ofExcluded ℕ (the whole family 𝒟; every cofinite Y has Yᶜ ⊆ ℕ).

theorem Domain.Neighborhood.Cofinite.ofExcluded_univ_isTotal : cofiniteSystem.IsTotal (ofExcluded Set.univ)

Exercise 1.16 — the unique total element. ofExcluded ℕ (matching the greatest element ℕ ∈ 𝒫(ℕ)) is total: it is ⊑-maximal.

A second ∩-closed system: all subsets.

def Domain.Neighborhood.Cofinite.fullSystem : NeighborhoodSystem ℕ

Exercise 1.16 (second example). All subsets of ℕ form a neighbourhood system, trivially closed under all finite intersections. Unlike cofiniteSystem it is not positive (∅ is a neighbourhood). Every neighbourhood is a finite element via principal; its total elements are the principal filters of singletons (the system is "flat").

Equations

• Domain.Neighborhood.Cofinite.fullSystem = { mem := fun (x : Set ℕ) => True, master := Set.univ, master_mem := trivial, inter_mem := ⋯, sub_master := ⋯ }