Exercise 6.27 (Scott 1981, PRG-19, §6) — which subsystem relations hold

EXERCISE 6.27. Which of the following relationships are true: (𝒟 ⊗ ℰ) ⊴ (𝒟 × ℰ); 𝒟 ⊴ 𝒟 × ℰ; (𝒟 ⊕ ℰ) ⊴ (𝒟 + ℰ); 𝒟 ⊴ 𝒟 ⊕ ℰ; (𝒟 →⊥ ℰ) ⊴ (𝒟 → ℰ); 𝒟 ⊴ 𝒟 ⊗ ℰ ?

Here ⊴ is Scott's embeds-as-a-subdomain relation of Lemma 6.15 (Trianglelefteq): D ⊴ E means D ≅ᴰ D' for some D' ◁ E. We use the concrete {0,1}* constructions of Exercises 6.19/6.21 (sumTok, prodTok, oplusTok, otimesTok) and the function spaces funSpace / strictFun.

Answer. The first five hold for all 𝒟, ℰ; the last fails in general.

relation	verdict	name
(𝒟 ⊗ ℰ) ⊴ (𝒟 × ℰ)	true	otimes_trianglelefteq_prod (in fact
otimesTok ◁ prodTok)
𝒟 ⊴ 𝒟 × ℰ	true	fst_trianglelefteq_prod
(𝒟 ⊕ ℰ) ⊴ (𝒟 + ℰ)	true	oplus_trianglelefteq_sum (in fact `oplusTok ◁
sumTok`)
𝒟 ⊴ 𝒟 ⊕ ℰ	true	inl_trianglelefteq_oplus
(𝒟 →⊥ ℰ) ⊴ (𝒟 → ℰ)	true	strictFun_trianglelefteq_funSpace
𝒟 ⊴ 𝒟 ⊗ ℰ	false in general	not_trianglelefteq_otimes_unit

The smash product collapses the bottom: pairing anything with ⊥_ℰ is ⊥. So 𝒟 embeds in 𝒟 ⊗ ℰ only when ℰ contributes a (finite) non-bottom point; for the trivial ℰ = 𝟙 we have 𝒟 ⊗ 𝟙 ≅ 𝟙, refuting the universal claim.

