MathlibAnnex/Analysis/CStarAlgebra/Spectrum/Topology.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.Primitive7import MathlibAnnex.Topology.ClosureSpace.HullKernel8import MathlibAnnex.Topology.ClosureSpace.TopologicalMaps910/-!11# Ordinary hull-kernel and irreducible-spectrum topologies1213Finite-union preservation is proved using meet-primality of the actual14representation kernels. T0 by itself would not suffice. Empty selections15have the genuine top ideal as their intersection. The topology on the16irreducible spectrum is the pullback along kappa, not the quotient of any17weak-star topology and not a topology transported from geometric spectra.18-/1920set_option autoImplicit false21noncomputable section22open Set2324namespace MathlibAnnex.Analysis.CStarAlgebra2526universe u27variable (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A]2829/-- The hull-kernel closure on the independently constructed primitive family. -/30def primitiveSpectrumClosure : ClosureSpace (PrimitiveSpectrum A) :=31  ClosureSpace.HullKernel.space (primitiveKernelFamily A) (univ_notMem_primitiveKernelFamily A)3233namespace PrimitiveSpectrum34variable {A}3536/-- The intersection of the ACTUAL two-sided ideals selected by S. -/37def kernelIntersection (S : Set (PrimitiveSpectrum A)) : TwoSidedIdeal A :=38  ⨅ P : S, P.val.toTwoSidedIdeal3940@[simp]41theorem mem_kernelIntersection (S : Set (PrimitiveSpectrum A)) (a : A) :42    a ∈ kernelIntersection S ↔ ∀ P : PrimitiveSpectrum A, P ∈ S → a ∈ P.val := by43  simp only [kernelIntersection, TwoSidedIdeal.mem_iInf, mem_toTwoSidedIdeal, Subtype.forall]4445@[simp]46theorem kernelIntersection_empty : kernelIntersection (∅ : Set (PrimitiveSpectrum A)) = ⊤ := by47  apply TwoSidedIdeal.ext48  intro a49  simp only [mem_kernelIntersection, Set.mem_empty_iff_false, false_implies, implies_true,50    TwoSidedIdeal.mem_top]5152theorem kernelIntersection_union (S T : Set (PrimitiveSpectrum A)) :53    kernelIntersection (S ∪ T) = kernelIntersection S ⊓ kernelIntersection T := by54  apply TwoSidedIdeal.ext55  intro a56  simp only [mem_kernelIntersection, TwoSidedIdeal.mem_inf, Set.mem_union]57  constructor58  · intro h59    exact ⟨fun P hP => h P (Or.inl hP), fun P hP => h P (Or.inr hP)⟩60  · rintro ⟨hS, hT⟩ P (hP | hP)61    · exact hS P hP62    · exact hT P hP6364theorem coe_kernelIntersection (S : Set (PrimitiveSpectrum A)) :65    (kernelIntersection S : Set A) = ClosureSpace.HullKernel.kernel (primitiveKernelFamily A) S := by66  ext a67  exact mem_kernelIntersection S a6869theorem mem_primitiveSpectrumClosure_iff (S : Set (PrimitiveSpectrum A)) (P : PrimitiveSpectrum A) :70    P ∈ (primitiveSpectrumClosure A).closure S ↔ kernelIntersection S ≤ P.toTwoSidedIdeal := by71  change ClosureSpace.HullKernel.kernel (primitiveKernelFamily A) S ⊆ P.val ↔ _72  rw [← coe_kernelIntersection, ← P.coe_toTwoSidedIdeal]73  rfl7475end PrimitiveSpectrum7677/-- The nontrivial topological axiom follows from actual primitive-kernel78meet-primality. No order-generating assumption on ALL two-sided ideals is needed. -/79theorem primitiveSpectrumClosure_union (S T : Set (PrimitiveSpectrum A)) :80    (primitiveSpectrumClosure A).closure (S ∪ T) =81      (primitiveSpectrumClosure A).closure S ∪ (primitiveSpectrumClosure A).closure T := by82  ext P83  rw [PrimitiveSpectrum.mem_primitiveSpectrumClosure_iff,84    PrimitiveSpectrum.kernelIntersection_union, P.inf_le_toTwoSidedIdeal_iff,85    Set.mem_union, PrimitiveSpectrum.mem_primitiveSpectrumClosure_iff,86    PrimitiveSpectrum.mem_primitiveSpectrumClosure_iff]8788theorem isTopologizable_primitiveSpectrumClosure : (primitiveSpectrumClosure A).IsTopologizable :=89  primitiveSpectrumClosure_union A9091/-- The usual hull-kernel topology on actual primitive kernels. -/92instance PrimitiveSpectrum.instTopologicalSpace : TopologicalSpace (PrimitiveSpectrum A) :=93  (primitiveSpectrumClosure A).toTopologicalSpace (isTopologizable_primitiveSpectrumClosure A)9495/-- The ordinary topological closure is literally the hull of the kernel. -/96theorem closure_primitiveSpectrum (S : Set (PrimitiveSpectrum A)) :97    _root_.closure S = {P | ∀ a : A, (∀ Q : PrimitiveSpectrum A, Q ∈ S → a ∈ Q.val) → a ∈ P.val} :=98  ClosureSpace.closure_toTopologicalSpace _ _ S99100/-- The equivalent ideal-valued ordinary closure formula. -/101theorem mem_closure_primitiveSpectrum_iff (S : Set (PrimitiveSpectrum A)) (P : PrimitiveSpectrum A) :102    P ∈ _root_.closure S ↔ PrimitiveSpectrum.kernelIntersection S ≤ P.toTwoSidedIdeal := by103  rw [ClosureSpace.closure_toTopologicalSpace]104  exact PrimitiveSpectrum.mem_primitiveSpectrumClosure_iff S P105106/-- The independent irreducible-spectrum closure is induced by the actual kappa. -/107def irreducibleSpectrumClosure : ClosureSpace (IrreducibleSpectrum A) :=108  (primitiveSpectrumClosure A).induced IrreducibleSpectrum.kernel109110theorem isTopologizable_irreducibleSpectrumClosure :111    (irreducibleSpectrumClosure A).IsTopologizable :=112  ClosureSpace.isTopologizable_induced (isTopologizable_primitiveSpectrumClosure A) _113114/-- The pullback closure written without image or preimage notation. -/115theorem irreducibleSpectrumClosure_closure (S : Set (IrreducibleSpectrum A)) :116    (irreducibleSpectrumClosure A).closure S =117      {q | ∀ a : A, (∀ r : IrreducibleSpectrum A, r ∈ S →118        a ∈ (IrreducibleSpectrum.kernel r).val) → a ∈ (IrreducibleSpectrum.kernel q).val} := by119  ext q120  change (∀ a : A, (∀ P : PrimitiveSpectrum A,121    P ∈ IrreducibleSpectrum.kernel '' S → a ∈ P.val) →122      a ∈ (IrreducibleSpectrum.kernel q).val) ↔ _123  constructor124  · intro h a ha125    apply h a126    rintro P ⟨r, hr, rfl⟩127    exact ha r hr128  · intro h a ha129    exact h a (fun r hr => ha (IrreducibleSpectrum.kernel r) ⟨r, hr, rfl⟩)130131/-- The spectrum topology, constructed from the kernel pullback. -/132instance IrreducibleSpectrum.instTopologicalSpace : TopologicalSpace (IrreducibleSpectrum A) :=133  (irreducibleSpectrumClosure A).toTopologicalSpace (isTopologizable_irreducibleSpectrumClosure A)134135/-- This equality rules out accidentally using the pure-state quotient topology. -/136theorem irreducibleSpectrum_topology_eq_induced :137    (IrreducibleSpectrum.instTopologicalSpace A) =138      TopologicalSpace.induced IrreducibleSpectrum.kernel (PrimitiveSpectrum.instTopologicalSpace A) :=139  ClosureSpace.toTopologicalSpace_induced _ (isTopologizable_primitiveSpectrumClosure A) _140141theorem closure_irreducibleSpectrum (S : Set (IrreducibleSpectrum A)) :142    _root_.closure S = IrreducibleSpectrum.kernel ⁻¹'143      _root_.closure (IrreducibleSpectrum.kernel '' S) := by144  rw [ClosureSpace.closure_toTopologicalSpace, ClosureSpace.closure_toTopologicalSpace]145  rfl146147/-- Ordinary continuity of kappa, with no injectivity assertion. -/148theorem continuous_irreducibleSpectrum_kernel :149    Continuous (IrreducibleSpectrum.kernel : IrreducibleSpectrum A → PrimitiveSpectrum A) := by150  apply (ClosureSpace.continuous_toTopologicalSpace_iff _ _151    (isTopologizable_irreducibleSpectrumClosure A)152    (isTopologizable_primitiveSpectrumClosure A) _).2153  exact ClosureSpace.continuous_induced _ _154155/-- Surjectivity, rather than injectivity, gives the exact image-closure identity. -/156theorem image_closure_irreducibleSpectrum_kernel (S : Set (IrreducibleSpectrum A)) :157    IrreducibleSpectrum.kernel '' _root_.closure S =158      _root_.closure (IrreducibleSpectrum.kernel '' S) := by159  rw [ClosureSpace.closure_toTopologicalSpace, ClosureSpace.closure_toTopologicalSpace]160  exact ClosureSpace.image_induced_closure _ _ IrreducibleSpectrum.kernel_surjective S161162end MathlibAnnex.Analysis.CStarAlgebra