MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralHomeomorph.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-/6import MathlibAnnex.Analysis.CStarAlgebra.Spectrum.Topology7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.SpectralComparison8import MathlibAnnex.Topology.ClosureSpace.HullKernelMap910/-!11# Ordinary homeomorphisms in spectral reconstruction1213Prim and Spec already have their independent ordinary topologies. Psi preserves14incidence in the ORIGINAL algebra, hence both hull-kernel closures. Phi preserves15closures because the representation kernels agree with J_C and both closures are16pullbacks along their respective kernel maps. Topologizability on the geometric17side is then proved. The final maps are ordinary `Homeomorph`s, not just bijections18or closure-space maps. No T0 or injectivity assumption on kappa is inserted.19-/2021set_option autoImplicit false22noncomputable section23open Set2425namespace MathlibAnnex.Analysis.CStarAlgebra2627universe u28variable (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]29variable [Nontrivial A]3031/-- The independent primitive comparison preserves the whole hull-kernel closure. -/32def primitiveSpectrumClosureHomeomorph :33    ClosureSpace.Homeomorph (primitiveSpectrumClosure A)34      (NormedSpace.primitiveGeometricSpectrumClosure ℂ A) :=35  ClosureSpace.HullKernel.homeomorphOfMemIff36    (univ_notMem_primitiveKernelFamily A)37    (NormedSpace.univ_notMem_primitiveGeometricSpectrumFamily ℂ A)38    (Equiv.refl A) (primitiveSpectrumEquivGeometric A) (fun _ _ => Iff.rfl)3940/-- Forward preservation, on EVERY selection including the empty set. -/41theorem image_primitiveSpectrumClosure (S : Set (PrimitiveSpectrum A)) :42    primitiveSpectrumEquivGeometric A '' (primitiveSpectrumClosure A).closure S =43      (NormedSpace.primitiveGeometricSpectrumClosure ℂ A).closure44        (primitiveSpectrumEquivGeometric A '' S) :=45  (primitiveSpectrumClosureHomeomorph A).image_closure S4647/-- Explicit inverse preservation; the carrier identity is used in both directions. -/48theorem image_symm_primitiveGeometricSpectrumClosure49    (S : Set (NormedSpace.PrimitiveGeometricSpectrum ℂ A)) :50    (primitiveSpectrumEquivGeometric A).symm ''51        (NormedSpace.primitiveGeometricSpectrumClosure ℂ A).closure S =52      (primitiveSpectrumClosure A).closure ((primitiveSpectrumEquivGeometric A).symm '' S) :=53  (primitiveSpectrumClosureHomeomorph A).symm.image_closure S5455/-- The actual bijection Phi preserves closure, via the kernel equality and56not by transporting the definition of the source topology. -/57theorem image_irreducibleSpectrumClosure (S : Set (IrreducibleSpectrum A)) :58    IrreducibleSpectrum.equivGeometricSpectrum '' (irreducibleSpectrumClosure A).closure S =59      (NormedSpace.geometricSpectrumClosure ℂ A).closure60        (IrreducibleSpectrum.equivGeometricSpectrum '' S) := by61  let e : IrreducibleSpectrum A ≃ NormedSpace.GeometricSpectrum ℂ A :=62    IrreducibleSpectrum.equivGeometricSpectrum63  rw [irreducibleSpectrumClosure_closure, NormedSpace.geometricSpectrumClosure_closure]64  ext C65  constructor66  · rintro ⟨q, hq, rfl⟩ a ha67    rw [geometricSpectrumKernel_equivGeometricSpectrum]68    apply hq a69    intro r hr70    have h := ha (e r) ⟨r, hr, rfl⟩71    exact (geometricSpectrumKernel_equivGeometricSpectrum A r) ▸ h72  · intro hC73    refine ⟨e.symm C, ?_, e.apply_symm_apply C⟩74    intro a ha75    rw [← geometricSpectrumKernel_equivGeometricSpectrum A (e.symm C)]76    change a ∈ NormedSpace.geometricSpectrumKernel ℂ A (e (e.symm C))77    rw [e.apply_symm_apply]78    apply hC a79    rintro D ⟨q, hq, rfl⟩80    rw [geometricSpectrumKernel_equivGeometricSpectrum]81    exact ha q hq8283/-- The closure-space homeomorphism is proved before passing to ordinary topologies. -/84def irreducibleSpectrumClosureHomeomorph :85    ClosureSpace.Homeomorph (irreducibleSpectrumClosure A)86      (NormedSpace.geometricSpectrumClosure ℂ A) :=87  ClosureSpace.Homeomorph.ofImageClosure _ _ IrreducibleSpectrum.equivGeometricSpectrum88    (image_irreducibleSpectrumClosure A)8990theorem image_symm_geometricSpectrumClosure (S : Set (NormedSpace.GeometricSpectrum ℂ A)) :91    (IrreducibleSpectrum.equivGeometricSpectrum (A := A)).symm ''92        (NormedSpace.geometricSpectrumClosure ℂ A).closure S =93      (irreducibleSpectrumClosure A).closure94        ((IrreducibleSpectrum.equivGeometricSpectrum (A := A)).symm '' S) :=95  (irreducibleSpectrumClosureHomeomorph A).symm.image_closure S9697/-- Paper 5.12 for PS(A), from proved primitive-kernel primality and Psi. -/98theorem isTopologizable_primitiveGeometricSpectrumClosure :99    (NormedSpace.primitiveGeometricSpectrumClosure ℂ A).IsTopologizable :=100  (primitiveSpectrumClosureHomeomorph A).isTopologizable101    (isTopologizable_primitiveSpectrumClosure A)102103/-- Paper 5.12 for GS(A). This is not deduced from any separation axiom. -/104theorem isTopologizable_geometricSpectrumClosure :105    (NormedSpace.geometricSpectrumClosure ℂ A).IsTopologizable :=106  (irreducibleSpectrumClosureHomeomorph A).isTopologizable107    (isTopologizable_irreducibleSpectrumClosure A)108109/-- The ordinary topology with exactly the existing PS(A) closure. -/110def primitiveGeometricSpectrumTopology : TopologicalSpace (NormedSpace.PrimitiveGeometricSpectrum ℂ A) :=111  (NormedSpace.primitiveGeometricSpectrumClosure ℂ A).toTopologicalSpace112    (isTopologizable_primitiveGeometricSpectrumClosure A)113114/-- The ordinary topology with exactly the existing GS(A) closure. -/115def geometricSpectrumTopology : TopologicalSpace (NormedSpace.GeometricSpectrum ℂ A) :=116  (NormedSpace.geometricSpectrumClosure ℂ A).toTopologicalSpace117    (isTopologizable_geometricSpectrumClosure A)118119attribute [local instance] primitiveGeometricSpectrumTopology geometricSpectrumTopology120121/-- Gamma retains precisely its pullback topology on the geometric side. -/122theorem geometricSpectrumTopology_eq_induced :123    geometricSpectrumTopology A = TopologicalSpace.induced124      (NormedSpace.geometricSpectrumToPrimitive ℂ A) (primitiveGeometricSpectrumTopology A) :=125  ClosureSpace.toTopologicalSpace_induced _ (isTopologizable_primitiveGeometricSpectrumClosure A) _126127/-- Paper 5.11 on Prim, with ordinary forward AND inverse continuity. -/128def primitiveSpectrumHomeomorph :129    @_root_.Homeomorph (PrimitiveSpectrum A) (NormedSpace.PrimitiveGeometricSpectrum ℂ A)130      inferInstance (primitiveGeometricSpectrumTopology A) :=131  (primitiveSpectrumClosureHomeomorph A).toTopologicalHomeomorph132    (isTopologizable_primitiveSpectrumClosure A)133    (isTopologizable_primitiveGeometricSpectrumClosure A)134135/-- Paper 5.11 on Spec, in its ordinary topology induced by kappa. -/136def irreducibleSpectrumHomeomorph :137    @_root_.Homeomorph (IrreducibleSpectrum A) (NormedSpace.GeometricSpectrum ℂ A)138      inferInstance (geometricSpectrumTopology A) :=139  (irreducibleSpectrumClosureHomeomorph A).toTopologicalHomeomorph140    (isTopologizable_irreducibleSpectrumClosure A) (isTopologizable_geometricSpectrumClosure A)141142@[simp]143theorem primitiveSpectrumHomeomorph_toEquiv :144    (primitiveSpectrumHomeomorph A).toEquiv = primitiveSpectrumEquivGeometric A := rfl145146@[simp]147theorem irreducibleSpectrumHomeomorph_toEquiv :148    (irreducibleSpectrumHomeomorph A).toEquiv = IrreducibleSpectrum.equivGeometricSpectrum := rfl149150/-- The natural formula is unchanged on passing to the ordinary homeomorphism. -/151theorem irreducibleSpectrumHomeomorph_ofPureState (phi : NonUnitalPureState A) :152    irreducibleSpectrumHomeomorph A (IrreducibleSpectrum.ofPureState phi) =153      NormedSpace.toGeometricSpectrum ℂ A phi.geometricPoint := rfl154155/-- The commuting square for the ordinary homeomorphisms, not just abstract bijections. -/156theorem primitiveSpectrumHomeomorph_kernel (q : IrreducibleSpectrum A) :157    primitiveSpectrumHomeomorph A (IrreducibleSpectrum.kernel q) =158      NormedSpace.geometricSpectrumToPrimitive ℂ A (irreducibleSpectrumHomeomorph A q) :=159  primitiveSpectrumEquivGeometric_kernel A q160161/-- Ordinary closure on GS(A) agrees with its original, unmodified closure space. -/162theorem closure_geometricSpectrumTopology (S : Set (NormedSpace.GeometricSpectrum ℂ A)) :163    @_root_.closure _ (geometricSpectrumTopology A) S =164      (NormedSpace.geometricSpectrumClosure ℂ A).closure S :=165  ClosureSpace.closure_toTopologicalSpace _ _ S166167/-- Ordinary closure on PS(A) agrees with its original, unmodified hull-kernel closure. -/168theorem closure_primitiveGeometricSpectrumTopology169    (S : Set (NormedSpace.PrimitiveGeometricSpectrum ℂ A)) :170    @_root_.closure _ (primitiveGeometricSpectrumTopology A) S =171      (NormedSpace.primitiveGeometricSpectrumClosure ℂ A).closure S :=172  ClosureSpace.closure_toTopologicalSpace _ _ S173174end MathlibAnnex.Analysis.CStarAlgebra