Exercise 3.19 / 3.20 (Scott 1981, PRG-19, §3) — the product functor f × g

Given approximable mappings f : 𝒟₀ → 𝒟₀' and g : 𝒟₁ → 𝒟₁', Scott's Exercise 3.19 constructs the product mapping f × g : 𝒟₀ × 𝒟₁ → 𝒟₀' × 𝒟₁' with

• (i) (f × g)(⟨x, y⟩) = ⟨f(x), g(y)⟩, and
• (ii) f × g = ⟨f ∘ p₀, g ∘ p₁⟩.

We take (ii) as the definition (prodMap, built from Definition 3.3's paired/proj), and prove (i) — indeed the more general toElementMap_prodMap ((f × g)(w) = ⟨f(w₀), g(w₁)⟩).

Exercise 3.20 (for category theorists) then follows: × is a functor (prodMap_id, prodMap_comp), and prod with its projections is the categorical product — the universal property paired/proj with uniqueness paired_unique.

The sum functor f + g is treated in Exercise318.lean/Exercise319Sum.lean after the sum system is built. Everything here is choice-free (#print axioms ⊆ {propext, Quot.sound}).

def Domain.Neighborhood.prodMap {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} (f : ApproximableMap V₀ V₀') (g : ApproximableMap V₁ V₁') : ApproximableMap (prod V₀ V₁) (prod V₀' V₁')

Exercise 3.19(ii) (Scott 1981, PRG-19). The product mapping f × g = ⟨f ∘ p₀, g ∘ p₁⟩.

Equations

• Domain.Neighborhood.prodMap f g = Domain.Neighborhood.paired (f.comp (Domain.Neighborhood.proj₀ V₀ V₁)) (g.comp (Domain.Neighborhood.proj₁ V₀ V₁))

theorem Domain.Neighborhood.toElementMap_prodMap {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} (f : ApproximableMap V₀ V₀') (g : ApproximableMap V₁ V₁') (w : (prod V₀ V₁).Element) : (prodMap f g).toElementMap w = pair (f.toElementMap w.fst) (g.toElementMap w.snd)

Exercise 3.19 (Scott 1981, PRG-19). (f × g)(w) = ⟨f(w₀), g(w₁)⟩ for every product element w (so in particular (f × g)(⟨x, y⟩) = ⟨f(x), g(y)⟩, equation (i)).

theorem Domain.Neighborhood.toElementMap_prodMap_pair {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} (f : ApproximableMap V₀ V₀') (g : ApproximableMap V₁ V₁') (x : V₀.Element) (y : V₁.Element) : (prodMap f g).toElementMap (pair x y) = pair (f.toElementMap x) (g.toElementMap y)

Exercise 3.19(i) (Scott 1981, PRG-19). (f × g)(⟨x, y⟩) = ⟨f(x), g(y)⟩.

Exercise 3.20 — × is a functor.

theorem Domain.Neighborhood.prodMap_id {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : prodMap (ApproximableMap.idMap V₀) (ApproximableMap.idMap V₁) = ApproximableMap.idMap (prod V₀ V₁)

Exercise 3.20 (Scott 1981, PRG-19). × preserves identities: I × I = I.

theorem Domain.Neighborhood.prodMap_comp {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} {α'' : Type u_6} {β'' : Type u_7} {V₀'' : NeighborhoodSystem α''} {V₁'' : NeighborhoodSystem β''} (f' : ApproximableMap V₀' V₀'') (f : ApproximableMap V₀ V₀') (g' : ApproximableMap V₁' V₁'') (g : ApproximableMap V₁ V₁') : prodMap (f'.comp f) (g'.comp g) = (prodMap f' g').comp (prodMap f g)

Exercise 3.20 (Scott 1981, PRG-19). × preserves composition: (f' ∘ f) × (g' ∘ g) = (f' × g') ∘ (f × g).

Exercise 3.20 — prod is the categorical product.

theorem Domain.Neighborhood.proj_paired {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h₀ : ApproximableMap V₂ V₀) (h₁ : ApproximableMap V₂ V₁) : (proj₀ V₀ V₁).comp (paired h₀ h₁) = h₀ ∧ (proj₁ V₀ V₁).comp (paired h₀ h₁) = h₁

Exercise 3.20 (Scott 1981, PRG-19). The universal property of the product (existence): p₀ ∘ ⟨h₀, h₁⟩ = h₀ and p₁ ∘ ⟨h₀, h₁⟩ = h₁ (these are Proposition 3.4(i)).

theorem Domain.Neighborhood.paired_unique {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} (h₀ : ApproximableMap V₂ V₀) (h₁ : ApproximableMap V₂ V₁) (k : ApproximableMap V₂ (prod V₀ V₁)) (hk₀ : (proj₀ V₀ V₁).comp k = h₀) (hk₁ : (proj₁ V₀ V₁).comp k = h₁) : k = paired h₀ h₁

Exercise 3.20 (Scott 1981, PRG-19). The universal property of the product (uniqueness): any k with p₀ ∘ k = h₀ and p₁ ∘ k = h₁ equals the pairing ⟨h₀, h₁⟩. Hence prod with proj₀, proj₁ is the categorical product of 𝒟₀ and 𝒟₁.