Exercise 3.14 (Scott 1981, PRG-19, §3) — the diagonal map

Scott's Exercise 3.14 makes two points.

• The disjointness of Δ₀ and Δ₁ is unnecessary. Working over a denumerable token alphabet Σ = {0, 1}, one may tag the two factors, taking the product system over 0Δ₀ ∪ 1Δ₁ with neighbourhoods 0X ∪ 1Y. Our Product.lean already realizes exactly this tagging abstractly: the disjoint union of token types α ⊕ β is the type-theoretic incarnation of 0Δ₀ ∪ 1Δ₁, and prodNbhd X Y = Sum.inl '' X ∪ Sum.inr '' Y is 0X ∪ 1Y. So no separate construction is needed — prod V₀ V₁ is the tagged product, and the revised pairing ⟨x, y⟩ is pair (Definition 3.1).

• The diagonal diag : 𝒟 → 𝒟 × 𝒟, diag(x) = ⟨x, x⟩. This is the paired map ⟨I, I⟩ of the identity with itself (Definition 3.3), so it is approximable for free, and toElementMap_diag computes diag(x) = ⟨x, x⟩ from toElementMap_paired.

The n-fold product 𝒟₀ × ⋯ × 𝒟_{n-1} over ⋃_{i<n} 1ⁱ0 Δᵢ is obtained by iterating the binary prod (it is associative up to isomorphism, Exercise 3.15); the binary diagonal here is the n = 2 instance of the general diagonal x ↦ ⟨x, …, x⟩.

Everything is choice-free (#print axioms ⊆ {propext, Quot.sound}).

def Domain.Neighborhood.diag {α : Type u_1} (V : NeighborhoodSystem α) : ApproximableMap V (prod V V)

Exercise 3.14 (Scott 1981, PRG-19). The diagonal approximable mapping diag : 𝒟 → 𝒟 × 𝒟, defined as the paired map ⟨I_𝒟, I_𝒟⟩ of the identity with itself.

Equations

• Domain.Neighborhood.diag V = Domain.Neighborhood.paired (Domain.Neighborhood.ApproximableMap.idMap V) (Domain.Neighborhood.ApproximableMap.idMap V)

@[simp]

theorem Domain.Neighborhood.diag_rel {α : Type u_1} (V : NeighborhoodSystem α) {Z : Set α} {P : Set (α ⊕ α)} : (diag V).rel Z P ↔ (prod V V).mem P ∧ (ApproximableMap.idMap V).rel Z (Sum.inl ⁻¹' P) ∧ (ApproximableMap.idMap V).rel Z (Sum.inr ⁻¹' P)

@[simp]

theorem Domain.Neighborhood.toElementMap_diag {α : Type u_1} (V : NeighborhoodSystem α) (x : V.Element) : (diag V).toElementMap x = pair x x

Exercise 3.14 (Scott 1981, PRG-19). diag(x) = ⟨x, x⟩ for every x ∈ |𝒟|.

theorem Domain.Neighborhood.proj₀_comp_diag {α : Type u_1} (V : NeighborhoodSystem α) : (proj₀ V V).comp (diag V) = ApproximableMap.idMap V

Exercise 3.14 (Scott 1981, PRG-19). Post-composing the diagonal with the two projections returns the identity: p₀ ∘ diag = I and p₁ ∘ diag = I.

theorem Domain.Neighborhood.proj₁_comp_diag {α : Type u_1} (V : NeighborhoodSystem α) : (proj₁ V V).comp (diag V) = ApproximableMap.idMap V