Exercise 3.15 (Scott 1981, PRG-19, §3) — the usual product isomorphisms

Scott asks for the standard isomorphisms of the product construction. Because Proposition 3.2 gives the order-isomorphism prodEquiv : |𝒟₀ × 𝒟₁| ≃o |𝒟₀| × |𝒟₁|, every isomorphism reduces to the corresponding fact about cartesian products of ordered sets: mathlib's OrderIso.prodComm and OrderIso.prodAssoc, together with the two product congruences prodCongrOrderIso / prodUniqueOrderIso we record here.

• (i) 𝒟₀ × 𝒟₁ ≅ 𝒟₁ × 𝒟₀ — prodCommD.
• (ii) 𝒟₀ × (𝒟₁ × 𝒟₂) ≅ (𝒟₀ × 𝒟₁) × 𝒟₂ — prodAssocD.
• The product of no factors is the one-point (terminal) domain 𝟙 = unitSys; it is a two-sided unit for ×: 𝒟 × 𝟙 ≅ 𝒟 ≅ 𝟙 × 𝒟 (prodUnitD, unitProdD).
• (iii) 𝒟₀ ≅ 𝒟₀' and 𝒟₁ ≅ 𝒟₁' imply 𝒟₀ × 𝒟₁ ≅ 𝒟₀' × 𝒟₁' — prodCongrD / Isomorphic.prod.

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

Order-iso helpers for cartesian products.

def Domain.Neighborhood.prodCongrOrderIso {A : Type u_6} {B : Type u_7} {C : Type u_8} {D : Type u_9} [Preorder A] [Preorder B] [Preorder C] [Preorder D] (e₀ : A ≃o B) (e₁ : C ≃o D) : A × C ≃o B × D

The product of two order isomorphisms, as an order isomorphism.

Equations

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

def Domain.Neighborhood.prodUniqueOrderIso (A : Type u_6) (C : Type u_7) [Preorder A] [Preorder C] [Unique C] : A × C ≃o A

For a Unique second factor, A × C ≃o A (forget the constant component).

Equations

