principal-ideal-spectrum

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.principal_ideal_spectrum_homeomorphism

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

For a nonzero element $a$ of a bounded lattice, the Stone spectrum of the principal ideal $[0,a]$ is canonically homeomorphic to the basic subspace $Q_a(L)$ . In the restriction direction,

Q_a(L)\longrightarrow Q([0,a]),\qquad \mathfrak B\longmapsto\mathfrak B\cap[0,a].

The inverse takes upward closure in $L$ . No completeness, orthomodularity or compactness assumption is required.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P20

open Set TopologicalSpace

open QAlgorithms.Papers.Independent.Next46.P33 (Projection)

open scoped Topology

universe u v

/-- principal-ideal-spectrum; de Groote, Observables I, PDF p./pp. 66.
-/
theorem principal_ideal_spectrum_homeomorphism {L : Type u} [Lattice L] [BoundedOrder L] (a : L) (ha : a ≠ ⊥) :
    letI : Bot (Set.Iic a) := ⟨⟨⊥, bot_le⟩⟩
    ∃ h : (stoneBasic a) ≃ₜ StoneSpectrum (Set.Iic a),
      (∀ B, (h B).val = {b | b.val ∈ B.val.val}) ∧
      (∀ C, (h.symm C).val.val = {b | ∃ c ∈ C.val, c.val ≤ b}) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 66, principal-ideal-spectrum

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

Let $L$ be a bounded lattice, and let $a\in L$ satisfy $a\neq\bot$ . For any ordered set with a bottom element, call a family a quasipoint if it is nonempty, excludes bottom, every pair of its members has a common lower bound in the family, and it is maximal under inclusion among families with these properties; equip its quasipoint space with the topology generated by membership in a specified element. Give the lower interval $L_{\leq a}=\{b\in L:b\leq a\}$ its inherited order and bottom element $\bot$ . There exists a homeomorphism $h$ from the subspace of quasipoints $B$ of $L$ satisfying $a\in B$ onto the quasipoint space of $L_{\leq a}$ , such that

h(B)=\{b\in L_{\leq a}:b\in B\} \quad\text{and}\quad h^{-1}(C)=\{b\in L:\exists c\in C,\ c\leq b\}

for every $B$ in the domain and every quasipoint $C$ of the lower interval. These equalities identify quasipoints with their underlying families and interval elements with their underlying elements of $L$ .

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph