MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ElementaryOfFiniteConjugation.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.Quotient.CompactIdealSeparation7import MathlibAnnex.Analysis.CStarAlgebra.Quotient.CompactAnnihilatingRepresentation8import MathlibAnnex.Analysis.CStarAlgebra.CompactModel9import Mathlib.Algebra.Star.StarAlgHom10import MathlibAnnex.Analysis.CStarAlgebra.CompactModelEquiv1112/-!13# Compact-model endpoints and the singular-state contradiction1415A received compact model has a genuine star-algebra equivalence onto the16existing compact subtype. This works for nonunital algebras; `StarAlgEquiv`17itself does not require a multiplicative unit. In finite Hilbert dimension,18the actual multiplier hypotheses prove such a compact model without any19quotient representation argument.2021The earlier partial theorem is retained unchanged, including its conditional22finite-dimensional clause. The new singular-state construction proves the23reverse compact inclusion in arbitrary Hilbert dimension. The final endpoint24uses the SAME pure-state witness and literal preimage homeomorphism returned25by the multiplier argument. No new representation of the original singleton26algebra is selected for the compact model. The separating action is constructed27on its literal image solely to obtain a contradiction.2829The compact algebra's singleton spectrum and the forward finite-conjugation30property remain independent obligations; this module does not redefine31`IsElementary` or assert the full equivalence in Paper 7.7.32-/3334set_option autoImplicit false35set_option maxHeartbeats 200000036set_option synthInstance.maxHeartbeats 20000037noncomputable section38open Set39open scoped CStarAlgebra4041namespace MathlibAnnex.Analysis.CStarAlgebra4243universe u v w z44variable {A : Type u} [NonUnitalCStarAlgebra A]45variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]4647section SingletonImage4849variable [PartialOrder A] [StarOrderedRing A]50local instance (pi : NonUnitalCStarRepresentation A H) :51    NonUnitalCStarAlgebra (NonUnitalStarAlgHom.range pi) :=52  NonUnitalStarSubalgebra.nonUnitalCStarAlgebra (NonUnitalStarAlgHom.range pi)53    (h_closed := HomKernelQuotient.isClosed_image pi)5455/-- In the same faithful multiplier image, a noncompact member would produce56an actual compact-annihilating irreducible action on that image. Pullback to57the original singleton algebra contradicts its rank-one detection theorem. -/58theorem isCompactOperator_map_of_singleton_of_image_mul_mem59    (hsingle : ∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q)60    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)61    (hinj : Function.Injective pi)62    (hmul : ∀ (b a : H →L[ℂ] H), a ∈ (NonUnitalStarAlgHom.range pi) →63      b * a ∈ (NonUnitalStarAlgHom.range pi) ∧ a * b ∈ (NonUnitalStarAlgHom.range pi)) :64    ∀ a : A, IsCompactOperator (pi a) := by65  intro a66  by_contra ha67  let s : (NonUnitalStarAlgHom.range pi) := (NonUnitalStarAlgHom.rangeRestrict pi) a68  obtain ⟨psi, hpsi, hpure, hann, _hbound, hpos⟩ :=69    exists_pureState_annihilating_compacts_of_not_isCompactOperator70      (NonUnitalStarSubalgebraClass.subtype (NonUnitalStarAlgHom.range pi)) s ha71  let f := positiveLinearMapOfMemStateSpace psi hpsi72  let rho : NonUnitalCStarRepresentation (NonUnitalStarAlgHom.range pi) f.GNS :=73    f.gnsStarAlgHom.toNonUnitalStarAlgHom.comp74      (Unitization.inrNonUnitalStarAlgHom ℂ (NonUnitalStarAlgHom.range pi))75  have hprops : rho.IsIrreducible ∧ rho s ≠ 0 ∧76      ∀ c : (NonUnitalStarAlgHom.range pi), IsCompactOperator (c : H →L[ℂ] H) → rho c = 0 :=77    isIrreducible_restriction_gns_of_pureState_annihilating78      (NonUnitalStarSubalgebraClass.subtype (NonUnitalStarAlgHom.range pi)) s psi hpsi hpure hann hpos79  exact (not_isIrreducible_of_image_annihilates_compacts80    hsingle pi hpi hinj hmul rho hprops.2.2) hprops.18182/-- No finite-dimensional or separability hypothesis is needed once the83same faithful image absorbs all bounded multipliers and has singleton spectrum. -/84theorem isCompactOperatorModel_of_singleton_of_image_mul_mem85    (hsingle : ∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q)86    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)87    (hinj : Function.Injective pi)88    (hmul : ∀ (b a : H →L[ℂ] H), a ∈ (NonUnitalStarAlgHom.range pi) →89      b * a ∈ (NonUnitalStarAlgHom.range pi) ∧ a * b ∈ (NonUnitalStarAlgHom.range pi)) :90    IsCompactOperatorModel pi := by91  exact ⟨hinj, isCompactOperator_map_of_singleton_of_image_mul_mem92    hsingle pi hpi hinj hmul,93    exists_preimage_compact_of_image_mul_mem pi hinj hpi.1 hmul⟩9495/-- Literal range equality, not merely abstract isomorphism of the algebras. -/96theorem range_eq_compactOperatorStarSubalgebra_of_singleton_of_image_mul_mem97    (hsingle : ∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q)98    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)99    (hinj : Function.Injective pi)100    (hmul : ∀ (b a : H →L[ℂ] H), a ∈ (NonUnitalStarAlgHom.range pi) →101      b * a ∈ (NonUnitalStarAlgHom.range pi) ∧ a * b ∈ (NonUnitalStarAlgHom.range pi)) :102    (NonUnitalStarAlgHom.range pi) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H := by103  have hmodel := isCompactOperatorModel_of_singleton_of_image_mul_mem104    hsingle pi hpi hinj hmul105  ext T106  constructor107  · intro hT108    obtain ⟨a, rfl⟩ := (NonUnitalStarAlgHom.mem_range pi).1 hT109    exact hmodel.2.1 a110  · intro hT111    exact (NonUnitalStarAlgHom.mem_range pi).2 (hmodel.2.2 T hT)112113end SingletonImage114115section OriginalAlgebra116117variable [Nontrivial A] [PartialOrder A] [StarOrderedRing A]118local instance (pi : NonUnitalCStarRepresentation A H) :119    NonUnitalCStarAlgebra (NonUnitalStarAlgHom.range pi) :=120  NonUnitalStarSubalgebra.nonUnitalCStarAlgebra (NonUnitalStarAlgHom.range pi)121    (h_closed := HomKernelQuotient.isClosed_image pi)122123/-- Joint partial endpoint for the original algebra. The pure state, faithful124representation and literal preimage map are unchanged. A separating irreducible125image action is ruled out, but its existence from properness is NOT presumed.126The finite-dimensional implication closes exactly that independent branch. -/127theorem exists_faithful_image_compact_obstruction_of_singleton128    (hsingle : ∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q)129    (hproperty : ∃ I : NormedSpace.GeometricStructureSpace ℂ A,130      ((NormedSpace.geometricStructureClosure ℂ A).subspace131        ((NormedSpace.geometricStructureClosure ℂ A).component I)).HasContinuousFiniteConjugation132          (ClosureCat.IsCStarRealizable.{u, max u w})) :133    ∃ phi : NonUnitalPureState A,134      Function.Injective phi.gnsRepresentation ∧135      normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation) = Set.univ ∧136      ∃ r : ClosureSpace.Homeomorph137          ((NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range phi.gnsRepresentation)).subspace138            (normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation)))139          (NormedSpace.geometricStructureClosure ℂ A),140        (∀ J : normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation),141          (r.toEquiv J).val = (NonUnitalStarAlgHom.rangeRestrict phi.gnsRepresentation) ⁻¹' J.val.val) ∧142        (∀ T : phi.GNS →L[ℂ] phi.GNS, IsCompactOperator T →143          ∃ a : A, phi.gnsRepresentation a = T) ∧144        (FiniteDimensional ℂ phi.GNS → IsCompactOperatorModel phi.gnsRepresentation) ∧145        (∀ (K : Type z) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]146          (rho : NonUnitalCStarRepresentation (NonUnitalStarAlgHom.range phi.gnsRepresentation) K),147          (∀ a : (NonUnitalStarAlgHom.range phi.gnsRepresentation),148            IsCompactOperator (a : phi.GNS →L[ℂ] phi.GNS) → rho a = 0) →149          ¬ rho.IsIrreducible) := by150  obtain ⟨phi, hfaith, hnormal, r, hr, _I, _hcarrier, _hI, _hclosed, _hcomp,151      hmul, hpre⟩ := exists_faithful_image_operatorIdeal_of_singleton.{u, w} hsingle hproperty152  refine ⟨phi, hfaith, hnormal, r, hr, hpre, ?_, ?_⟩153  · intro hfinite154    letI := hfinite155    exact isCompactOperatorModel_of_finiteDimensional_of_image_mul_mem156      phi.gnsRepresentation hfaith phi.isIrreducible_gnsRepresentation.1 hmul157  · intro K _ _ _ rho hann158    exact not_isIrreducible_of_image_annihilates_compacts159      hsingle phi.gnsRepresentation phi.isIrreducible_gnsRepresentation hfaith hmul rho hann160161/-- The reverse finite-conjugation implication reaches the compact model of162the original algebra. The same `phi`, `pi`, image, and preimage homeomorphism163are retained. The displayed star equivalence and its inverse use this `pi`.164This does not assert the converse compact-algebra test property. -/165theorem exists_faithful_compactOperatorModel_of_singleton_finiteConjugation166    (hsingle : ∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q)167    (hproperty : ∃ I : NormedSpace.GeometricStructureSpace ℂ A,168      ((NormedSpace.geometricStructureClosure ℂ A).subspace169        ((NormedSpace.geometricStructureClosure ℂ A).component I)).HasContinuousFiniteConjugation170          (ClosureCat.IsCStarRealizable.{u, max u w})) :171    ∃ phi : NonUnitalPureState A,172      Function.Injective phi.gnsRepresentation ∧173      normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation) = Set.univ ∧174      ∃ r : ClosureSpace.Homeomorph175          ((NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range phi.gnsRepresentation)).subspace176            (normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation)))177          (NormedSpace.geometricStructureClosure ℂ A),178        (∀ J : normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation),179          (r.toEquiv J).val = (NonUnitalStarAlgHom.rangeRestrict phi.gnsRepresentation) ⁻¹' J.val.val) ∧180        ∃ hmodel : IsCompactOperatorModel phi.gnsRepresentation,181          (NonUnitalStarAlgHom.range phi.gnsRepresentation) =182            ContinuousLinearMap.compactOperatorStarSubalgebra ℂ phi.GNS ∧183          (∀ a : A, (compactOperatorStarAlgEquiv phi.gnsRepresentation hmodel a).val =184            phi.gnsRepresentation a) ∧185          (∀ T : ContinuousLinearMap.compactOperatorStarSubalgebra ℂ phi.GNS,186            phi.gnsRepresentation ((compactOperatorStarAlgEquiv187              phi.gnsRepresentation hmodel).symm T) = T.val) ∧188          ∀ a : A, ‖compactOperatorStarAlgEquiv phi.gnsRepresentation hmodel a‖ = ‖a‖ := by189  obtain ⟨phi, hfaith, hnormal, r, hr, _I, _hcarrier, _hI, _hclosed, _hcomp,190      hmul, _hpre⟩ := exists_faithful_image_operatorIdeal_of_singleton.{u, w} hsingle hproperty191  have hmodel := isCompactOperatorModel_of_singleton_of_image_mul_mem192    hsingle phi.gnsRepresentation phi.isIrreducible_gnsRepresentation hfaith hmul193  refine ⟨phi, hfaith, hnormal, r, hr, hmodel, ?_, ?_, ?_, ?_⟩194  · exact range_eq_compactOperatorStarSubalgebra_of_singleton_of_image_mul_mem195      hsingle phi.gnsRepresentation phi.isIrreducible_gnsRepresentation hfaith hmul196  · exact compactOperatorStarAlgEquiv_apply phi.gnsRepresentation hmodel197  · exact compactOperatorStarAlgEquiv_symm_apply phi.gnsRepresentation hmodel198  · exact norm_compactOperatorStarAlgEquiv_apply phi.gnsRepresentation hmodel199200end OriginalAlgebra201end MathlibAnnex.Analysis.CStarAlgebra