Exercise 1.15 (Scott 1981, PRG-19, §1) — non-isomorphic "finite-only" domains

"Construct non-isomorphic infinite domains where all elements are finite but where there are no infinite chains ⟨xₙ⟩ of elements with xₙ ⊏ xₙ₊₁ for all n."

We give two neighbourhood systems over Δ = ℕ:

• flat — 𝒟 = {ℕ} ∪ {{n} ∣ n ∈ ℕ} (the flat domain). Its elements are exactly ⊥ and the pairwise-incomparable atoms ↑{n} (flat_classify), so all elements are finite/principal (flat_all_finite), every atom is maximal (flat_atom_maximal), there is no 3-chain (flat_no_three_chain) and hence no infinite ascending chain (flat_no_infinite_chain). It is infinite (flat_infinite).

• stem — 𝒟 = {ℕ, {0,1}} ∪ {{n} ∣ n ∈ ℕ} (a flat domain with one length-3 "stem"). It contains a strict 3-chain ⊥ ⊏ ↑{0,1} ⊏ ↑{0} (stem_three_chain). It too has only finite elements and no infinite ascending chain (same flat-with-stem classification; the formally decisive difference from flat is the 3-chain).

Since an order-isomorphism transports strict chains, the 3-chain in stem would force a 3-chain in flat, which has none: hence ¬ (flat ≅ᴰ stem) (not_isomorphic). Two infinite, finite-element, chain-bounded domains that are not isomorphic.

The classification results are classical (they decide whether an element contains some atom); the constructions and the non-isomorphism argument are otherwise elementary.

theorem Domain.Neighborhood.Exercise115.singleton_disjoint {n m : ℕ} (h : n ≠ m) : {n} ∩ {m} = ∅

{n} ∩ {m} = ∅ for n ≠ m.

The flat domain flat.

def Domain.Neighborhood.Exercise115.flatMem (X : Set ℕ) : Prop

Neighbourhoods of the flat domain: Δ = ℕ together with all singletons.

Equations

• Domain.Neighborhood.Exercise115.flatMem X = (X = Set.univ ∨ ∃ (n : ℕ), X = {n})

theorem Domain.Neighborhood.Exercise115.flatNOD : NestedOrDisjoint flatMem

def Domain.Neighborhood.Exercise115.flat : NeighborhoodSystem ℕ

Exercise 1.15 — the flat domain. 𝒟 = {ℕ} ∪ {{n}}.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise115.flat_mem {X : Set ℕ} : flat.mem X ↔ X = Set.univ ∨ ∃ (n : ℕ), X = {n}

@[simp]

theorem Domain.Neighborhood.Exercise115.flat_master : flat.master = Set.univ

theorem Domain.Neighborhood.Exercise115.flat_empty_not_mem : ¬flat.mem ∅

theorem Domain.Neighborhood.Exercise115.flat_mem_singleton (n : ℕ) : flat.mem {n}

The atom ↑{n} (a finite element).

theorem Domain.Neighborhood.Exercise115.flat_classify (x : flat.Element) : x = flat.bot ∨ ∃ (n : ℕ), x = flat.principal ⋯

Flat classification. Every element is ⊥ or an atom ↑{n}. Classical.

theorem Domain.Neighborhood.Exercise115.flat_atom_maximal (n : ℕ) (y : flat.Element) (hle : flat.principal ⋯ ≤ y) : y = flat.principal ⋯

Flat: every atom is maximal (total).

theorem Domain.Neighborhood.Exercise115.flat_no_three_chain : ¬∃ (a : flat.Element) (b : flat.Element) (c : flat.Element), a < b ∧ b < c

Flat has no strict 3-chain (a ⊏ b ⊏ c is impossible): ⊥ is least and atoms are maximal.

theorem Domain.Neighborhood.Exercise115.flat_no_infinite_chain : ¬∃ (f : ℕ → flat.Element), StrictMono f

Flat has no infinite ascending chain.

theorem Domain.Neighborhood.Exercise115.flat_all_finite (x : flat.Element) : ∃ (X : Set ℕ) (h : flat.mem X), x = flat.principal h

All elements of flat are finite (principal).

theorem Domain.Neighborhood.Exercise115.flat_infinite : Function.Injective fun (n : ℕ) => flat.principal ⋯

flat is infinite: the atoms ↑{n} are pairwise distinct.

The "stem" domain stem.

def Domain.Neighborhood.Exercise115.stemMem (X : Set ℕ) : Prop

Neighbourhoods of the stem domain: Δ = ℕ, the pair {0,1}, and all singletons.

Equations

• Domain.Neighborhood.Exercise115.stemMem X = (X = Set.univ ∨ X = {0, 1} ∨ ∃ (n : ℕ), X = {n})

theorem Domain.Neighborhood.Exercise115.stemNOD : NestedOrDisjoint stemMem

def Domain.Neighborhood.Exercise115.stem : NeighborhoodSystem ℕ

Exercise 1.15 — the stem domain. 𝒟 = {ℕ, {0,1}} ∪ {{n}}.

Equations

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

@[simp]

theorem Domain.Neighborhood.Exercise115.stem_mem {X : Set ℕ} : stem.mem X ↔ X = Set.univ ∨ X = {0, 1} ∨ ∃ (n : ℕ), X = {n}

theorem Domain.Neighborhood.Exercise115.stem_mem_univ : stem.mem Set.univ

theorem Domain.Neighborhood.Exercise115.stem_mem_pair : stem.mem {0, 1}

theorem Domain.Neighborhood.Exercise115.stem_mem_zero : stem.mem {0}

theorem Domain.Neighborhood.Exercise115.stem_principal_lt {X Y : Set ℕ} (hX : stem.mem X) (hY : stem.mem Y) (hYX : Y ⊆ X) (hne : X ≠ Y) : stem.principal hX < stem.principal hY

A strict step between principal filters of stem: Y ⊊ X (proper) gives ↑X ⊏ ↑Y.

theorem Domain.Neighborhood.Exercise115.stem_three_chain : ∃ (a : stem.Element) (b : stem.Element) (c : stem.Element), a < b ∧ b < c

Stem contains a strict 3-chain ⊥ = ↑ℕ ⊏ ↑{0,1} ⊏ ↑{0} — the structural feature that distinguishes it from flat.

Non-isomorphism.

theorem Domain.Neighborhood.Exercise115.not_isomorphic : ¬(flat ≅ᴰ stem)

Exercise 1.15. flat and stem are not isomorphic: an order-isomorphism would transport stem's strict 3-chain ⊥ ⊏ ↑{0,1} ⊏ ↑{0} back to a strict 3-chain in flat, which has none.