• Domain.Neighborhood.prodUniqueOrderIso A C = { toFun := fun (p : A × C) => p.1, invFun := fun (a : A) => (a, default), left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

def Domain.Neighborhood.uniqueProdOrderIso (A : Type u_6) (C : Type u_7) [Preorder A] [Preorder C] [Unique C] : C × A ≃o A

For a Unique first factor, C × A ≃o A (forget the constant component).

Equations

• Domain.Neighborhood.uniqueProdOrderIso A C = { toFun := fun (p : C × A) => p.2, invFun := fun (a : A) => (default, a), left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

(i) Commutativity.

def Domain.Neighborhood.prodCommD {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : (prod V₀ V₁).Element ≃o (prod V₁ V₀).Element

Exercise 3.15(i) (Scott 1981, PRG-19). The commutativity order-isomorphism |𝒟₀ × 𝒟₁| ≃o |𝒟₁ × 𝒟₀|, factored through Proposition 3.2 and the cartesian swap.

Equations

• Domain.Neighborhood.prodCommD V₀ V₁ = (Domain.Neighborhood.prodEquiv V₀ V₁).trans (OrderIso.prodComm.trans (Domain.Neighborhood.prodEquiv V₁ V₀).symm)

theorem Domain.Neighborhood.prod_comm_isomorphic {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : prod V₀ V₁ ≅ᴰ prod V₁ V₀

Exercise 3.15(i). 𝒟₀ × 𝒟₁ ≅ 𝒟₁ × 𝒟₀.

(ii) Associativity.

def Domain.Neighborhood.prodAssocD {α : Type u_1} {β : Type u_2} {γ : Type u_3} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) (V₂ : NeighborhoodSystem γ) : (prod V₀ (prod V₁ V₂)).Element ≃o (prod (prod V₀ V₁) V₂).Element

Exercise 3.15(ii) (Scott 1981, PRG-19). The associativity order-isomorphism |𝒟₀ × (𝒟₁ × 𝒟₂)| ≃o |(𝒟₀ × 𝒟₁) × 𝒟₂|.

Equations

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

theorem Domain.Neighborhood.prod_assoc_isomorphic {α : Type u_1} {β : Type u_2} {γ : Type u_3} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₂ : NeighborhoodSystem γ} : prod V₀ (prod V₁ V₂) ≅ᴰ prod (prod V₀ V₁) V₂

Exercise 3.15(ii). 𝒟₀ × (𝒟₁ × 𝒟₂) ≅ (𝒟₀ × 𝒟₁) × 𝒟₂.

The product of no factors — the terminal (one-point) domain.

def Domain.Neighborhood.unitSys : NeighborhoodSystem Unit

The terminal domain 𝟙: the neighbourhood system over Unit with the single neighbourhood Δ = univ. Its domain |𝟙| has exactly one element (⊥ = {Δ}), so 𝟙 is the product of no factors.

Equations

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

theorem Domain.Neighborhood.unitSys_element_eq (x : unitSys.Element) : x = unitSys.bot

|𝟙| is a subsingleton: every element is ⊥.

@[implicit_reducible]

instance Domain.Neighborhood.instUniqueElementUnitUnitSys : Unique unitSys.Element

Equations

• Domain.Neighborhood.instUniqueElementUnitUnitSys = { default := Domain.Neighborhood.unitSys.bot, uniq := Domain.Neighborhood.unitSys_element_eq }

def Domain.Neighborhood.prodUnitD {α : Type u_1} (V₀ : NeighborhoodSystem α) : (prod V₀ unitSys).Element ≃o V₀.Element

Exercise 3.15 (empty product). 𝟙 is a right unit: 𝒟 × 𝟙 ≅ 𝒟.

Equations

• Domain.Neighborhood.prodUnitD V₀ = (Domain.Neighborhood.prodEquiv V₀ Domain.Neighborhood.unitSys).trans (Domain.Neighborhood.prodUniqueOrderIso V₀.Element Domain.Neighborhood.unitSys.Element)

theorem Domain.Neighborhood.prod_unit_isomorphic {α : Type u_1} {V₀ : NeighborhoodSystem α} : prod V₀ unitSys ≅ᴰ V₀

def Domain.Neighborhood.unitProdD {α : Type u_1} (V₀ : NeighborhoodSystem α) : (prod unitSys V₀).Element ≃o V₀.Element

Exercise 3.15 (empty product). 𝟙 is a left unit: 𝟙 × 𝒟 ≅ 𝒟.

Equations

• Domain.Neighborhood.unitProdD V₀ = (Domain.Neighborhood.prodEquiv Domain.Neighborhood.unitSys V₀).trans (Domain.Neighborhood.uniqueProdOrderIso V₀.Element Domain.Neighborhood.unitSys.Element)

theorem Domain.Neighborhood.unit_prod_isomorphic {α : Type u_1} {V₀ : NeighborhoodSystem α} : prod unitSys V₀ ≅ᴰ V₀

(iii) Functoriality of ≅.

def Domain.Neighborhood.prodCongrD {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} (e₀ : V₀.Element ≃o V₀'.Element) (e₁ : V₁.Element ≃o V₁'.Element) : (prod V₀ V₁).Element ≃o (prod V₀' V₁').Element

Exercise 3.15(iii) (Scott 1981, PRG-19). Two domain isomorphisms induce one on the products: |𝒟₀ × 𝒟₁| ≃o |𝒟₀' × 𝒟₁'|.

Equations

• Domain.Neighborhood.prodCongrD e₀ e₁ = (Domain.Neighborhood.prodEquiv V₀ V₁).trans ((Domain.Neighborhood.prodCongrOrderIso e₀ e₁).trans (Domain.Neighborhood.prodEquiv V₀' V₁').symm)

theorem Domain.Neighborhood.Isomorphic.prod {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {V₀' : NeighborhoodSystem α'} {V₁' : NeighborhoodSystem β'} (h₀ : V₀ ≅ᴰ V₀') (h₁ : V₁ ≅ᴰ V₁') : Neighborhood.prod V₀ V₁ ≅ᴰ Neighborhood.prod V₀' V₁'

Exercise 3.15(iii). 𝒟₀ ≅ 𝒟₀' and 𝒟₁ ≅ 𝒟₁' imply 𝒟₀ × 𝒟₁ ≅ 𝒟₀' × 𝒟₁'.