MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/HomogeneousCharacterization.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.GCRCharacterization8import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.NormalPartFiniteCharacter9import MathlibAnnex.Analysis.Normed.GeometricStructure.Separation10import Mathlib.LinearAlgebra.Dimension.Finite1112/-!13# Finite-dimensional irreducible representations and compact component models1415The representation conditions are raw: finite dimensionality AND a predicate16on `finrank`. They do not define type I, and they never interpret the zero17`finrank` of an infinite-dimensional space as dimension zero. Taking the18predicate to be equality with `n` gives the homogeneous criterion; the bound19variant is in `SubhomogeneousCharacterization`.2021A finite comparison has no full-continuity premise. Its promotion to a full22homeomorphism keeps its point map: first transfer finite dimension between the23actual normal parts, then apply the received finite-character theorem. This24includes dimensions one and two, without a projective semilinear lift.2526The equivalences use compact models in the algebra universe. Separate27elimination theorems accept models in an arbitrary universe and conclude the28representation condition in EVERY independently specified Hilbert universe.29-/3031@[expose] public section32set_option autoImplicit false33set_option maxHeartbeats 200000034set_option synthInstance.maxHeartbeats 20000035noncomputable section36open Set3738namespace ClosureSpace3940attribute [local instance] ContinuousLinearMap.isClosed_compactOperatorStarSubalgebra4142/-- A finite comparison with a nonzero finite-dimensional compact-operator GSS,43with an additional predicate on the dimension. This is a geometric predicate,44not a definition of homogeneous representations. -/45def HasFiniteDimensionalCompactComparison.{uH, uX} {X : Type uX}46    (c : ClosureSpace X) (P : ℕ → Prop) : Prop :=47  ∃ (H : Type uH) (instN : NormedAddCommGroup H),48    letI := instN49    ∃ instI : InnerProductSpace ℂ H,50      letI := instI51      ∃ instC : CompleteSpace H,52        letI := instC53        ∃ instT : Nontrivial H,54          letI := instT55          FiniteDimensional ℂ H ∧ P (Module.finrank ℂ H) ∧56            Nonempty (FiniteHomeomorph c57              (NormedSpace.geometricStructureClosure ℂ58                (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))5960/-- The full-homeomorphism version retains a real finite-dimensional Hilbert61witness and the same dimension predicate. -/62def HasFiniteDimensionalCompactHomeomorph.{uH, uX} {X : Type uX}63    (c : ClosureSpace X) (P : ℕ → Prop) : Prop :=64  ∃ (H : Type uH) (instN : NormedAddCommGroup H),65    letI := instN66    ∃ instI : InnerProductSpace ℂ H,67      letI := instI68      ∃ instC : CompleteSpace H,69        letI := instC70        ∃ instT : Nontrivial H,71          letI := instT72          FiniteDimensional ℂ H ∧ P (Module.finrank ℂ H) ∧73            Nonempty (Homeomorph c74              (NormedSpace.geometricStructureClosure ℂ75                (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))7677universe uH uX78variable {X : Type uX} {c : ClosureSpace X} {P : ℕ → Prop}7980/-- Forget only full continuity, not the finite-dimensional witness. -/81theorem HasFiniteDimensionalCompactHomeomorph.hasFiniteDimensionalCompactComparison82    (h : HasFiniteDimensionalCompactHomeomorph.{uH, uX} c P) :83    HasFiniteDimensionalCompactComparison.{uH, uX} c P := by84  obtain ⟨H, instN, instI, instC, instT, hdim, hP, ⟨e⟩⟩ := h85  letI := instN86  letI := instI87  letI := instC88  letI := instT89  exact ⟨H, instN, instI, instC, instT, hdim, hP, ⟨e.toFiniteHomeomorph⟩⟩9091/-- Every compact model in this predicate has positive dimension. In particular,92an empty target is not silently counted as a dimension-zero model. -/93theorem HasFiniteDimensionalCompactComparison.exists_pos_finrank94    (h : HasFiniteDimensionalCompactComparison.{uH, uX} c P) :95    ∃ m : ℕ, 0 < m ∧ P m := by96  obtain ⟨H, instN, instI, instC, instT, hdim, hP, _he⟩ := h97  letI := instN98  letI := instI99  letI := instC100  letI := instT101  letI : FiniteDimensional ℂ H := hdim102  exact ⟨Module.finrank ℂ H, Module.finrank_pos, hP⟩103104end ClosureSpace105106namespace MathlibAnnex.Analysis.CStarAlgebra107108universe u v w109attribute [local instance] ContinuousLinearMap.isClosed_compactOperatorStarSubalgebra110  HomKernelQuotient.imageCStarAlgebra HomKernelQuotient.isClosed_image111112section Concrete113variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]114variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]115116/-- Transfer a genuine finite target dimension through the specified finite117map. No forward or inverse full continuity is an input. -/118theorem finite_and_finrank_eq_of_normalPart_compact_comparison119    [Nontrivial K] [FiniteDimensional ℂ K]120    (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))121    [IsClosed (S : Set (H →L[ℂ] H))]122    (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))123    (e : ClosureSpace.FiniteHomeomorph124      ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S))125      (NormedSpace.geometricStructureClosure ℂ126        (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K))) :127    FiniteDimensional ℂ H ∧ Module.finrank ℂ H = Module.finrank ℂ K := by128  let T := ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K129  let f := e.trans (compactNormalPartHomeomorph (H := K)).symm.toFiniteHomeomorph130  have hd := finite_and_finrank_eq_of_normalPart_finiteHomeomorph S T hS131    (isIrreducible_compactOperatorRepresentation K) f132    (Or.inr (inferInstance : Module.Finite ℂ K))133  exact ⟨hd.1, hd.2.2⟩134135/-- Promote this SAME finite comparison to a full homeomorphism. Only actual136coefficient kernels are used by the finite-character theorem. -/137theorem exists_homeomorph_eq_of_finiteDimensional_compact_comparison138    [Nontrivial K] [FiniteDimensional ℂ K]139    (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))140    [IsClosed (S : Set (H →L[ℂ] H))]141    (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))142    (e : ClosureSpace.FiniteHomeomorph143      ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S))144      (NormedSpace.geometricStructureClosure ℂ145        (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K))) :146    ∃ F : ClosureSpace.Homeomorph147      ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S))148      (NormedSpace.geometricStructureClosure ℂ149        (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K)),150      F.toEquiv = e.toEquiv := by151  letI : FiniteDimensional ℂ H :=152    (finite_and_finrank_eq_of_normalPart_compact_comparison S hS e).1153  let T := ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K154  letI : FiniteDimensional ℂ S := finiteDimensional_operator_subalgebra S155  letI : FiniteDimensional ℂ T := finiteDimensional_operator_subalgebra T156  let a := compactNormalPartHomeomorph (H := K)157  let f := e.trans a.symm.toFiniteHomeomorph158  refine ⟨(normalPartHomeomorphOfFiniteDimensional S T f).trans a, ?_⟩159  apply Equiv.ext160  intro I161  change a.toEquiv (a.toEquiv.symm (e.toEquiv I)) = e.toEquiv I162  exact a.toEquiv.apply_symm_apply (e.toEquiv I)163164end Concrete165166section Algebra167variable {A : Type u} [NonUnitalCStarAlgebra A] [hA : Nontrivial A]168attribute [local instance] _root_.CStarAlgebra.spectralOrder169  _root_.CStarAlgebra.spectralOrderedRing170variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]171variable {K : Type w} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]172173include hA in174/-- The SAME component comparison upgrades; the homeomorphism of a normal part175with the component (not its closure) cancels from the point-map formula. -/176theorem exists_component_homeomorph_eq_of_finiteDimensional_compact_comparison177    [Nontrivial K] [FiniteDimensional ℂ K]178    (I : NormedSpace.GeometricStructureSpace ℂ A)179    (e : ClosureSpace.FiniteHomeomorph180      ((NormedSpace.geometricStructureClosure ℂ A).subspace181        ((NormedSpace.geometricStructureClosure ℂ A).component I))182      (NormedSpace.geometricStructureClosure ℂ183        (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K))) :184    ∃ F : ClosureSpace.Homeomorph185      ((NormedSpace.geometricStructureClosure ℂ A).subspace186        ((NormedSpace.geometricStructureClosure ℂ A).component I))187      (NormedSpace.geometricStructureClosure ℂ188        (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K)),189      F.toEquiv = e.toEquiv := by190  obtain ⟨L, instN, instI, instC, pi, hpi, a, _ha⟩ :=191    exists_representation_normalPart_homeomorph_component A I192  letI := instN193  letI := instI194  letI := instC195  have hi := (NonUnitalCStarRepresentation.isIrreducible_imageRepresentation_iff pi).2 hpi196  obtain ⟨F, hF⟩ := exists_homeomorph_eq_of_finiteDimensional_compact_comparison197    (NonUnitalStarAlgHom.range pi) hi (a.toFiniteHomeomorph.trans e)198  refine ⟨a.symm.trans F, ?_⟩199  apply Equiv.ext200  intro J201  change F.toEquiv (a.toEquiv.symm J) = e.toEquiv J202  rw [hF]203  change e.toEquiv (a.toEquiv (a.toEquiv.symm J)) = e.toEquiv J204  rw [Equiv.apply_symm_apply]205206include hA in207/-- Full and finite comparisons are equivalent on actual components with a208finite-dimensional compact target, even in an independent model universe. -/209theorem component_hasFiniteDimensionalCompactComparison_iff_homeomorph210    (P : ℕ → Prop) (I : NormedSpace.GeometricStructureSpace ℂ A) :211    ClosureSpace.HasFiniteDimensionalCompactComparison.{w, u}212        ((NormedSpace.geometricStructureClosure ℂ A).subspace213          ((NormedSpace.geometricStructureClosure ℂ A).component I)) P ↔214      ClosureSpace.HasFiniteDimensionalCompactHomeomorph.{w, u}215        ((NormedSpace.geometricStructureClosure ℂ A).subspace216          ((NormedSpace.geometricStructureClosure ℂ A).component I)) P := by217  constructor218  · rintro ⟨L, instN, instI, instC, instT, hdim, hP, ⟨e⟩⟩219    letI := instN220    letI := instI221    letI := instC222    letI := instT223    letI : FiniteDimensional ℂ L := hdim224    obtain ⟨F, _hF⟩ :=225      exists_component_homeomorph_eq_of_finiteDimensional_compact_comparison I e226    exact ⟨L, instN, instI, instC, instT, hdim, hP, ⟨F⟩⟩227  · exact ClosureSpace.HasFiniteDimensionalCompactHomeomorph.hasFiniteDimensionalCompactComparison228229include hA in230/-- A comparison model in ANY fixed universe supplies both genuine finiteness231and the numerical dimension predicate in each small pure GNS model. -/232theorem forall_pure_state_finiteDimensional_finrank_of_component_compact_comparisons233    (P : ℕ → Prop)234    (h : ∀ I : NormedSpace.GeometricStructureSpace ℂ A,235      ClosureSpace.HasFiniteDimensionalCompactComparison.{w, u}236        ((NormedSpace.geometricStructureClosure ℂ A).subspace237          ((NormedSpace.geometricStructureClosure ℂ A).component I)) P) :238    ∀ phi : NonUnitalPureState A,239      FiniteDimensional ℂ phi.GNS ∧ P (Module.finrank ℂ phi.GNS) := by240  intro phi241  let pi := phi.gnsRepresentation242  let x := phi.gnsVector243  let I := NonUnitalCStarRepresentation.matrixCoefficientKernel pi244    phi.isIrreducible_gnsRepresentation x x phi.gnsVector_ne_zero phi.gnsVector_ne_zero245  let a := imageNormalPartHomeomorph pi phi.isIrreducible_gnsRepresentation246    x x phi.gnsVector_ne_zero phi.gnsVector_ne_zero247  obtain ⟨L, instN, instI, instC, instT, hdim, hP, ⟨e⟩⟩ := h I248  letI := instN249  letI := instI250  letI := instC251  letI := instT252  letI : FiniteDimensional ℂ L := hdim253  have hi := (NonUnitalCStarRepresentation.isIrreducible_imageRepresentation_iff pi).2254    phi.isIrreducible_gnsRepresentation255  have hd := finite_and_finrank_eq_of_normalPart_compact_comparison (NonUnitalStarAlgHom.range pi) hi256    (a.toFiniteHomeomorph.trans e)257  exact ⟨hd.1, hd.2.symm ▸ hP⟩258259include hA in260/-- Pure-state finite-dimensional tests are equivalent to finite compact261component models in the algebra universe. Exact interpolation gives262image = B(H) = K(H); the GNS component and its preimage homeomorphism are retained. -/263theorem forall_pure_state_finiteDimensional_finrank_iff_component_compact_comparison264    (P : ℕ → Prop) :265    (∀ phi : NonUnitalPureState A,266      FiniteDimensional ℂ phi.GNS ∧ P (Module.finrank ℂ phi.GNS)) ↔267    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,268      ClosureSpace.HasFiniteDimensionalCompactComparison.{u, u}269        ((NormedSpace.geometricStructureClosure ℂ A).subspace270          ((NormedSpace.geometricStructureClosure ℂ A).component I)) P := by271  constructor272  · intro h I273    obtain ⟨L, instN, instI, instC, pi, hpi, a, _ha⟩ :=274      exists_representation_normalPart_homeomorph_component A I275    letI := instN276    letI := instI277    letI := instC278    letI : Nontrivial L := pi.nontrivial_of_isNonzero hpi.1279    have hd := NonUnitalCStarRepresentation.finiteDimensional_finrank_of_forall_pure_state280      P h pi hpi281    letI : FiniteDimensional ℂ L := hd.1282    have hi := (NonUnitalCStarRepresentation.isIrreducible_imageRepresentation_iff pi).2 hpi283    have hr : (NonUnitalStarAlgHom.range pi) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ L := by284      rw [eq_top_of_isIrreducible_subtype_of_finiteDimensional (NonUnitalStarAlgHom.range pi) hi,285        ContinuousLinearMap.compactOperatorStarSubalgebra_eq_top]286    obtain ⟨b⟩ := nonempty_homeomorph_compact_of_eq (NonUnitalStarAlgHom.range pi) hr287    exact ⟨L, instN, instI, instC, inferInstance, hd.1, hd.2,288      ⟨(a.symm.trans b).toFiniteHomeomorph⟩⟩289  · exact forall_pure_state_finiteDimensional_finrank_of_component_compact_comparisons P290291include hA in292/-- The conclusion covers an arbitrary represented Hilbert universe; the293comparison models may inhabit yet another universe. -/294theorem finiteDimensional_finrank_of_component_compact_comparisons295    (P : ℕ → Prop)296    (h : ∀ I : NormedSpace.GeometricStructureSpace ℂ A,297      ClosureSpace.HasFiniteDimensionalCompactComparison.{w, u}298        ((NormedSpace.geometricStructureClosure ℂ A).subspace299          ((NormedSpace.geometricStructureClosure ℂ A).component I)) P)300    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :301    FiniteDimensional ℂ H ∧ P (Module.finrank ℂ H) :=302  NonUnitalCStarRepresentation.finiteDimensional_finrank_of_forall_pure_state P303    (forall_pure_state_finiteDimensional_finrank_of_component_compact_comparisons P h) pi hpi304305include hA in306/-- Raw all-representation condition in the small universe. The preceding307elimination theorem is its separately proved extension to every Hilbert universe. -/308theorem forall_irreducible_finiteDimensional_finrank_iff_component_compact_comparison309    (P : ℕ → Prop) :310    (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],311      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →312        FiniteDimensional ℂ L ∧ P (Module.finrank ℂ L)) ↔313    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,314      ClosureSpace.HasFiniteDimensionalCompactComparison.{u, u}315        ((NormedSpace.geometricStructureClosure ℂ A).subspace316          ((NormedSpace.geometricStructureClosure ℂ A).component I)) P := by317  constructor318  · intro h319    apply (forall_pure_state_finiteDimensional_finrank_iff_component_compact_comparison P).1320    intro phi321    exact h phi.GNS phi.gnsRepresentation phi.isIrreducible_gnsRepresentation322  · intro h L _ _ _ pi hpi323    exact finiteDimensional_finrank_of_component_compact_comparisons P h pi hpi324325include hA in326/-- The same raw condition with full component homeomorphisms, obtained by327finite character, not by adding continuity assumptions to the finite comparison. -/328theorem forall_irreducible_finiteDimensional_finrank_iff_component_compact_homeomorph329    (P : ℕ → Prop) :330    (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],331      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →332        FiniteDimensional ℂ L ∧ P (Module.finrank ℂ L)) ↔333    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,334      ClosureSpace.HasFiniteDimensionalCompactHomeomorph.{u, u}335        ((NormedSpace.geometricStructureClosure ℂ A).subspace336          ((NormedSpace.geometricStructureClosure ℂ A).component I)) P := by337  rw [forall_irreducible_finiteDimensional_finrank_iff_component_compact_comparison P]338  exact forall_congr' (fun I => component_hasFiniteDimensionalCompactComparison_iff_homeomorph P I)339340include hA in341/-- Nontriviality supplies an actual GSS point and a nonzero pure GNS model.342Consequently every uniformly prescribed finite-dimension condition is realized343at a POSITIVE natural number. -/344theorem exists_pos_finrank_of_forall_pure_state (P : ℕ → Prop)345    (h : ∀ phi : NonUnitalPureState A,346      FiniteDimensional ℂ phi.GNS ∧ P (Module.finrank ℂ phi.GNS)) :347    ∃ m : ℕ, 0 < m ∧ P m := by348  obtain ⟨a, ha⟩ := exists_ne (0 : A)349  obtain ⟨I, _hI⟩ := NormedSpace.exists_geometricStructureSpace_notMem ℂ A ha350  obtain ⟨phi, _hphi⟩ := NonUnitalPureState.toGeometricSpectrum_surjective351    (NormedSpace.toGeometricSpectrum ℂ A I)352  have hd := h phi353  letI : FiniteDimensional ℂ phi.GNS := hd.1354  letI : Nontrivial phi.GNS := phi.gnsRepresentation.nontrivial_of_isNonzero355    phi.isIrreducible_gnsRepresentation.1356  exact ⟨Module.finrank ℂ phi.GNS, Module.finrank_pos, hd.2⟩357358include hA in359/-- The n-homogeneous criterion with n allowed to be zero, and explicit finite360dimensionality on the representation side. No independent Type-I bridge is used. -/361theorem forall_irreducible_finrank_eq_iff_component_compact_comparison (n : ℕ) :362    (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],363      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →364        FiniteDimensional ℂ L ∧ Module.finrank ℂ L = n) ↔365    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,366      ClosureSpace.HasFiniteDimensionalCompactComparison.{u, u}367        ((NormedSpace.geometricStructureClosure ℂ A).subspace368          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m = n) :=369  forall_irreducible_finiteDimensional_finrank_iff_component_compact_comparison (fun m => m = n)370371include hA in372/-- The full-homeomorphism form of the SAME homogeneous criterion. -/373theorem forall_irreducible_finrank_eq_iff_component_compact_homeomorph (n : ℕ) :374    (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],375      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →376        FiniteDimensional ℂ L ∧ Module.finrank ℂ L = n) ↔377    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,378      ClosureSpace.HasFiniteDimensionalCompactHomeomorph.{u, u}379        ((NormedSpace.geometricStructureClosure ℂ A).subspace380          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m = n) :=381  forall_irreducible_finiteDimensional_finrank_iff_component_compact_homeomorph (fun m => m = n)382383include hA in384/-- Zero-homogeneity is impossible for a nontrivial algebra, through an actual385nonzero pure GNS model rather than a convention about infinite-dimensional finrank. -/386theorem not_forall_irreducible_finrank_eq_zero :387    ¬ (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],388      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →389        FiniteDimensional ℂ L ∧ Module.finrank ℂ L = 0) := by390  intro h391  obtain ⟨m, hm, hm0⟩ := exists_pos_finrank_of_forall_pure_state (fun m => m = 0)392    (fun phi => h phi.GNS phi.gnsRepresentation phi.isIrreducible_gnsRepresentation)393  exact (Nat.ne_of_gt hm) hm0394395include hA in396/-- No collection of zero-dimensional nonzero compact targets can model every397component. Model witnesses are allowed in any independently specified universe. -/398theorem not_forall_component_compact_comparison_finrank_zero :399    ¬ (∀ I : NormedSpace.GeometricStructureSpace ℂ A,400      ClosureSpace.HasFiniteDimensionalCompactComparison.{w, u}401        ((NormedSpace.geometricStructureClosure ℂ A).subspace402          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m = 0)) := by403  intro h404  obtain ⟨m, hm, hm0⟩ := exists_pos_finrank_of_forall_pure_state (fun m => m = 0)405    (forall_pure_state_finiteDimensional_finrank_of_component_compact_comparisons406      (fun m => m = 0) h)407  exact (Nat.ne_of_gt hm) hm0408409end Algebra410end MathlibAnnex.Analysis.CStarAlgebra