Exercise 6.29 (Scott 1981, PRG-19, §6) — infinitary sum and product

EXERCISE 6.29. Generalize + and × to infinitary operations on domains: ∑_{n=0}^∞ D_n and ∏_{n=0}^∞ D_n. Would a similar generalization be possible for ⊕ and ⊗?

We work with an arbitrary index type ι and a family of neighbourhood systems D : ∀ i, 𝒟ᵢ over token types α i (Scott's D_n, with ℕ the intended ι). Tokens of the combined systems live in Σ i, α i (for product-like operations) or Option (Σ i, α i) (for sum-like operations, the none being the fresh basepoint). This is the indexed analogue of the abstract binary prod/sum over α ⊕ β / Option (α ⊕ β).

The four operations and the answer

• ∏_i D_i (iprod) — the indexed product. A neighbourhood is a tuple X i ∈ 𝒟ᵢ that is the master in all but finitely many coordinates (a cylinder). The finite-support condition is essential: it is exactly what makes the compact elements of the product the finitely-presented ones, giving the headline result iprodEquiv : |∏_i D_i| ≃o ∀ i, |D_i| (the product order is pointwise) — the infinitary Proposition 3.2.
• ∑_i D_i (isum) — the indexed separated sum. A neighbourhood is the basepoint master or a single tagged copy inj i X of one summand (finite information — only one coordinate is constrained), so no finite-support condition is needed. Element trichotomy isum_trichotomy: every element is ⊥ or lives in exactly one summand.
• ⊕_i D_i (ioplus) — the indexed coalesced sum, as ∑ but with the improper tagged copies deleted (the bottoms identified). Single-coordinate, so it generalizes fine.
• ⊗_i D_i (iotimes) — the indexed smash product. A proper neighbourhood would need every coordinate proper (≠ master), which over an infinite ι contradicts finite support. So the infinite smash degenerates: iotimes_only_master/iotimes_subsingleton — over an infinite index it has only the basepoint, a one-point domain.

Answer to Scott's question. +, ×, ⊕ all generalize to infinitary operations; ⊗ does not — the infinite smash collapses to the trivial domain.

Choice discipline. Every data construction is choice-free (iprod, isum, ioplus, iotimes, the order iso iprodEquiv, and isum_summand_unique all have #print axioms ⊆ {propext, Quot.sound}). The finite-support predicate is a List of coordinates in its positive form ∀ i, i ∉ l → X i = master, which keeps intersection (FinSupp.inter) and the reconstruction (z_mem_of_slices) constructive. Only two genuinely classical Prop-level results remain: isum_trichotomy (an excluded-middle case split on whether an element reaches a summand) and the degeneracy iotimes_only_master/iotimes_subsingleton (a cardinality argument through Mathlib's classical Set.Finite). Both are flagged in their docstrings.

The product neighbourhood and its algebra

def Domain.Neighborhood.Exercise629.iprodNbhd {ι : Type u} {α : ι → Type v} (X : (i : ι) → Set (α i)) : Set ((i : ι) × α i)

A product neighbourhood iprodNbhd X = {⟨i, a⟩ ∣ a ∈ X i} over Σ i, α i.

Equations

• Domain.Neighborhood.Exercise629.iprodNbhd X = {p : (i : ι) × α i | p.snd ∈ X p.fst}

@[simp]

theorem Domain.Neighborhood.Exercise629.mem_iprodNbhd {ι : Type u} {α : ι → Type v} {X : (i : ι) → Set (α i)} {i : ι} {a : α i} : ⟨i, a⟩ ∈ iprodNbhd X ↔ a ∈ X i

theorem Domain.Neighborhood.Exercise629.iprodNbhd_inter {ι : Type u} {α : ι → Type v} (X X' : (i : ι) → Set (α i)) : iprodNbhd X ∩ iprodNbhd X' = iprodNbhd fun (i : ι) => X i ∩ X' i

Product neighbourhoods intersect coordinatewise (Scott's (2)).

theorem Domain.Neighborhood.Exercise629.iprodNbhd_subset_iff {ι : Type u} {α : ι → Type v} {X X' : (i : ι) → Set (α i)} : iprodNbhd X ⊆ iprodNbhd X' ↔ ∀ (i : ι), X i ⊆ X' i

Inclusion of product neighbourhoods is coordinatewise (Scott's (1)).

theorem Domain.Neighborhood.Exercise629.iprodNbhd_injective {ι : Type u} {α : ι → Type v} {X X' : (i : ι) → Set (α i)} (h : iprodNbhd X = iprodNbhd X') : X = X'

The tuple representation of a product neighbourhood is unique.

def Domain.Neighborhood.Exercise629.FinSupp {ι : Type u} {α : ι → Type v} (D : (i : ι) → NeighborhoodSystem (α i)) (X : (i : ι) → Set (α i)) : Prop

Choice-free finite support: a list enumerating all coordinates where X is non-master. (Mathlib's Set.Finite is built on Fintype and pulls in Classical.choice; a List witness keeps the construction constructive, which is exactly what is needed for the cylinder.)

Equations

• Domain.Neighborhood.Exercise629.FinSupp D X = ∃ (l : List ι), ∀ i ∉ l, X i = (D i).master

theorem Domain.Neighborhood.Exercise629.FinSupp.master {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} : FinSupp D fun (i : ι) => (D i).master

theorem Domain.Neighborhood.Exercise629.FinSupp.inter {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} {X X' : (i : ι) → Set (α i)} (hX : FinSupp D X) (hX' : FinSupp D X') : FinSupp D fun (i : ι) => X i ∩ X' i

def Domain.Neighborhood.Exercise629.iprod {ι : Type u} {α : ι → Type v} (D : (i : ι) → NeighborhoodSystem (α i)) : NeighborhoodSystem ((i : ι) × α i)

Exercise 6.29 — the indexed product ∏_i D_i. Neighbourhoods are cylinders: tuples X i ∈ 𝒟ᵢ that are the master in all but finitely many coordinates.

Equations

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

theorem Domain.Neighborhood.Exercise629.iprod_mem_iprodNbhd {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} {X : (i : ι) → Set (α i)} (hX : ∀ (i : ι), (D i).mem (X i)) (hXf : FinSupp D X) : (iprod D).mem (iprodNbhd X)

The element isomorphism |∏_i D_i| ≃o ∀ i, |D_i|

Throughout we use the slices slice i U — the cylinder that is U at coordinate i and the master elsewhere.

def Domain.Neighborhood.Exercise629.updTuple {ι : Type u} {α : ι → Type v} [DecidableEq ι] (D : (i : ι) → NeighborhoodSystem (α i)) (i : ι) (U : Set (α i)) (j : ι) : Set (α j)

The tuple that is U at coordinate i and the master elsewhere.

Equations

• Domain.Neighborhood.Exercise629.updTuple D i U = Function.update (fun (j : ι) => (D j).master) i U

@[simp]

theorem Domain.Neighborhood.Exercise629.updTuple_apply_self {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (i : ι) (U : Set (α i)) : updTuple D i U i = U

theorem Domain.Neighborhood.Exercise629.updTuple_apply_ne {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] {i j : ι} (U : Set (α i)) (h : j ≠ i) : updTuple D i U j = (D j).master

def Domain.Neighborhood.Exercise629.slice {ι : Type u} {α : ι → Type v} [DecidableEq ι] (D : (i : ι) → NeighborhoodSystem (α i)) (i : ι) (U : Set (α i)) : Set ((i : ι) × α i)

The slice cylinder: U at coordinate i, master elsewhere.

Equations

• Domain.Neighborhood.Exercise629.slice D i U = Domain.Neighborhood.Exercise629.iprodNbhd (Domain.Neighborhood.Exercise629.updTuple D i U)

theorem Domain.Neighborhood.Exercise629.slice_eq {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (i : ι) (U : Set (α i)) : slice D i U = iprodNbhd (updTuple D i U)

theorem Domain.Neighborhood.Exercise629.iprod_mem_slice {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] {i : ι} {U : Set (α i)} (hU : (D i).mem U) : (iprod D).mem (slice D i U)

A slice has support ⊆ {i}, hence is a neighbourhood of the product when U ∈ 𝒟ᵢ.

theorem Domain.Neighborhood.Exercise629.iprod_mem_slice_inv {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] {i : ι} {U : Set (α i)} (h : (iprod D).mem (slice D i U)) : (D i).mem U

Recovering the coordinate from a slice neighbourhood.

theorem Domain.Neighborhood.Exercise629.slice_inter {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (i : ι) (U U' : Set (α i)) : slice D i U ∩ slice D i U' = slice D i (U ∩ U')

Slices at the same coordinate intersect by intersecting their data.

theorem Domain.Neighborhood.Exercise629.slice_subset {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (i : ι) {U U' : Set (α i)} (hUU' : U ⊆ U') : slice D i U ⊆ slice D i U'

Slices are monotone in their data.

theorem Domain.Neighborhood.Exercise629.iprodNbhd_subset_slice {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] {X : (i : ι) → Set (α i)} (hX : ∀ (i : ι), (D i).mem (X i)) (i : ι) : iprodNbhd X ⊆ slice D i (X i)

A cylinder is contained in each of its own slices.

def Domain.Neighborhood.Exercise629.proj {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (z : (iprod D).Element) (i : ι) : (D i).Element

The i-th component of a product element (Scott's z_i).

Equations

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

def Domain.Neighborhood.Exercise629.fromPi {ι : Type u} {α : ι → Type v} (D : (i : ι) → NeighborhoodSystem (α i)) (x : (i : ι) → (D i).Element) : (iprod D).Element

The element of ∏_i D_i assembled from a tuple of components.

Equations

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

theorem Domain.Neighborhood.Exercise629.fromPi_mem_slice {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (x : (i : ι) → (D i).Element) (i : ι) (U : Set (α i)) : (fromPi D x).mem (slice D i U) ↔ (x i).mem U

def Domain.Neighborhood.Exercise629.restrictTo {ι : Type u} {α : ι → Type v} [DecidableEq ι] (D : (i : ι) → NeighborhoodSystem (α i)) (l : List ι) (X : (i : ι) → Set (α i)) (j : ι) : Set (α j)

The cylinder restricted to a list of coordinates l (master outside l).

Equations

• Domain.Neighborhood.Exercise629.restrictTo D l X j = if j ∈ l then X j else (D j).master

theorem Domain.Neighborhood.Exercise629.iprodNbhd_restrictTo_cons {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] {X : (i : ι) → Set (α i)} (hXsub : ∀ (i : ι), X i ⊆ (D i).master) (a : ι) (l : List ι) : iprodNbhd (restrictTo D (a :: l) X) = slice D a (X a) ∩ iprodNbhd (restrictTo D l X)

theorem Domain.Neighborhood.Exercise629.z_mem_iprodNbhd_restrictTo {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (z : (iprod D).Element) {X : (i : ι) → Set (α i)} (hXsub : ∀ (i : ι), X i ⊆ (D i).master) (hslice : ∀ (i : ι), z.mem (slice D i (X i))) (l : List ι) : z.mem (iprodNbhd (restrictTo D l X))

An element contains the restricted cylinder once it contains each listed slice.

theorem Domain.Neighborhood.Exercise629.z_mem_of_slices {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (z : (iprod D).Element) {X : (i : ι) → Set (α i)} (hXmem : ∀ (i : ι), (D i).mem (X i)) (hXf : FinSupp D X) (hslice : ∀ (i : ι), z.mem (slice D i (X i))) : z.mem (iprodNbhd X)

Reconstruction. A product element containing each of a cylinder's slices contains the cylinder. The finite support (a list of coordinates) lets the only finitely many non-trivial slices be intersected inside the element — entirely choice-free.

theorem Domain.Neighborhood.Exercise629.fromPi_toPi {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (z : (iprod D).Element) : (fromPi D fun (i : ι) => proj z i) = z

theorem Domain.Neighborhood.Exercise629.proj_fromPi {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} [DecidableEq ι] (x : (i : ι) → (D i).Element) (i : ι) : proj (fromPi D x) i = x i

def Domain.Neighborhood.Exercise629.iprodEquiv {ι : Type u} {α : ι → Type v} [DecidableEq ι] (D : (i : ι) → NeighborhoodSystem (α i)) : (iprod D).Element ≃o ((i : ι) → (D i).Element)

Exercise 6.29 — × generalizes to ∏, correct up to isomorphism. The domain of the indexed product is the pointwise product of the factor domains: |∏_i D_i| ≃o ∀ i, |D_i|. This is the infinitary Proposition 3.2 (prodEquiv).

Equations

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

+ generalizes to ∑: the indexed separated sum

Tokens live in Option (Σ i, α i): the none basepoint plus tagged copies inj i X of the summands. A neighbourhood constrains only a single coordinate, so — unlike the product — no finite-support condition is needed. We need ∅ ∉ 𝒟ᵢ (hne) to keep distinct tagged copies disjoint.

def Domain.Neighborhood.Exercise629.injI {ι : Type u} {α : ι → Type v} (i : ι) (X : Set (α i)) : Set (Option ((i : ι) × α i))

A tagged copy inj i X = {some ⟨i, a⟩ ∣ a ∈ X} of summand i.

Equations

• Domain.Neighborhood.Exercise629.injI i X = (fun (a : α i) => some ⟨i, a⟩) '' X

theorem Domain.Neighborhood.Exercise629.none_not_mem_injI {ι : Type u} {α : ι → Type v} {i : ι} {X : Set (α i)} : none ∉ injI i X

@[simp]

theorem Domain.Neighborhood.Exercise629.some_mem_injI {ι : Type u} {α : ι → Type v} {i : ι} {a : α i} {X : Set (α i)} : some ⟨i, a⟩ ∈ injI i X ↔ a ∈ X

theorem Domain.Neighborhood.Exercise629.index_of_some_mem_injI {ι : Type u} {α : ι → Type v} {i k : ι} {a : α k} {X : Set (α i)} (hmem : some ⟨k, a⟩ ∈ injI i X) : k = i

A tagged token determines its summand index.

theorem Domain.Neighborhood.Exercise629.injI_nonempty {ι : Type u} {α : ι → Type v} {i : ι} {X : Set (α i)} (hX : X.Nonempty) : (injI i X).Nonempty

theorem Domain.Neighborhood.Exercise629.injI_subset_iff {ι : Type u} {α : ι → Type v} {i : ι} {X Y : Set (α i)} : injI i X ⊆ injI i Y ↔ X ⊆ Y

theorem Domain.Neighborhood.Exercise629.injI_inter_same {ι : Type u} {α : ι → Type v} (i : ι) (X Y : Set (α i)) : injI i X ∩ injI i Y = injI i (X ∩ Y)

theorem Domain.Neighborhood.Exercise629.injI_inter_ne {ι : Type u} {α : ι → Type v} {i j : ι} (h : i ≠ j) (X : Set (α i)) (Y : Set (α j)) : injI i X ∩ injI j Y = ∅

def Domain.Neighborhood.Exercise629.sumMasterI {ι : Type u} {α : ι → Type v} (D : (i : ι) → NeighborhoodSystem (α i)) : Set (Option ((i : ι) × α i))

The basepoint master of the indexed sum: {none} ∪ {some ⟨i, a⟩ ∣ a ∈ Δᵢ}.

Equations

• Domain.Neighborhood.Exercise629.sumMasterI D = insert none ((fun (p : (i : ι) × α i) => some p) '' Domain.Neighborhood.Exercise629.iprodNbhd fun (i : ι) => (D i).master)

theorem Domain.Neighborhood.Exercise629.none_mem_sumMasterI {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} : none ∈ sumMasterI D

theorem Domain.Neighborhood.Exercise629.injI_subset_sumMasterI {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} {i : ι} {X : Set (α i)} (hX : (D i).mem X) : injI i X ⊆ sumMasterI D

def Domain.Neighborhood.Exercise629.isum {ι : Type u} {α : ι → Type v} (D : (i : ι) → NeighborhoodSystem (α i)) (hne : ∀ (i : ι) (X : Set (α i)), (D i).mem X → X.Nonempty) : NeighborhoodSystem (Option ((i : ι) × α i))

Exercise 6.29 — the indexed separated sum ∑_i D_i.

Equations

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

theorem Domain.Neighborhood.Exercise629.isum_trichotomy {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} {hne : ∀ (i : ι) (X : Set (α i)), (D i).mem X → X.Nonempty} (z : (isum D hne).Element) : (∃ (i : ι) (X : Set (α i)), (D i).mem X ∧ z.mem (injI i X)) ∨ ∀ (W : Set (Option ((i : ι) × α i))), z.mem W → W = (isum D hne).master

Exercise 6.29 — sum trichotomy. Every element of ∑_i D_i either reaches into some summand or is the basepoint ⊥. (Prop-level and genuinely classical: the case split is excluded middle on whether z reaches a summand, so this depends on Classical.choice.)

theorem Domain.Neighborhood.Exercise629.isum_summand_unique {ι : Type u} {α : ι → Type v} {D : (i : ι) → NeighborhoodSystem (α i)} {hne : ∀ (i : ι) (X : Set (α i)), (D i).mem X → X.Nonempty} (z : (isum D hne).Element) {i j : ι} {X : Set (α i)} {Y : Set (α j)} (hX : z.mem (injI i X)) (hY : z.mem (injI j Y)) : i = j

Exercise 6.29 — a sum element reaches at most one summand.

⊕ generalizes: the indexed coalesced sum

As ∑, but the improper tagged copies inj i Δᵢ are deleted (the per-summand bottoms are identified with the basepoint). Single-coordinate, so it generalizes with no finite-support issue.

def Domain.Neighborhood.Exercise629.ioplus {ι : Type u} {α : ι → Type v} (D : (i : ι) → NeighborhoodSystem (α i)) (hne : ∀ (i : ι) (X : Set (α i)), (D i).mem X → X.Nonempty) : NeighborhoodSystem (Option ((i : ι) × α i))

Exercise 6.29 — the indexed coalesced sum ⊕_i D_i.

Equations

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

⊗ does not generalize: the infinite smash degenerates

The smash product keeps only those tuples that are proper (≠ master) in every coordinate (plus the basepoint master). Over an infinite index this collides with the finite-support requirement that any neighbourhood imposes — there are no proper neighbourhoods at all, so the infinite smash collapses to the one-point domain.

def Domain.Neighborhood.Exercise629.iotimes {ι : Type u} {α : ι → Type v} (D : (i : ι) → NeighborhoodSystem (α i)) : NeighborhoodSystem ((i : ι) × α i)

Exercise 6.29 — the indexed smash product ⊗_i D_i. A proper neighbourhood is a cylinder proper in every coordinate; closure under intersection is as for iprod plus the observation that X i ∩ X' i ⊆ X i ≠ master stays proper.

Equations

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

theorem Domain.Neighborhood.Exercise629.iotimes_only_master {ι : Type u} {α : ι → Type v} [Infinite ι] (D : (i : ι) → NeighborhoodSystem (α i)) (W : Set ((i : ι) × α i)) : (iotimes D).mem W → W = (iotimes D).master

Exercise 6.29 — ⊗ does not generalize. Over an infinite index, the smash product has only its basepoint: an all-coordinates-proper cylinder has support Set.univ, which cannot be finite.

theorem Domain.Neighborhood.Exercise629.iotimes_subsingleton {ι : Type u} {α : ι → Type v} [Infinite ι] (D : (i : ι) → NeighborhoodSystem (α i)) : Subsingleton (iotimes D).Element

Exercise 6.29 — the infinite smash collapses to one point. Its element domain is a singleton (⊥ only), so ⊗ has no sensible infinitary generalization.