Prove2Me

Proposition 3.16

Open
QAlgorithms.Papers.Independent.Intakethird100.P20.regularization_homeomorphism

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

prove2quantum

For every topological space MM, the canonical regularization map is a homeomorphism:

Q(T(M))→ ≅ Q(Tr(M)),B⟼{int⁡U‾:U∈B}.Q(T(M))\xrightarrow{\ \cong\ }Q(T_r(M)),\qquad \mathfrak B\longmapsto\{\operatorname{int}\overline U:U\in\mathfrak B\}.

This identifies the spectra even when the open-set and regular-open lattices themselves are not isomorphic.

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

/-- Proposition 3.16; de Groote, Observables I, PDF p./pp. 56.
-/
theorem regularization_homeomorphism {M : Type u} [TopologicalSpace M] :
    ∃ h : StoneSpectrum (Opens M) ≃ₜ StoneSpectrum (RegularOpens M),
      ∀ B, (h B).val = regularizedBase B := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P20

end
Source
Observables I: Stone Spectra, arXiv:math-ph/0509020v1, PDF p. 56, Proposition 3.16
Read-back

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

Let MM be any topological space, let O(M)\mathcal O(M) be its open subsets, and let R(M)={V∈O(M):int⁡(V‾)=V}\mathcal R(M)=\{V\in\mathcal O(M):\operatorname{int}(\overline V)=V\} be its regular open subsets; both are ordered by inclusion with bottom ∅\varnothing. For either collection AA, define Q(A)\mathcal Q(A) to consist of the inclusion-maximal nonempty families B⊆AB\subseteq A that exclude ∅\varnothing and such that any two members contain a common member of BB, and equip Q(A)\mathcal Q(A) with the topology generated by {B:U∈B}\{B:U\in B\} for U∈AU\in A. There exists a homeomorphism h:Q(O(M))→Q(R(M))h:\mathcal Q(\mathcal O(M))\to\mathcal Q(\mathcal R(M)) such that, for every B∈Q(O(M))B\in\mathcal Q(\mathcal O(M)),

h(B)={V∈R(M):∃U∈B, int⁡(U‾)=V}.h(B)=\{V\in\mathcal R(M):\exists U\in B,\ \operatorname{int}(\overline U)=V\}.

No separation or nonemptiness assumption is imposed on MM; the empty space is included.

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