compact-point-map-not-open

Open

QAlgorithms.Papers.Independent.Intakethird100.P20.compact_connected_point_map_not_open

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

prove2quantum

Let $M$ be a connected compact Hausdorff space with at least two points. Its canonical point map from $Q(T(M))$ is continuous, surjective and closed, but

\operatorname{pt}:Q(T(M))\to M\quad\text{is not open}.

The map is characterized by the singleton intersection of closures of each quasipoint's members. The nontriviality condition excludes the singleton exception.

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

/-- compact-point-map-not-open; de Groote, Observables I, PDF p./pp. 56, 57.
-/
theorem compact_connected_point_map_not_open {M : Type u} [TopologicalSpace M] [CompactSpace M] [T2Space M]
    [ConnectedSpace M] [Nontrivial M] :
    ∃ pt : StoneSpectrum (Opens M) → M, (∀ B, LiesOver B (pt B)) ∧
      Continuous pt ∧ Function.Surjective pt ∧ IsClosedMap pt ∧ ¬ IsOpenMap pt := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end

Source

Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 56, compact-point-map-not-open

Read-back

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

Let $M$ be a compact Hausdorff connected topological space with at least two distinct points. 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 continuous, surjective, and a closed map, but is not an open map. Thus images of all closed subsets under this $p$ are closed, while at least one open subset has an image that is not open.

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