Corollary 3.5

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.compact_space_canonical_point_quotient

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

prove2quantum

For a compact Hausdorff space $M$ , each quasipoint of $T(M)$ lies over a unique point, defining a canonical continuous surjection $\operatorname{pt}:Q(T(M))\to M$ with

\bigcap_{U\in\mathfrak B}\overline U=\{\operatorname{pt}(\mathfrak B)\}.

This map is a quotient map: its induced quotient topology is the given topology on $M$ . The empty space is allowed.

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

/-- Corollary 3.5; de Groote, Observables I, PDF p./pp. 56.
-/
theorem compact_space_canonical_point_quotient {M : Type u} [TopologicalSpace M] [CompactSpace M] [T2Space M] :
    ∃ pt : StoneSpectrum (Opens M) → M,
      (∀ B, LiesOver B (pt B)) ∧ Function.Surjective pt ∧
        Continuous pt ∧ Topology.IsQuotientMap pt := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 56, Corollary 3.5

Read-back

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

Let $M$ be a compact Hausdorff topological space. Let $\mathcal Q(\mathcal O(M))$ consist of the inclusion-maximal nonempty families $B$ of open subsets of $M$ that exclude $\varnothing$ and such that any two members contain a common member of $B$ , with topology generated by $\{B:U\in B\}$ for open $U\subseteq M$ . There exists a function $p:\mathcal Q(\mathcal O(M))\to M$ such that

\forall B\in\mathcal Q(\mathcal O(M)),\qquad \bigcap_{U\in B}\overline U=\{p(B)\},

and $p$ is surjective, continuous, and a quotient map: a subset $A\subseteq M$ is open if and only if $p^{-1}(A)$ is open. The statement includes the empty compact Hausdorff space.

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