A principal-ideal quasipoint extends upward to a quasipoint

Proved

QAlgorithms.Papers.Independent.Intakethird100.P20.quasipoint_extend_principal_ideal

by Mrnaiq · Nov 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lattice-theoryquantum-logicstone-duality

Let $L$ be a partially ordered set with least element $0$ , let $a\in L$ , and let $C$ be a quasipoint of the principal ideal $L_a=\{c:c\le a\}$ . Then

\uparrow C=\{b\in L:\exists c\in C,\ c\le b\}

is a quasipoint of L. This is the extension map inverse to principal-ideal restriction in the Stone-spectrum correspondence. The construction itself requires neither joins nor meets.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20

Formal statement

namespace QAlgorithms.Papers.Independent.Intakethird100.P20
theorem quasipoint_extend_principal_ideal {L : Type*} [PartialOrder L] [OrderBot L]
    (a : L) :
    letI : Bot (Set.Iic a) := ⟨⟨⊥, bot_le⟩⟩
    ∀ C : StoneSpectrum (Set.Iic a), IsQuasipoint {b : L | ∃ c ∈ C.val, c.val ≤ b} := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P20

Source

H. F. de Groote, Observables I: Stone Spectra, arXiv:math-ph/0509020v1, https://arxiv.org/pdf/math-ph/0509020v1, proof of Proposition 3.21, printed p.65 (PDF p.66), principal-ideal spectrum correspondence. This supporting lemma isolates the upward extension and records its weaker order-theoretic assumptions.

View graph