MathlibAnnex/Analysis/CStarAlgebra/DirectSum/OrthogonalIdealCompactModel.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.DirectSum.OrthogonalIdealAssembly8import MathlibAnnex.Analysis.CStarAlgebra.DirectSum.Equiv9import MathlibAnnex.Analysis.CStarAlgebra.DirectSum.CompactOperators10import MathlibAnnex.Analysis.CStarAlgebra.CompactModelEquiv1112/-!13# Compact-fiber transport of an orthogonal ideal assembly1415For a given family `J` of actual closed star ideals, suppose that different16ideals annihilate one another.  Given exact star-algebra equivalences from17`Fiber J i` to the compact operators on dependent Hilbert spaces `H i`, the18existing dependent c₀ equivalence transports the orthogonal-ideal sum map to19an isometric star homomorphism `CompactOperatorC0Sum H → A`.  Its range is the20norm closure of `finiteSums J`; density is not needed for this statement.2122Only after an explicit hypothesis `Dense (finiteSums J)` is supplied do we23construct an equivalence `A ≃⋆ₐ[ℂ] CompactOperatorC0Sum H`.  The inverse is the24same transported sum map, not another chosen representation.  The final25section also accepts given exact compact representations and uses the26existing `compactOperatorStarAlgEquiv` to obtain the fiber equivalences.2728This file proves neither existence of the ideal family, its orthogonality,29nor density for a particular algebra.  Exact compact models are inputs, not30consequences of an unproved elementary-ideal classification.  Their C-star31norms make the given star equivalences automatically isometric; no separate32norm hypothesis is imposed.  Indices are arbitrary and fibers are dependent;33empty indices and zero fibers are not excluded.  The target is the completed34c₀-sum of compact-operator algebras, not the finite-support algebra, the bounded35product, or all compact operators on a Hilbert direct sum.36-/37383940set_option autoImplicit false41set_option maxHeartbeats 200000042set_option synthInstance.maxHeartbeats 20000043noncomputable section4445open Set Topology46open scoped BigOperators CStarAlgebra ENNReal4748namespace MathlibAnnex.Analysis.CStarAlgebra.ClosedStarIdeal4950universe uι uA uH5152variable {ι : Type uι} {A : Type uA} [NonUnitalCStarAlgebra A]53variable (J : ι → ClosedStarIdeal A) (hJ : PairwiseOrthogonal J)54variable (H : ι → Type uH)55variable [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)]56variable [∀ i, CompleteSpace (H i)]57variable (E : ∀ i, Fiber J i ≃⋆ₐ[ℂ]58  ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))5960set_option backward.isDefEq.respectTransparency false in61/-- Transport the completed orthogonal-ideal sum map along the given exact62compact fiber equivalences.  No ambient density hypothesis is needed. -/63def compactC0SumHom : CompactOperatorC0Sum H →⋆ₙₐ[ℂ] A :=64  (c0SumHom J hJ).comp65    (C0DirectSum.equiv (Fiber J)66      (fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))67      (Equiv.refl ι) E).symm.toNonUnitalStarAlgHom6869@[simp]70theorem compactC0SumHom_apply (x : CompactOperatorC0Sum H) :71    compactC0SumHom J hJ H E x =72      c0SumHom J hJ73        ((C0DirectSum.equiv (Fiber J)74          (fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))75          (Equiv.refl ι) E).symm x) := rfl7677/-- The transported sum map preserves the completed c₀ supremum norm. -/78@[simp]79theorem norm_compactC0SumHom (x : CompactOperatorC0Sum H) :80    ‖compactC0SumHom J hJ H E x‖ = ‖x‖ := by81  rw [compactC0SumHom_apply, norm_c0SumHom, C0DirectSum.norm_equiv_symm_apply]8283/-- The compact-fiber sum map is an isometry, even when its range is proper. -/84theorem isometry_compactC0SumHom : Isometry (compactC0SumHom J hJ H E) := by85  rw [AddMonoidHomClass.isometry_iff_norm]86  exact norm_compactC0SumHom J hJ H E8788/-- No nonzero completed c₀-family is lost by the transported sum map. -/89theorem compactC0SumHom_injective : Function.Injective (compactC0SumHom J hJ H E) :=90  (isometry_compactC0SumHom J hJ H E).injective9192/-- A single compact coordinate is sent to its actual preimage in the93corresponding ambient ideal. -/94@[simp]95theorem compactC0SumHom_single (i : ι)96    (T : ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i)) :97    compactC0SumHom J hJ H E98      (C0DirectSum.single99        (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i T) =100      ((E i).symm T : A) := by101  have hsingle :102      C0DirectSum.equiv (Fiber J)103        (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j))104        (Equiv.refl ι) E105        (C0DirectSum.single (Fiber J) i ((E i).symm T)) =106      C0DirectSum.single107        (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i T := by108    have h := C0DirectSum.equiv_single (Fiber J)109      (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j))110      (Equiv.refl ι) E i ((E i).symm T)111    change C0DirectSum.equiv (Fiber J)112      (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j))113      (Equiv.refl ι) E (C0DirectSum.single (Fiber J) i ((E i).symm T)) =114      C0DirectSum.single115        (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i116        ((E i) ((E i).symm T)) at h117    exact h.trans (congrArg118      (C0DirectSum.single119        (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i)120      ((E i).apply_symm_apply T))121  rw [← hsingle, compactC0SumHom_apply, StarAlgEquiv.symm_apply_apply, c0SumHom_single]122123/-- Finite truncations are transported to finite ambient ideal sums. -/124@[simp]125theorem compactC0SumHom_truncate (s : Finset ι) (x : CompactOperatorC0Sum H) :126    compactC0SumHom J hJ H E127      (C0DirectSum.truncate128        (fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i)) s x) =129      ∑ i ∈ s, ((E i).symm130        (C0DirectSum.eval131          (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i x) : A) := by132  simp only [C0DirectSum.truncate, map_sum, compactC0SumHom_single]133134/-- Exact compact fiber transport does not change the ambient range of the135orthogonal-ideal sum map. -/136theorem range_compactC0SumHom :137    Set.range (compactC0SumHom J hJ H E) = Set.range (c0SumHom J hJ) := by138  ext a139  constructor140  · rintro ⟨x, rfl⟩141    exact ⟨(C0DirectSum.equiv (Fiber J)142      (fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))143      (Equiv.refl ι) E).symm x, rfl⟩144  · rintro ⟨x, rfl⟩145    refine ⟨C0DirectSum.equiv (Fiber J)146      (fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))147      (Equiv.refl ι) E x, ?_⟩148    rw [compactC0SumHom_apply, StarAlgEquiv.symm_apply_apply]149150/-- Without any density hypothesis, the transported compact c₀-sum has151exactly the norm-closed ambient finite-sum range. -/152theorem range_compactC0SumHom_eq_closure_finiteSums :153    Set.range (compactC0SumHom J hJ H E) = closure (finiteSums J) := by154  rw [range_compactC0SumHom, range_c0SumHom_eq_closure_finiteSums]155156/-- Ambient density is the explicit additional input for surjectivity. -/157theorem compactC0SumHom_surjective (hdense : Dense (finiteSums J)) :158    Function.Surjective (compactC0SumHom J hJ H E) := by159  intro a160  obtain ⟨x, hx⟩ := c0SumHom_surjective J hJ hdense a161  refine ⟨C0DirectSum.equiv (Fiber J)162    (fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))163    (Equiv.refl ι) E x, ?_⟩164  simpa only [compactC0SumHom_apply, StarAlgEquiv.symm_apply_apply] using hx165166set_option backward.isDefEq.respectTransparency false in167/-- The actual compact c₀-model of the ambient algebra, conditional on the168given exact fiber equivalences and on explicit norm density of finite sums.169The direction is from `A` to the completed compact c₀-sum. -/170def compactC0SumEquivOfDense (hdense : Dense (finiteSums J)) :171    A ≃⋆ₐ[ℂ] CompactOperatorC0Sum H :=172  (c0SumEquivOfDense J hJ hdense).symm.trans173    (C0DirectSum.equiv (Fiber J)174      (fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))175      (Equiv.refl ι) E)176177@[simp]178theorem compactC0SumEquivOfDense_apply (hdense : Dense (finiteSums J)) (a : A) :179    compactC0SumEquivOfDense J hJ H E hdense a =180      C0DirectSum.equiv (Fiber J)181        (fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))182        (Equiv.refl ι) E ((c0SumEquivOfDense J hJ hdense).symm a) := rfl183184/-- The inverse of the compact c₀-model is literally the transported sum185homomorphism already constructed without density. -/186@[simp]187theorem compactC0SumEquivOfDense_symm_apply188    (hdense : Dense (finiteSums J)) (x : CompactOperatorC0Sum H) :189    (compactC0SumEquivOfDense J hJ H E hdense).symm x =190      compactC0SumHom J hJ H E x := rfl191192/-- The forward coordinate formula uses exactly the specified fiber model. -/193@[simp]194theorem eval_compactC0SumEquivOfDense (hdense : Dense (finiteSums J)) (a : A) (i : ι) :195    C0DirectSum.eval196      (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i197      (compactC0SumEquivOfDense J hJ H E hdense a) =198      E i (C0DirectSum.eval (Fiber J) i ((c0SumEquivOfDense J hJ hdense).symm a)) := by199  exact C0DirectSum.eval_equiv_apply (Fiber J)200    (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j))201    (Equiv.refl ι) E ((c0SumEquivOfDense J hJ hdense).symm a) i202203/-- On each displayed ideal, the model is its specified compact equivalence204followed by the corresponding single-coordinate embedding. -/205@[simp]206theorem compactC0SumEquivOfDense_coe (hdense : Dense (finiteSums J))207    (i : ι) (a : Fiber J i) :208    compactC0SumEquivOfDense J hJ H E hdense (a : A) =209      C0DirectSum.single210        (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i (E i a) := by211  apply (compactC0SumEquivOfDense J hJ H E hdense).symm.injective212  calc213    (compactC0SumEquivOfDense J hJ H E hdense).symm214        (compactC0SumEquivOfDense J hJ H E hdense (a : A)) = (a : A) :=215      (compactC0SumEquivOfDense J hJ H E hdense).symm_apply_apply (a : A)216    _ = ((E i).symm (E i a) : A) :=217      congrArg (fun z : Fiber J i => (z : A)) ((E i).symm_apply_apply a).symm218    _ = compactC0SumHom J hJ H E219        (C0DirectSum.single220          (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i (E i a)) :=221      (compactC0SumHom_single J hJ H E i (E i a)).symm222    _ = (compactC0SumEquivOfDense J hJ H E hdense).symm223        (C0DirectSum.single224          (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i (E i a)) :=225      (compactC0SumEquivOfDense_symm_apply J hJ H E hdense _).symm226227/-- The inverse single-coordinate formula takes values in the actual ideal228carrier before inclusion into `A`. -/229@[simp]230theorem compactC0SumEquivOfDense_symm_single (hdense : Dense (finiteSums J)) (i : ι)231    (T : ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i)) :232    (compactC0SumEquivOfDense J hJ H E hdense).symm233      (C0DirectSum.single234        (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i T) =235      ((E i).symm T : A) := by236  rw [compactC0SumEquivOfDense_symm_apply, compactC0SumHom_single]237238/-- The model sends finite ambient ideal sums to the corresponding finite239compact-coordinate sums. -/240@[simp]241theorem compactC0SumEquivOfDense_sum (hdense : Dense (finiteSums J))242    (s : Finset ι) (a : ∀ i, Fiber J i) :243    compactC0SumEquivOfDense J hJ H E hdense (∑ i ∈ s, (a i : A)) =244      ∑ i ∈ s, C0DirectSum.single245        (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i (E i (a i)) := by246  simp only [map_sum, compactC0SumEquivOfDense_coe]247248/-- The conditional ambient-to-c₀ equivalence is isometric. -/249theorem isometry_compactC0SumEquivOfDense (hdense : Dense (finiteSums J)) :250    Isometry (compactC0SumEquivOfDense J hJ H E hdense) :=251  NonUnitalStarAlgHom.isometry252    (compactC0SumEquivOfDense J hJ H E hdense).toNonUnitalStarAlgHom253    (compactC0SumEquivOfDense J hJ H E hdense).injective254255@[simp]256theorem norm_compactC0SumEquivOfDense (hdense : Dense (finiteSums J)) (a : A) :257    ‖compactC0SumEquivOfDense J hJ H E hdense a‖ = ‖a‖ :=258  NonUnitalStarAlgHom.norm_map259    (compactC0SumEquivOfDense J hJ H E hdense).toNonUnitalStarAlgHom260    (compactC0SumEquivOfDense J hJ H E hdense).injective a261262@[simp]263theorem norm_compactC0SumEquivOfDense_symm (hdense : Dense (finiteSums J))264    (x : CompactOperatorC0Sum H) :265    ‖(compactC0SumEquivOfDense J hJ H E hdense).symm x‖ = ‖x‖ := by266  rw [compactC0SumEquivOfDense_symm_apply, norm_compactC0SumHom]267268section GivenCompactModels269270variable (pi : ∀ i, NonUnitalCStarRepresentation (Fiber J i) (H i))271variable (hpi : ∀ i, IsCompactOperatorModel (pi i))272273/-- A given family of exact compact representations supplies the fiber274equivalences through the existing `compactOperatorStarAlgEquiv` constructor.275Orthogonality and density remain explicit inputs. -/276def compactC0SumEquivOfModels (hdense : Dense (finiteSums J)) :277    A ≃⋆ₐ[ℂ] CompactOperatorC0Sum H :=278  compactC0SumEquivOfDense J hJ H279    (fun i => compactOperatorStarAlgEquiv (pi i) (hpi i)) hdense280281/-- In the representation-input version, each coordinate acts by the original282specified representation, not by an abstractly chosen replacement. -/283@[simp]284theorem eval_compactC0SumEquivOfModels (hdense : Dense (finiteSums J)) (a : A) (i : ι) :285    (C0DirectSum.eval286      (fun j => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H j)) i287      (compactC0SumEquivOfModels J hJ H pi hpi hdense a) : H i →L[ℂ] H i) =288      pi i (C0DirectSum.eval (Fiber J) i ((c0SumEquivOfDense J hJ hdense).symm a)) := by289  unfold compactC0SumEquivOfModels290  rw [eval_compactC0SumEquivOfDense]291  rfl292293/-- The representation-input compact model also preserves the original norm. -/294@[simp]295theorem norm_compactC0SumEquivOfModels (hdense : Dense (finiteSums J)) (a : A) :296    ‖compactC0SumEquivOfModels J hJ H pi hpi hdense a‖ = ‖a‖ :=297  norm_compactC0SumEquivOfDense J hJ H298    (fun i => compactOperatorStarAlgEquiv (pi i) (hpi i)) hdense a299300end GivenCompactModels301302end MathlibAnnex.Analysis.CStarAlgebra.ClosedStarIdeal