MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/CStarRealization.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6module78public import Mathlib.Analysis.CStarAlgebra.Classes9public import MathlibAnnex.Analysis.Normed.GeometricStructure.Basic10public import MathlibAnnex.Topology.ClosureSpace.FiniteConjugation1112/-!13# Closure spaces realized by nontrivial complex C-star algebras1415`ClosureCat.IsCStarRealizable.{uA,uX} X` uses an actual algebra of carrier16universe `uA`, its actual nonunital C-star algebra structure, a nontriviality17proof and an actual homeomorphism from its face-defined geometric structure18space to `X`. The carrier of `X` has the independent universe `uX`.1920This is the object predicate in Definition 7.4 of arXiv:2504.05551v1. It is21homeomorphism-closed, including across carrier universes, and hence invariant22under the existing categorical isomorphisms. No categorical wrapper is needed23for the class-relative property: use24`c.HasContinuousFiniteConjugation (ClosureCat.IsCStarRealizable.{uA,uX})`.25That expression quantifies over ALL eligible objects of the indicated carrier26universe and ALL their component points, not over one selected algebra.2728No separability, unitality, order structure, choice of irreducible representation,29or assertion of the characterization of elementary algebras is part of the30witness. The pre-existing geometric structure space definition is unchanged.31-/3233@[expose] public section3435set_option autoImplicit false3637namespace ClosureCat3839/-- An actual nontrivial complex C-star algebra realization of a closure space.40The algebra's universe and the target carrier's universe are explicit and independent. -/41def IsCStarRealizable.{uA, uX} (X : ClosureCat.{uX}) : Prop :=42  ∃ (A : Type uA) (instA : NonUnitalCStarAlgebra A),43    letI : NonUnitalCStarAlgebra A := instA44    Nontrivial A ∧ Nonempty45      (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A) X.str)4647universe uA uX uY4849/-- Every nontrivial complex C-star algebra realizes its actual face-defined GSS. -/50theorem isCStarRealizable_geometricStructureSpace (A : Type uA)51    [NonUnitalCStarAlgebra A] [Nontrivial A] :52    IsCStarRealizable.{uA, uA}53      (ClosureCat.of (NormedSpace.GeometricStructureSpace ℂ A)54        (NormedSpace.geometricStructureClosure ℂ A)) :=55  ⟨A, inferInstance, inferInstance, ⟨ClosureSpace.Homeomorph.refl _⟩⟩5657/-- Transport the same witness algebra and its homeomorphism; there is no58new representation or replacement of the original geometric structure space. -/59theorem IsCStarRealizable.homeomorph {X : ClosureCat.{uX}} {Y : ClosureCat.{uY}}60    (hX : IsCStarRealizable.{uA, uX} X) (e : ClosureSpace.Homeomorph X.str Y.str) :61    IsCStarRealizable.{uA, uY} Y := by62  rcases hX with ⟨A, instA, hA, ⟨f⟩⟩63  letI : NonUnitalCStarAlgebra A := instA64  exact ⟨A, instA, hA, ⟨f.trans e⟩⟩6566/-- Homeomorphism-closedness in both directions, keeping the witness universe. -/67theorem isCStarRealizable_iff_of_homeomorph {X : ClosureCat.{uX}} {Y : ClosureCat.{uY}}68    (e : ClosureSpace.Homeomorph X.str Y.str) :69    IsCStarRealizable.{uA, uX} X ↔ IsCStarRealizable.{uA, uY} Y :=70  ⟨fun hX => hX.homeomorph e, fun hY => hY.homeomorph e.symm⟩7172/-- The object predicate is isomorphism-closed in the existing category of73closure spaces with fully continuous arrows. -/74theorem isCStarRealizable_iff_of_iso {X Y : ClosureCat.{uX}}75    (e : CategoryTheory.Iso X Y) :76    IsCStarRealizable.{uA, uX} X ↔ IsCStarRealizable.{uA, uX} Y :=77  isCStarRealizable_iff_of_homeomorph (ClosureCat.homeomorphOfIso e)7879end ClosureCat