Proposition 3.18
OpenQAlgorithms.Papers.Independent.Intakethird100.P20.second_category_spectrum_homeomorphismFor a Baire space , the saturation map is a homeomorphism onto the subspace of second-category Borel quasipoints:
Here consists of quasipoints containing no meagre Borel set and carries the subspace topology. The target is not the full Borel Stone spectrum.
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P20
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.18; de Groote, Observables I, PDF p./pp. 58.
-/
theorem second_category_spectrum_homeomorphism {M : Type u} [TopologicalSpace M] [BaireSpace M] :
∃ h : StoneSpectrum (Opens M) ≃ₜ
{C : StoneSpectrum (BorelSets M) // ∀ A ∈ C.val, ¬ IsMeagre A.val},
∀ B, (h B).val.val = borelSaturation B := by sorry
end QAlgorithms.Papers.Independent.Intakethird100.P20
end
Read-back
What the Lean code literally says, in plain math · gpt-6.1-sol
For every Baire topological space , there exists a homeomorphism from the quasipoints of the open subsets of onto the quasipoints of its Borel subsets whose every member is nonmeagre. Here, for either collection of subsets, a quasipoint is a nonempty family excluding , every pair of whose members contains a common member of the family, maximal under inclusion among families with these properties. Each quasipoint space has the topology generated by the sets of quasipoints containing a specified open set or a specified Borel set, respectively; the target carries the subspace topology on the quasipoints with only nonmeagre members. The homeomorphism satisfies, for every open-set quasipoint ,
where the equality identifies a quasipoint with its underlying family of sets.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.