Exercise 6.28 (Scott 1981, PRG-19, §6) — Plotkin's finite

Cantor–Schröder–Bernstein

EXERCISE 6.28. (Suggested by G. Plotkin). Show that if 𝒟 and ℰ are finite systems and 𝒟 ⊴ ℰ ⊴ 𝒟, then 𝒟 ≅ ℰ. Need the same be true of infinite systems?

Here ⊴ is Scott's embeds-as-a-subdomain relation of Lemma 6.15: D ⊴ E means D ≅ᴰ D' for some subdomain D' ◁ E.

The argument

The whole proof rests on a single observation: D ⊴ E already supplies an order embedding of element domains |D| ↪o |E| (Trianglelefteq.elementEmbedding). Indeed, unfolding ⊴ gives an order isomorphism e : |D| ≃o |D'| onto a subdomain D' ◁ E, and Proposition 6.12 turns D' ◁ E into a projection pair i : D' → E, j : E → D' with j ∘ i = I. The element-wise map i(·) is then an order embedding (projElementEmbedding): it is monotone (toElementMap_mono), and j(·) is a monotone left inverse, so i(a) ⊑ i(b) → j(i(a)) ⊑ j(i(b)) → a ⊑ b. Compose with e.

For finite domains, mutual order embeddings force an isomorphism (orderIso_of_embeddings): each embedding is injective, so the two finite element types have equal cardinality, whence either embedding is a bijection — a surjective strictly-monotone map, i.e. an order isomorphism. This is the finite Cantor–Schröder–Bernstein, and it is exactly what Plotkin's hint exploits. (The retraction structure of ⊴ is stronger than a mere embedding, but the proof only needs the embedding.)

"Finite system" is read faithfully as finitely many neighbourhoods (NeighborhoodSystem.IsFinite); this yields Finite |D| (finite_element_of_isFinite) because a filter is pinned down by which of the finitely many neighbourhoods it contains.

Need the same be true of infinite systems? No. Plotkin's hint is the finite cardinality count above; it has no infinite analogue. Mutual retracts of dcpos need not be isomorphic — the analogue of Cantor–Schröder–Bernstein fails for the retraction preorder once the domains are infinite (a Eilenberg-swindle-style obstruction). Only the finite statement is formalized here; the infinite counterexample is recorded as prose, outside this file's scope.

Everything is choice-free at the relational core (projElementEmbedding, elementEmbedding audit to {propext, Quot.sound}); the finite count (orderIso_of_embeddings, hence the main theorems) uses Classical.choice — genuinely unavoidable, as it extracts a Fintype from Finite and a surjection's section.

An order embedding |D| ↪o |E| from a projection pair / from ⊴

def Domain.Neighborhood.projElementEmbedding {α : Type u_3} {β : Type u_4} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (i : ApproximableMap D E) (j : ApproximableMap E D) (hji : j.comp i = ApproximableMap.idMap D) : D.Element ↪o E.Element

The element-wise map of an injection i is an order embedding. Given approximable maps i : D → E, j : E → D with j ∘ i = I_D, the map x ↦ i(x) on elements is an order embedding |D| ↪o |E|: monotone by toElementMap_mono, and order-reflecting because j(·) is a monotone left inverse (j(i(x)) = x). Choice-free.

Equations

• Domain.Neighborhood.projElementEmbedding i j hji = OrderEmbedding.ofMapLEIff i.toElementMap ⋯

theorem Domain.Neighborhood.Trianglelefteq.elementEmbedding {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (h : D ⊴ E) : Nonempty (D.Element ↪o E.Element)

D ⊴ E yields an order embedding |D| ↪o |E|. Unfold ⊴ to an iso |D| ≅o |D'| onto a subdomain D' ◁ E, turn D' ◁ E into Proposition 6.12's projection pair, and compose its injection embedding with the iso. Choice-free.

Finite Cantor–Schröder–Bernstein for ordered types

theorem Domain.Neighborhood.orderIso_of_embeddings {P : Type u_3} {Q : Type u_4} [PartialOrder P] [PartialOrder Q] [Finite P] [Finite Q] (f : P ↪o Q) (g : Q ↪o P) : Nonempty (P ≃o Q)

Finite Cantor–Schröder–Bernstein (order version). Mutual order embeddings between two finite ordered types yield an order isomorphism. The embeddings are injective, so equal finite cardinality forces f to be surjective; a surjective strictly-monotone map is an order iso. Uses Classical.choice (via Fintype/surjection-section).

Exercise 6.28 — the finite statement

theorem Domain.Neighborhood.isomorphic_of_trianglelefteq_both {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} [Finite D.Element] [Finite E.Element] (h₁ : D ⊴ E) (h₂ : E ⊴ D) : D ≅ᴰ E

Exercise 6.28 (core). If |D| and |E| are finite and D ⊴ E ⊴ D, then D ≅ᴰ E. The two ⊴s give mutual order embeddings of the (finite) element domains, and orderIso_of_embeddings upgrades them to an isomorphism.

"Finite system" = finitely many neighbourhoods

def Domain.Neighborhood.NeighborhoodSystem.IsFinite {α : Type u_3} (D : NeighborhoodSystem α) : Prop

A neighbourhood system is finite when it has only finitely many neighbourhoods.

Equations

• D.IsFinite = Finite { X : Set α // D.mem X }

theorem Domain.Neighborhood.finite_element_of_isFinite {α : Type u_3} {D : NeighborhoodSystem α} (h : D.IsFinite) : Finite D.Element

A finite system has a finite element domain. A filter x : |D| is determined by which of the (finitely many) neighbourhoods it contains, so x ↦ {p | x.mem p.1} injects |D| into the finite powerset Set {X // D.mem X}.

theorem Domain.Neighborhood.isomorphic_of_finite_system {α : Type u_1} {β : Type u_2} {D : NeighborhoodSystem α} {E : NeighborhoodSystem β} (hD : D.IsFinite) (hE : E.IsFinite) (h₁ : D ⊴ E) (h₂ : E ⊴ D) : D ≅ᴰ E

Exercise 6.28 (Scott 1981, PRG-19; suggested by G. Plotkin). If 𝒟 and ℰ are finite neighbourhood systems with 𝒟 ⊴ ℰ and ℰ ⊴ 𝒟, then 𝒟 ≅ ℰ.