All parts are choice-free (#print axioms ⊆ {propext, Quot.sound}) except (4) (inl_trianglelefteq_oplus), whose oplus_mem_leftN decides the genuinely-undecidable test X = Δ₀ over an arbitrary system and so depends on Classical.choice.

(1) (𝒟 ⊗ ℰ) ◁ (𝒟 × ℰ) — the smash is literally a subsystem of the product

The smash otimesTok has the same master {Λ} ∪ 0Δ₀ ∪ 1Δ₁ = prodTokNbhd Δ₀ Δ₁ and its proper neighbourhoods prodTokNbhd X Y (with X ≠ Δ₀, Y ≠ Δ₁) are a sub-family of the product's neighbourhoods. The consistency clause is inherited because intersections stay off the boundary.

theorem Domain.Neighborhood.Exercise627.otimesTok_subsystem_prodTok (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : Exercise619.otimesTok D₀ D₁ ◁ Exercise619.prodTok D₀ D₁

theorem Domain.Neighborhood.Exercise627.otimes_trianglelefteq_prod (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : Exercise619.otimesTok D₀ D₁ ⊴ Exercise619.prodTok D₀ D₁

Exercise 6.27 (1). (𝒟 ⊗ ℰ) ⊴ (𝒟 × ℰ).

(2) 𝒟 ⊴ 𝒟 × ℰ — first-factor projection pair

𝒟 is not literally a subsystem of 𝒟 × ℰ (the neighbourhoods have a different shape), but it embeds via the projection pair i(X) = (X, ⊥), j(W) = fst W. Concretely we send X ∈ 𝒟 to the product neighbourhood prodTokNbhd X Δ₁ (pair X with all of ℰ); the embedding/projection are the two refinement relations against that neighbourhood, exactly as in Proposition 6.12.

def Domain.Neighborhood.Exercise627.fstInj (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : ApproximableMap D₀ (Exercise619.prodTok D₀ D₁)

The injection i : 𝒟 → 𝒟 × ℰ: X i W ↔ X ∈ 𝒟 ∧ W ∈ 𝒟×ℰ ∧ (X,Δ₁) ⊆ W.

Equations

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

def Domain.Neighborhood.Exercise627.fstProj (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : ApproximableMap (Exercise619.prodTok D₀ D₁) D₀

The projection j : 𝒟 × ℰ → 𝒟: W j X ↔ W ∈ 𝒟×ℰ ∧ X ∈ 𝒟 ∧ W ⊆ (X,Δ₁).

Equations

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

theorem Domain.Neighborhood.Exercise627.fstProj_comp_fstInj (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : (fstProj D₀ D₁).comp (fstInj D₀ D₁) = ApproximableMap.idMap D₀

theorem Domain.Neighborhood.Exercise627.fstInj_comp_fstProj_le (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : (fstInj D₀ D₁).comp (fstProj D₀ D₁) ≤ ApproximableMap.idMap (Exercise619.prodTok D₀ D₁)

theorem Domain.Neighborhood.Exercise627.fst_trianglelefteq_prod (D₀ D₁ : NeighborhoodSystem ExampleB.Str) : D₀ ⊴ Exercise619.prodTok D₀ D₁

Exercise 6.27 (2). 𝒟 ⊴ 𝒟 × ℰ.

(3) (𝒟 ⊕ ℰ) ◁ (𝒟 + ℰ) — the coalesced sum is literally a subsystem of the

sum

oplusTok drops the improper copies 0Δ₀, 1Δ₁ of sumTok; what remains is a sub-family, and consistency is inherited (cross-tag intersections are empty, hence not sumTok-neighbourhoods).

theorem Domain.Neighborhood.Exercise627.oplusTok_subsystem_sumTok {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty) (h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty) : Exercise619.oplusTok D₀ D₁ h₀ h₁ ◁ Exercise619.sumTok D₀ D₁ h₀ h₁

theorem Domain.Neighborhood.Exercise627.oplus_trianglelefteq_sum {D₀ D₁ : NeighborhoodSystem ExampleB.Str} (h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty) (h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty) : Exercise619.oplusTok D₀ D₁ h₀ h₁ ⊴ Exercise619.sumTok D₀ D₁ h₀ h₁

Exercise 6.27 (3). (𝒟 ⊕ ℰ) ⊴ (𝒟 + ℰ).

(4) 𝒟 ⊴ 𝒟 ⊕ ℰ — left-injection projection pair

Unlike the product, the coalesced sum identifies the two bottoms, so the embedding of 𝒟 must send ⊥_𝒟 = Δ₀ to the shared bottom sumTokMaster and a proper X to its left copy 0X. We package this in leftN X (= 0X for proper X, = sumTokMaster for X = Δ₀).

Distinguishing the two cases is exactly the test X = Δ₀, which is undecidable for an arbitrary neighbourhood; consequently the single lemma oplus_mem_leftN — and only it — uses Classical.em. This is genuinely unavoidable at this level of generality (Scott's tokens are concrete and decidable, but we work over arbitrary NeighborhoodSystems), so inl_trianglelefteq_oplus depends on Classical.choice (called out in the axiom audit). Every other part of Exercise 6.27 is choice-free.

def Domain.Neighborhood.Exercise627.leftN (D₀ D₁ : NeighborhoodSystem ExampleB.Str) (X : Set ExampleB.Str) : Set ExampleB.Str

The left-copy generator: 0X for proper X, the shared bottom sumTokMaster for X = Δ₀. The set-builder {w ∣ w ∈ sumTokMaster ∧ X = Δ₀} keeps the definition choice-free.

Equations

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

theorem Domain.Neighborhood.Exercise627.embF_subset_leftN {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} : Example62.embBit false X ⊆ leftN D₀ D₁ X

theorem Domain.Neighborhood.Exercise627.leftN_master {D₀ D₁ : NeighborhoodSystem ExampleB.Str} : leftN D₀ D₁ D₀.master = Exercise619.sumTokMaster D₀ D₁

theorem Domain.Neighborhood.Exercise627.leftN_proper {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} (hne : X ≠ D₀.master) : leftN D₀ D₁ X = Example62.embBit false X

theorem Domain.Neighborhood.Exercise627.X_eq_master_of_nil_mem_leftN {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X : Set ExampleB.Str} (h : [] ∈ leftN D₀ D₁ X) : X = D₀.master

theorem Domain.Neighborhood.Exercise627.subset_of_embF_subset_leftN {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {A X : Set ExampleB.Str} (hA : A ⊆ D₀.master) (h : Example62.embBit false A ⊆ leftN D₀ D₁ X) : A ⊆ X

theorem Domain.Neighborhood.Exercise627.X_eq_master_of_embT_subset_leftN {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {B X : Set ExampleB.Str} (hB : B.Nonempty) (h : Example62.embBit true B ⊆ leftN D₀ D₁ X) : X = D₀.master

theorem Domain.Neighborhood.Exercise627.leftN_subset_iff {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {X X' : Set ExampleB.Str} (hX : D₀.mem X) (hX' : D₀.mem X') : leftN D₀ D₁ X ⊆ leftN D₀ D₁ X' ↔ X ⊆ X'

theorem Domain.Neighborhood.Exercise627.oplus_mem_leftN {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} {X : Set ExampleB.Str} (hX : D₀.mem X) : (Exercise619.oplusTok D₀ D₁ h₀ h₁).mem (leftN D₀ D₁ X)

The only classical step in Exercise 6.27: leftN X is an 𝒟 ⊕ ℰ-neighbourhood. The proof splits on the (undecidable for arbitrary X) test X = Δ₀.

def Domain.Neighborhood.Exercise627.inlInj {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : ApproximableMap D₀ (Exercise619.oplusTok D₀ D₁ h₀ h₁)

The injection i : 𝒟 → 𝒟 ⊕ ℰ: X i W ↔ X ∈ 𝒟 ∧ W ∈ 𝒟⊕ℰ ∧ leftN X ⊆ W.

Equations

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

def Domain.Neighborhood.Exercise627.inlProj {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : ApproximableMap (Exercise619.oplusTok D₀ D₁ h₀ h₁) D₀

The projection j : 𝒟 ⊕ ℰ → 𝒟: W j X ↔ W ∈ 𝒟⊕ℰ ∧ X ∈ 𝒟 ∧ W ⊆ leftN X.

Equations

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

theorem Domain.Neighborhood.Exercise627.inlProj_comp_inlInj {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : inlProj.comp inlInj = ApproximableMap.idMap D₀

theorem Domain.Neighborhood.Exercise627.inlInj_comp_inlProj_le {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : inlInj.comp inlProj ≤ ApproximableMap.idMap (Exercise619.oplusTok D₀ D₁ h₀ h₁)

theorem Domain.Neighborhood.Exercise627.inl_trianglelefteq_oplus {D₀ D₁ : NeighborhoodSystem ExampleB.Str} {h₀ : ∀ (X : Set ExampleB.Str), D₀.mem X → X.Nonempty} {h₁ : ∀ (Y : Set ExampleB.Str), D₁.mem Y → Y.Nonempty} : D₀ ⊴ Exercise619.oplusTok D₀ D₁ h₀ h₁

Exercise 6.27 (4). 𝒟 ⊴ 𝒟 ⊕ ℰ. (Uses Classical.choice via oplus_mem_leftN.)

(5) (𝒟 →⊥ ℰ) ⊴ (𝒟 → ℰ) — the strict maps embed in all maps

A strict map is an approximable map, so 𝒟 →⊥ ℰ sits inside 𝒟 → ℰ by inclusion i, with the strictification j (force f(⊥) = ⊥) as its retraction. strictify f ⊑ f always, and on a strict f strictification is the identity; this gives the projection-pair laws j ∘ i = id, i ∘ j ⊑ id. We work over arbitrary systems V₀, V₁ (not just Str); the construction is choice-free. We realise i, j on principal inputs via ofMono of the element-level inclusion / strictification, then identify their element maps using the representations funSpaceEquiv (|𝒟→ℰ| ≃ ApproximableMap) and strictFunEquiv (|𝒟→⊥ℰ| ≃ StrictMap).

def Domain.Neighborhood.Exercise627.strictifyMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : ApproximableMap V₀ V₁) : ApproximableMap V₀ V₁

Strictification of a map (on relations): keep f but force the master input to the master output. The resulting map is strict, lies below f, and is the identity on strict maps.

Equations

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

theorem Domain.Neighborhood.Exercise627.strictifyMap_isStrict {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : ApproximableMap V₀ V₁) : Exercise510.IsStrict (strictifyMap g)

theorem Domain.Neighborhood.Exercise627.strictifyMap_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : ApproximableMap V₀ V₁) : strictifyMap g ≤ g

theorem Domain.Neighborhood.Exercise627.strictifyMap_of_isStrict {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} {f : ApproximableMap V₀ V₁} (hf : Exercise510.IsStrict f) : strictifyMap f = f

def Domain.Neighborhood.Exercise627.strictify {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : ApproximableMap V₀ V₁) : Exercise510.StrictMap V₀ V₁

The strictification as an element of the strict function space's token type.

Equations

• Domain.Neighborhood.Exercise627.strictify g = ⟨Domain.Neighborhood.Exercise627.strictifyMap g, ⋯⟩

theorem Domain.Neighborhood.Exercise627.toApproxMap_toFilter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : ApproximableMap V₀ V₁) : toApproxMap (toFilter g) = g

The four inverse identities of the two representation equivalences (defeq unfoldings).

theorem Domain.Neighborhood.Exercise627.toFilter_toApproxMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (ψ : (funSpace V₀ V₁).Element) : toFilter (toApproxMap ψ) = ψ

theorem Domain.Neighborhood.Exercise627.toStrictMap_toStrictFilter {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (g : Exercise510.StrictMap V₀ V₁) : Exercise510.toStrictMap (Exercise510.toStrictFilter g) = g

theorem Domain.Neighborhood.Exercise627.toStrictFilter_toStrictMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (Exercise510.strictFun V₀ V₁).Element) : Exercise510.toStrictFilter (Exercise510.toStrictMap φ) = φ

def Domain.Neighborhood.Exercise627.incl {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (Exercise510.strictFun V₀ V₁).Element) : (funSpace V₀ V₁).Element

Element-level inclusion |𝒟 →⊥ ℰ| → |𝒟 → ℰ|.

Equations

• Domain.Neighborhood.Exercise627.incl φ = Domain.Neighborhood.toFilter ↑(Domain.Neighborhood.Exercise510.toStrictMap φ)

def Domain.Neighborhood.Exercise627.strct {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (ψ : (funSpace V₀ V₁).Element) : (Exercise510.strictFun V₀ V₁).Element

Element-level strictification |𝒟 → ℰ| → |𝒟 →⊥ ℰ|.

Equations

• Domain.Neighborhood.Exercise627.strct ψ = Domain.Neighborhood.Exercise510.toStrictFilter (Domain.Neighborhood.Exercise627.strictify (Domain.Neighborhood.toApproxMap ψ))

theorem Domain.Neighborhood.Exercise627.incl_mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : Monotone incl

theorem Domain.Neighborhood.Exercise627.strct_mono {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : Monotone strct

def Domain.Neighborhood.Exercise627.inclMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : ApproximableMap (Exercise510.strictFun V₀ V₁) (funSpace V₀ V₁)

The inclusion i : 𝒟 →⊥ ℰ ↪ 𝒟 → ℰ.

Equations

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

def Domain.Neighborhood.Exercise627.strctMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : ApproximableMap (funSpace V₀ V₁) (Exercise510.strictFun V₀ V₁)

The strictification retraction j : 𝒟 → ℰ → 𝒟 →⊥ ℰ.

Equations

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

theorem Domain.Neighborhood.Exercise627.toElementMap_inclMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (Exercise510.strictFun V₀ V₁).Element) : inclMap.toElementMap φ = incl φ

theorem Domain.Neighborhood.Exercise627.toElementMap_strctMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (ψ : (funSpace V₀ V₁).Element) : strctMap.toElementMap ψ = strct ψ

theorem Domain.Neighborhood.Exercise627.strct_incl {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (φ : (Exercise510.strictFun V₀ V₁).Element) : strct (incl φ) = φ

theorem Domain.Neighborhood.Exercise627.incl_strct_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} (ψ : (funSpace V₀ V₁).Element) : incl (strct ψ) ≤ ψ

theorem Domain.Neighborhood.Exercise627.ext_of_principal {γ : Type u_3} {δ : Type u_4} {W₀ : NeighborhoodSystem γ} {W₁ : NeighborhoodSystem δ} {f g : ApproximableMap W₀ W₁} (h : ∀ (X : Set γ) (hX : W₀.mem X), f.toElementMap (W₀.principal hX) = g.toElementMap (W₀.principal hX)) : f = g

Choice-free extensionality from agreement on principal inputs. Unlike ext_of_toElementMap (which splits on the undecidable V₀.mem X), both sides of the relation carry domain membership via rel_dom, so no case analysis — and hence no Classical.choice — is needed.

theorem Domain.Neighborhood.Exercise627.strctMap_comp_inclMap {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : strctMap.comp inclMap = ApproximableMap.idMap (Exercise510.strictFun V₀ V₁)

theorem Domain.Neighborhood.Exercise627.inclMap_comp_strctMap_le {α : Type u_1} {β : Type u_2} {V₀ : NeighborhoodSystem α} {V₁ : NeighborhoodSystem β} : inclMap.comp strctMap ≤ ApproximableMap.idMap (funSpace V₀ V₁)

theorem Domain.Neighborhood.Exercise627.strictFun_trianglelefteq_funSpace {α : Type u_1} {β : Type u_2} (V₀ : NeighborhoodSystem α) (V₁ : NeighborhoodSystem β) : Exercise510.strictFun V₀ V₁ ⊴ funSpace V₀ V₁

Exercise 6.27 (5). (𝒟 →⊥ ℰ) ⊴ (𝒟 → ℰ) for all 𝒟, ℰ (choice-free).

(6) 𝒟 ⊴ 𝒟 ⊗ ℰ is false in general

The smash product sends (x, ⊥) and (⊥, y) to the single bottom, so if ℰ contributes no proper neighbourhood the whole product collapses to its bottom. Concretely, for the one-point unit ℰ = 𝟙 the system 𝒟 ⊗ 𝟙 has only its master as a neighbourhood, hence a one-point element lattice; a 𝒟 with two distinct points therefore cannot embed. This refutes the universal claim.

theorem Domain.Neighborhood.Exercise627.subsingleton_element_of_only_master {γ : Type u_1} {V : NeighborhoodSystem γ} (h : ∀ (X : Set γ), V.mem X → X = V.master) : Subsingleton V.Element

If a system's only neighbourhood is its master, its element lattice is a single point (⊥).

def Domain.Neighborhood.Exercise627.twoPt : NeighborhoodSystem ExampleB.Str

A concrete two-point domain over {0,1}*: neighbourhoods Set.univ (= ⊥) and {[]}.

Equations

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

def Domain.Neighborhood.Exercise627.unitPt : NeighborhoodSystem ExampleB.Str

The one-point unit domain 𝟙 over {0,1}* (only neighbourhood {[]}).

Equations

• Domain.Neighborhood.Exercise627.unitPt = (Domain.Neighborhood.Exercise619.singletonSys {[]} Domain.Neighborhood.Exercise627.unitPt._proof_1).sys

theorem Domain.Neighborhood.Exercise627.otimes_unitPt_collapse (W : Set ExampleB.Str) : (Exercise619.otimesTok twoPt unitPt).mem W → W = (Exercise619.otimesTok twoPt unitPt).master

With the unit second factor, the smash twoPt ⊗ 𝟙 collapses to its master.

theorem Domain.Neighborhood.Exercise627.not_trianglelefteq_otimes : ¬twoPt ⊴ Exercise619.otimesTok twoPt unitPt

Exercise 6.27 (6). 𝒟 ⊴ 𝒟 ⊗ ℰ does not hold for all 𝒟, ℰ: take 𝒟 two-point and ℰ = 𝟙. Then 𝒟 ⊗ 𝟙 has a one-point element lattice while 𝒟 has two, so no isomorphism onto a subsystem can exist.