MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ElementaryFiniteDimensionalRigidity.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-/67import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.CompactRepresentationRigidity8import MathlibAnnex.Analysis.CStarAlgebra.Representation.ElementaryCompact9import MathlibAnnex.Analysis.CStarAlgebra.Representation.FiniteDimensionalCompact1011/-!12# Elementary and finite-dimensional geometric structure rigidity1314The one-sided compact representation theorem yields two symmetric corollaries.15An exact elementary model supplies the actual representation16`NonUnitalCStarRepresentation.ofCompactOperatorEquiv`. A finite-dimensional17algebra supplies the already constructed finite separating GNS sum. The other18algebra is not assumed compact, elementary, or finite-dimensional.1920The elementary existence statement spells out the paper's definition: there21is a complete complex Hilbert space and a star equivalence with its compact22operator algebra. Its Hilbert carrier and structures are explicitly quantified;23the two possible model universes are independent of both algebra universes.24No new predicate named `IsElementary` is introduced, and no equivalence with25an independently axiomatized elementary-algebra predicate is presumed. A given26exact representation model is also supported without replacing its action.2728The finite-dimensional disjunction is a proposition. Each branch installs29only the finite-dimensional instance that the branch actually supplies.30Finite GNS separation, compactness, and all model and density inputs are proved31by the existing producers, not supplied as extra hypotheses of the corollaries.3233Zero algebras and zero Hilbert models are allowed. No unit, nontriviality,34nonempty spectrum, countability, or separability is assumed. Auxiliary spectral35orders are local to the proof that uses the finite GNS representation.3637All conclusions concern existence of a star equivalence. They do not say that38such an equivalence induces a specified nonlinear GSS homeomorphism, or that39the star equivalence is unique. The forward implications use the full closure40homeomorphism induced by a star equivalence, not a finite-closure replacement.41-/4243@[expose] public section44set_option autoImplicit false45noncomputable section4647namespace MathlibAnnex.Analysis.CStarAlgebra4849universe u v w z5051variable {A : Type u} {B : Type v}52variable [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B]5354section GivenModel5556variable {H : Type w} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]5758/-- A specified exact compact-operator model supplies the same actual faithful59compact representation to the general rigidity theorem. No model or compactness60of the other algebra is required, and the zero model is not excluded. -/61theorem nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_compactOperatorEquiv62    (E : A ≃⋆ₐ[ℂ] ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H) :63    Nonempty (A ≃⋆ₐ[ℂ] B) ↔64      Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)65        (NormedSpace.geometricStructureClosure ℂ B)) := by66  exact nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_isCompactlyRepresented67    (NonUnitalCStarRepresentation.ofCompactOperatorEquiv E)68    (NonUnitalCStarRepresentation.isCompactlyRepresented_ofCompactOperatorEquiv E)6970/-- The given-representation version uses the original exact model `pi` itself.71Its established injectivity and pointwise compactness are the two inputs to72the general theorem; no second representation is chosen. -/73theorem nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_isCompactOperatorModel74    (pi : NonUnitalCStarRepresentation A H) (hpi : IsCompactOperatorModel pi) :75    Nonempty (A ≃⋆ₐ[ℂ] B) ↔76      Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)77        (NormedSpace.geometricStructureClosure ℂ B)) := by78  exact nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_isCompactlyRepresented79    pi ⟨hpi.1, hpi.2.1⟩8081end GivenModel8283/-- Either algebra may have an elementary model, with its Hilbert carrier and84structures explicitly quantified in independently specified universes. This is85the model-existence formulation of elementary, not an additional model premise86attached to an unrelated elementary predicate. The right branch uses the inverse87GSS homeomorphism and then reverses the resulting star equivalence. -/88theorem nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_exists_compactOperatorEquiv89    (hModel :90      (∃ (H : Type w) (normed : NormedAddCommGroup H),91        letI : NormedAddCommGroup H := normed92        ∃ inner : InnerProductSpace ℂ H,93          letI : InnerProductSpace ℂ H := inner94          ∃ complete : CompleteSpace H,95            letI : CompleteSpace H := complete96            Nonempty (A ≃⋆ₐ[ℂ] ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)) ∨97      (∃ (K : Type z) (normed : NormedAddCommGroup K),98        letI : NormedAddCommGroup K := normed99        ∃ inner : InnerProductSpace ℂ K,100          letI : InnerProductSpace ℂ K := inner101          ∃ complete : CompleteSpace K,102            letI : CompleteSpace K := complete103            Nonempty (B ≃⋆ₐ[ℂ] ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K))) :104    Nonempty (A ≃⋆ₐ[ℂ] B) ↔105      Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)106        (NormedSpace.geometricStructureClosure ℂ B)) := by107  constructor108  · rintro ⟨E⟩109    exact ⟨geometricStructureHomeomorphOfStarAlgEquiv E⟩110  · rintro ⟨e⟩111    rcases hModel with hA | hB112    · rcases hA with ⟨H, normed, inner, complete, ⟨E⟩⟩113      letI : NormedAddCommGroup H := normed114      letI : InnerProductSpace ℂ H := inner115      letI : CompleteSpace H := complete116      exact117        (nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_compactOperatorEquiv118          (B := B) E).mpr ⟨e⟩119    · rcases hB with ⟨K, normed, inner, complete, ⟨E⟩⟩120      letI : NormedAddCommGroup K := normed121      letI : InnerProductSpace ℂ K := inner122      letI : CompleteSpace K := complete123      obtain ⟨F⟩ :=124        (nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_compactOperatorEquiv125          (B := A) E).mpr ⟨e.symm⟩126      exact ⟨F.symm⟩127128/-- Finite-dimensionality of the source alone supplies a finite separating GNS129selection and its actual faithful compact action. Neither the selection nor130its separating or compactness properties are hypotheses of this theorem. -/131theorem nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_finiteDimensional132    [FiniteDimensional ℂ A] :133    Nonempty (A ≃⋆ₐ[ℂ] B) ↔134      Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)135        (NormedSpace.geometricStructureClosure ℂ B)) := by136  letI : PartialOrder A := _root_.CStarAlgebra.spectralOrder A137  letI : StarOrderedRing A := _root_.CStarAlgebra.spectralOrderedRing A138  obtain ⟨s, hs⟩ :=139    PrimitiveSpectrum.exists_finset_isCompactlyRepresented_finiteGNSRepresentation (A := A)140  exact nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_isCompactlyRepresented141    (PrimitiveSpectrum.finiteGNSRepresentation (A := A) s) hs142143/-- The symmetric finite-dimensional corollary, including the zero algebra.144Only one of the two finite-dimensional instances is installed in each branch.145The specified nonlinear GSS homeomorphism is used to prove existence, not146claimed to be the map induced by the resulting star equivalence. -/147theorem nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_finiteDimensional_or148    (hfinite : FiniteDimensional ℂ A ∨ FiniteDimensional ℂ B) :149    Nonempty (A ≃⋆ₐ[ℂ] B) ↔150      Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)151        (NormedSpace.geometricStructureClosure ℂ B)) := by152  constructor153  · rintro ⟨E⟩154    exact ⟨geometricStructureHomeomorphOfStarAlgEquiv E⟩155  · rintro ⟨e⟩156    rcases hfinite with hA | hB157    · letI : FiniteDimensional ℂ A := hA158      exact159        (nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_finiteDimensional160          (A := A) (B := B)).mpr ⟨e⟩161    · letI : FiniteDimensional ℂ B := hB162      obtain ⟨F⟩ :=163        (nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_finiteDimensional164          (A := B) (B := A)).mpr ⟨e.symm⟩165      exact ⟨F.symm⟩166167end MathlibAnnex.Analysis.CStarAlgebra