MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SpectralPreserver.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.GeometricStructure.SpectralHomeomorph7import MathlibAnnex.Analysis.Normed.GeometricStructure.SpectrumMap89/-!10# Spectral homeomorphisms induced by a geometric-structure homeomorphism1112Compose the independently established ordinary spectral comparisons with13MAIN's received full-closure G/P transport. These are the (primitive) spectral14homeomorphisms of Corollary 5.13. The hypothesis is the original GSS closure15homeomorphism, not a separately supplied spectral bijection. No linear map,16star isomorphism, equality of Hilbert dimensions or faithful action is assumed.17-/1819set_option autoImplicit false20noncomputable section2122namespace MathlibAnnex.Analysis.CStarAlgebra2324attribute [local instance] primitiveGeometricSpectrumTopology geometricSpectrumTopology2526universe u v27variable {A : Type u} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A]28variable {B : Type v} [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [Nontrivial B]29variable (e : ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)30  (NormedSpace.geometricStructureClosure ℂ B))3132/-- Corollary 5.13: ordinary homeomorphism of the actual irreducible spectra. -/33def irreducibleSpectrumHomeomorphOfGeometricStructure : IrreducibleSpectrum A ≃ₜ IrreducibleSpectrum B :=34  (irreducibleSpectrumHomeomorph A).trans35    (((NormedSpace.geometricSpectrumHomeomorph e).toTopologicalHomeomorph36      (isTopologizable_geometricSpectrumClosure A) (isTopologizable_geometricSpectrumClosure B)).trans37        (irreducibleSpectrumHomeomorph B).symm)3839/-- Corollary 5.13: ordinary homeomorphism of the actual primitive ideal spectra. -/40def primitiveSpectrumHomeomorphOfGeometricStructure : PrimitiveSpectrum A ≃ₜ PrimitiveSpectrum B :=41  (primitiveSpectrumHomeomorph A).trans42    (((NormedSpace.primitiveGeometricSpectrumHomeomorph e).toTopologicalHomeomorph43      (isTopologizable_primitiveGeometricSpectrumClosure A)44      (isTopologizable_primitiveGeometricSpectrumClosure B)).trans45        (primitiveSpectrumHomeomorph B).symm)4647/-- The underlying maps are the stated compositions, rather than new chosen bijections. -/48theorem irreducibleSpectrumHomeomorphOfGeometricStructure_apply (q : IrreducibleSpectrum A) :49    irreducibleSpectrumHomeomorphOfGeometricStructure e q =50      (IrreducibleSpectrum.equivGeometricSpectrum (A := B)).symm51        ((NormedSpace.geometricSpectrumHomeomorph e).toEquiv52          (IrreducibleSpectrum.equivGeometricSpectrum q)) := rfl5354theorem primitiveSpectrumHomeomorphOfGeometricStructure_apply (P : PrimitiveSpectrum A) :55    primitiveSpectrumHomeomorphOfGeometricStructure e P =56      (primitiveSpectrumEquivGeometric B).symm57        ((NormedSpace.primitiveGeometricSpectrumHomeomorph e).toEquiv58          (primitiveSpectrumEquivGeometric A P)) := rfl5960/-- The two actual spectral homeomorphisms commute with their kernel maps. -/61theorem kernel_irreducibleSpectrumHomeomorphOfGeometricStructure (q : IrreducibleSpectrum A) :62    IrreducibleSpectrum.kernel (irreducibleSpectrumHomeomorphOfGeometricStructure e q) =63      primitiveSpectrumHomeomorphOfGeometricStructure e (IrreducibleSpectrum.kernel q) := by64  apply (primitiveSpectrumEquivGeometric B).injective65  rw [primitiveSpectrumEquivGeometric_kernel,66    primitiveSpectrumHomeomorphOfGeometricStructure_apply,67    Equiv.apply_symm_apply, irreducibleSpectrumHomeomorphOfGeometricStructure_apply,68    Equiv.apply_symm_apply,69    NormedSpace.geometricSpectrumToPrimitive_geometricSpectrumHomeomorph,70    primitiveSpectrumEquivGeometric_kernel]7172include e in73/-- Existence form of Corollary 5.13, keeping both ordinary topological conclusions. -/74theorem nonempty_spectralHomeomorphs_of_geometricStructure :75    Nonempty (IrreducibleSpectrum A ≃ₜ IrreducibleSpectrum B) ∧76      Nonempty (PrimitiveSpectrum A ≃ₜ PrimitiveSpectrum B) :=77  ⟨⟨irreducibleSpectrumHomeomorphOfGeometricStructure e⟩,78    ⟨primitiveSpectrumHomeomorphOfGeometricStructure e⟩⟩7980end MathlibAnnex.Analysis.CStarAlgebra