MathlibAnnex/Analysis/CStarAlgebra/DirectSum/CompactlyRepresentedDecomposition.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.Ideal.MinimalIdealFamilyModel8import MathlibAnnex.Analysis.CStarAlgebra.DirectSum.OrthogonalIdealCompactModel910/-!11# The canonical compact c₀-decomposition of a compactly represented C-star algebra1213A faithful compact-valued representation supplies the canonical family of all14minimal nonzero closed star ideals, norm density of their actual finite sums,15and exact compact models on their chosen cyclic Hilbert spaces. This file16passes these proved data to the existing orthogonal-ideal transport and defines17an actual equivalence from the original algebra to the completed compact c₀-sum.1819No density or fiber-model hypothesis is added. The auxiliary spectral order is20fixed to `CStarAlgebra.spectralOrder A`, locally, before selecting any cyclic21fiber. The explicit `letI` in the main declaration's result type fixes this22choice even in a caller's context with a different order instance. The local23attributes below make every subsequent formula use exactly the same order,24`compactModelWitness`, dependent carrier, and compact equivalence. They do not25export a new order instance or introduce an order argument to these declarations.2627The forward direction is `A` to `CompactOperatorC0Sum`; the inverse is the28already constructed compact ideal-sum map. Coordinate, single, finite-sum,29norm, and finite reconstruction formulas refer to this one equivalence.30The canonical index may be empty. No unit, nontriviality, countability,31separability, or finite-dimensional assumption is imposed.3233This is the forward decomposition theorem. It does not identify a diagonal34block algebra with all compact operators on a Hilbert sum, construct the35converse representation, or establish the other characterizations of compact36C-star algebras.37-/3839@[expose] public section4041set_option autoImplicit false42set_option maxHeartbeats 200000043set_option synthInstance.maxHeartbeats 20000044set_option backward.isDefEq.respectTransparency false45set_option backward.whnf.reducibleClassField false46noncomputable section4748open Set49open scoped BigOperators CStarAlgebra Topology5051namespace MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation5253universe u v5455variable {A : Type u} [NonUnitalCStarAlgebra A]56variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]57variable (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented)5859attribute [local instance] _root_.CStarAlgebra.spectralOrder60  _root_.CStarAlgebra.spectralOrderedRing6162/-- The canonical global compact c₀-decomposition supplied by the given63faithful compact representation. The ideal family, its orthogonality and64norm density, and its exact fiber models are all produced from `pi` and65`hpi`; none is an additional premise. The order is fixed locally in the66result type as well as in the defining term. -/67def compactC0Decomposition :68    letI : PartialOrder A := _root_.CStarAlgebra.spectralOrder A69    letI : StarOrderedRing A := _root_.CStarAlgebra.spectralOrderedRing A70    A ≃⋆ₐ[ℂ] CompactOperatorC0Sum71      (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi) := by72  letI : PartialOrder A := _root_.CStarAlgebra.spectralOrder A73  letI : StarOrderedRing A := _root_.CStarAlgebra.spectralOrderedRing A74  exact ClosedStarIdeal.compactC0SumEquivOfDense75    (minimalClosedStarIdealFamily (A := A))76    pairwiseOrthogonal_minimalClosedStarIdealFamily77    (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi)78    (fun i => i.compactModelEquiv pi hpi)79    (dense_finiteSums_minimalClosedStarIdealFamily pi hpi)8081/-- The forward map is the existing ideal decomposition followed by the82specified coordinatewise compact equivalences. -/83theorem compactC0Decomposition_apply (a : A) :84    pi.compactC0Decomposition hpi a =85      C0DirectSum.equiv86        (ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)))87        (fun i : MinimalClosedStarIdeal A =>88          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi))89        (Equiv.refl (MinimalClosedStarIdeal A))90        (fun i => i.compactModelEquiv pi hpi)91        ((ClosedStarIdeal.c0SumEquivOfDense92          (minimalClosedStarIdealFamily (A := A))93          pairwiseOrthogonal_minimalClosedStarIdealFamily94          (dense_finiteSums_minimalClosedStarIdealFamily pi hpi)).symm a) := rfl9596/-- The inverse is literally the compact sum homomorphism constructed by97the orthogonal-ideal transport, with the actual canonical family and models. -/98@[simp]99theorem compactC0Decomposition_symm_apply100    (x : CompactOperatorC0Sum101      (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi)) :102    (pi.compactC0Decomposition hpi).symm x =103      ClosedStarIdeal.compactC0SumHom104        (minimalClosedStarIdealFamily (A := A))105        pairwiseOrthogonal_minimalClosedStarIdealFamily106        (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi)107        (fun i => i.compactModelEquiv pi hpi) x := rfl108109/-- Each forward coordinate is the fixed compact model of the corresponding110actual ideal coordinate. The ideal coordinate uses the same density proof111and the same assembly as the defining global equivalence. -/112@[simp]113theorem eval_compactC0Decomposition (a : A) (i : MinimalClosedStarIdeal A) :114    C0DirectSum.eval115      (fun j : MinimalClosedStarIdeal A =>116        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi)) i117      (pi.compactC0Decomposition hpi a) =118      i.compactModelEquiv pi hpi119        (C0DirectSum.eval120          (ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A))) i121          ((ClosedStarIdeal.c0SumEquivOfDense122            (minimalClosedStarIdealFamily (A := A))123            pairwiseOrthogonal_minimalClosedStarIdealFamily124            (dense_finiteSums_minimalClosedStarIdealFamily pi hpi)).symm a)) := by125  exact ClosedStarIdeal.eval_compactC0SumEquivOfDense126    (minimalClosedStarIdealFamily (A := A))127    pairwiseOrthogonal_minimalClosedStarIdealFamily128    (fun j : MinimalClosedStarIdeal A => j.CompactModelSpace pi hpi)129    (fun j => j.compactModelEquiv pi hpi)130    (dense_finiteSums_minimalClosedStarIdealFamily pi hpi) a i131132/-- The inclusion of a displayed ideal is taken to its own single compact133coordinate, using its already fixed exact compact model. -/134@[simp]135theorem compactC0Decomposition_coe (i : MinimalClosedStarIdeal A)136    (a : ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)) i) :137    pi.compactC0Decomposition hpi (a : A) =138      C0DirectSum.single139        (fun j : MinimalClosedStarIdeal A =>140          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi)) i141        (i.compactModelEquiv pi hpi a) := by142  exact ClosedStarIdeal.compactC0SumEquivOfDense_coe143    (minimalClosedStarIdealFamily (A := A))144    pairwiseOrthogonal_minimalClosedStarIdealFamily145    (fun j : MinimalClosedStarIdeal A => j.CompactModelSpace pi hpi)146    (fun j => j.compactModelEquiv pi hpi)147    (dense_finiteSums_minimalClosedStarIdealFamily pi hpi) i a148149/-- On an ideal element, its own coordinate is its chosen compact model. -/150@[simp]151theorem eval_compactC0Decomposition_coe_same (i : MinimalClosedStarIdeal A)152    (a : ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)) i) :153    C0DirectSum.eval154      (fun j : MinimalClosedStarIdeal A =>155        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi)) i156      (pi.compactC0Decomposition hpi (a : A)) = i.compactModelEquiv pi hpi a := by157  rw [compactC0Decomposition_coe, C0DirectSum.eval_single_same]158159/-- Every other coordinate of a displayed ideal element is zero. -/160theorem eval_compactC0Decomposition_coe_of_ne {i j : MinimalClosedStarIdeal A}161    (hji : j ≠ i)162    (a : ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)) i) :163    C0DirectSum.eval164      (fun k : MinimalClosedStarIdeal A =>165        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (k.CompactModelSpace pi hpi)) j166      (pi.compactC0Decomposition hpi (a : A)) = 0 := by167  rw [compactC0Decomposition_coe, C0DirectSum.eval_single_of_ne _ hji]168169/-- The inverse of a single compact coordinate is the actual element of the170corresponding ideal obtained from the inverse of its fixed compact model. -/171@[simp]172theorem compactC0Decomposition_symm_single (i : MinimalClosedStarIdeal A)173    (T : ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi)) :174    (pi.compactC0Decomposition hpi).symm175      (C0DirectSum.single176        (fun j : MinimalClosedStarIdeal A =>177          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi))178        i T) = ((i.compactModelEquiv pi hpi).symm T : A) := by179  exact ClosedStarIdeal.compactC0SumEquivOfDense_symm_single180    (minimalClosedStarIdealFamily (A := A))181    pairwiseOrthogonal_minimalClosedStarIdealFamily182    (fun j : MinimalClosedStarIdeal A => j.CompactModelSpace pi hpi)183    (fun j => j.compactModelEquiv pi hpi)184    (dense_finiteSums_minimalClosedStarIdealFamily pi hpi) i T185186/-- Finite ambient ideal sums are sent to their finite compact-coordinate187sums under this same global equivalence. -/188@[simp]189theorem compactC0Decomposition_sum (s : Finset (MinimalClosedStarIdeal A))190    (a : ∀ i, ClosedStarIdeal.Fiber (minimalClosedStarIdealFamily (A := A)) i) :191    pi.compactC0Decomposition hpi (∑ i ∈ s, (a i : A)) =192      ∑ i ∈ s, C0DirectSum.single193        (fun j : MinimalClosedStarIdeal A =>194          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi))195        i (i.compactModelEquiv pi hpi (a i)) := by196  exact ClosedStarIdeal.compactC0SumEquivOfDense_sum197    (minimalClosedStarIdealFamily (A := A))198    pairwiseOrthogonal_minimalClosedStarIdealFamily199    (fun j : MinimalClosedStarIdeal A => j.CompactModelSpace pi hpi)200    (fun j => j.compactModelEquiv pi hpi)201    (dense_finiteSums_minimalClosedStarIdealFamily pi hpi) s a202203/-- A finite sum of compact single-coordinate elements reconstructs the204finite sum of their actual ideal preimages. -/205@[simp]206theorem compactC0Decomposition_symm_sum (s : Finset (MinimalClosedStarIdeal A))207    (T : ∀ i : MinimalClosedStarIdeal A,208      ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi)) :209    (pi.compactC0Decomposition hpi).symm210      (∑ i ∈ s, C0DirectSum.single211        (fun j : MinimalClosedStarIdeal A =>212          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi))213        i (T i)) = ∑ i ∈ s, ((i.compactModelEquiv pi hpi).symm (T i) : A) := by214  simp only [map_sum, compactC0Decomposition_symm_single]215216/-- Finite truncation followed by the inverse reconstructs an actual finite217sum in the original algebra. -/218@[simp]219theorem compactC0Decomposition_symm_truncate (s : Finset (MinimalClosedStarIdeal A))220    (x : CompactOperatorC0Sum221      (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi)) :222    (pi.compactC0Decomposition hpi).symm223      (C0DirectSum.truncate224        (fun i : MinimalClosedStarIdeal A =>225          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi)) s x) =226      ∑ i ∈ s, ((i.compactModelEquiv pi hpi).symm227        (C0DirectSum.eval228          (fun j : MinimalClosedStarIdeal A =>229            ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi))230          i x) : A) := by231  rw [compactC0Decomposition_symm_apply]232  exact ClosedStarIdeal.compactC0SumHom_truncate233    (minimalClosedStarIdealFamily (A := A))234    pairwiseOrthogonal_minimalClosedStarIdealFamily235    (fun j : MinimalClosedStarIdeal A => j.CompactModelSpace pi hpi)236    (fun j => j.compactModelEquiv pi hpi) s x237238/-- The canonical decomposition preserves the original C-star norm. -/239@[simp]240theorem norm_compactC0Decomposition (a : A) :241    ‖pi.compactC0Decomposition hpi a‖ = ‖a‖ := by242  exact ClosedStarIdeal.norm_compactC0SumEquivOfDense243    (minimalClosedStarIdealFamily (A := A))244    pairwiseOrthogonal_minimalClosedStarIdealFamily245    (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi)246    (fun i => i.compactModelEquiv pi hpi)247    (dense_finiteSums_minimalClosedStarIdealFamily pi hpi) a248249/-- The inverse compact sum preserves the completed c₀ norm. -/250@[simp]251theorem norm_compactC0Decomposition_symm252    (x : CompactOperatorC0Sum253      (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi)) :254    ‖(pi.compactC0Decomposition hpi).symm x‖ = ‖x‖ := by255  rw [compactC0Decomposition_symm_apply, ClosedStarIdeal.norm_compactC0SumHom]256257/-- The canonical forward equivalence is an isometry. -/258theorem isometry_compactC0Decomposition : Isometry (pi.compactC0Decomposition hpi) := by259  rw [AddMonoidHomClass.isometry_iff_norm]260  exact norm_compactC0Decomposition pi hpi261262/-- The inverse of the very same canonical equivalence is an isometry. -/263theorem isometry_compactC0Decomposition_symm :264    Isometry (pi.compactC0Decomposition hpi).symm := by265  rw [AddMonoidHomClass.isometry_iff_norm]266  exact norm_compactC0Decomposition_symm pi hpi267268/-- The original norm is the supremum of the compact-coordinate norms.269The formula also covers the empty canonical index in the zero algebra. -/270theorem norm_eq_ciSup_norm_eval_compactC0Decomposition (a : A) :271    ‖a‖ = ⨆ i : MinimalClosedStarIdeal A,272      ‖C0DirectSum.eval273        (fun j : MinimalClosedStarIdeal A =>274          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi)) i275        (pi.compactC0Decomposition hpi a)‖ := by276  calc277    ‖a‖ = ‖pi.compactC0Decomposition hpi a‖ := (norm_compactC0Decomposition pi hpi a).symm278    _ = _ := C0DirectSum.norm_eq_ciSup _ _279280/-- Each displayed compact coordinate is contractive in the ambient norm. -/281theorem norm_eval_compactC0Decomposition_le (a : A) (i : MinimalClosedStarIdeal A) :282    ‖C0DirectSum.eval283      (fun j : MinimalClosedStarIdeal A =>284        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi)) i285      (pi.compactC0Decomposition hpi a)‖ ≤ ‖a‖ := by286  calc287    _ ≤ ‖pi.compactC0Decomposition hpi a‖ := C0DirectSum.norm_eval_le _ i _288    _ = ‖a‖ := norm_compactC0Decomposition pi hpi a289290/-- The error of the finite ideal reconstruction equals the c₀ truncation291error of the same canonical decomposition. -/292theorem norm_sub_sum_compactC0Decomposition_symm_eval293    (a : A) (s : Finset (MinimalClosedStarIdeal A)) :294    ‖a - ∑ i ∈ s, ((i.compactModelEquiv pi hpi).symm295      (C0DirectSum.eval296        (fun j : MinimalClosedStarIdeal A =>297          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi)) i298        (pi.compactC0Decomposition hpi a)) : A)‖ =299      ‖pi.compactC0Decomposition hpi a - C0DirectSum.truncate300        (fun i : MinimalClosedStarIdeal A =>301          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi)) s302        (pi.compactC0Decomposition hpi a)‖ := by303  have hnorm := norm_compactC0Decomposition_symm pi hpi304    (pi.compactC0Decomposition hpi a - C0DirectSum.truncate305      (fun i : MinimalClosedStarIdeal A =>306        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi)) s307      (pi.compactC0Decomposition hpi a))308  simpa only [map_sub, StarAlgEquiv.symm_apply_apply,309    compactC0Decomposition_symm_truncate] using hnorm310311/-- Every element is approximated in norm by the finite reconstruction of312its own canonical compact coordinates, not by independently chosen ideal313approximants. The pre-existing norm density was used to construct the314surjective equivalence; this is a subsequent reconstruction formula. -/315theorem exists_finset_norm_sub_sum_compactC0Decomposition_symm_eval_lt316    (a : A) {ε : ℝ} (hε : 0 < ε) :317    ∃ s : Finset (MinimalClosedStarIdeal A),318      ‖a - ∑ i ∈ s, ((i.compactModelEquiv pi hpi).symm319        (C0DirectSum.eval320          (fun j : MinimalClosedStarIdeal A =>321            ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (j.CompactModelSpace pi hpi)) i322          (pi.compactC0Decomposition hpi a)) : A)‖ < ε := by323  have ht : ∃ s : Finset (MinimalClosedStarIdeal A),324      ‖pi.compactC0Decomposition hpi a - C0DirectSum.truncate325        (fun i : MinimalClosedStarIdeal A =>326          ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi)) s327        (pi.compactC0Decomposition hpi a)‖ < ε :=328    @C0DirectSum.exists_finset_norm_sub_truncate_lt329      (MinimalClosedStarIdeal A)330      (fun i : MinimalClosedStarIdeal A =>331        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (i.CompactModelSpace pi hpi))332      (fun i => inferInstance)333      (pi.compactC0Decomposition hpi a) ε hε334  obtain ⟨s, hs⟩ := ht335  refine ⟨s, ?_⟩336  rw [norm_sub_sum_compactC0Decomposition_symm_eval]337  exact hs338339end MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation