MathlibAnnex/Analysis/CStarAlgebra/CompactModel.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.

1import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap2import Mathlib.Analysis.InnerProductSpace.LinearMap3import Mathlib.Analysis.Normed.Operator.Compact.FiniteDimension4import Mathlib.Topology.Algebra.Module.FiniteDimension56/-!7# Algebraic models of the compact operators89The fixed Mathlib version exposes compact operators as a predicate/submodule,10not as a bundled star algebra.  `IsCompactOperatorModel` is the exact range11characterization of an ordinary nonunital star-algebra isomorphism onto all12compact operators.13-/1415set_option autoImplicit false1617open scoped InnerProduct1819namespace MathlibAnnex.Analysis.CStarAlgebra2021universe u v2223variable {A : Type u}24variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]2526/-- A nonunital star representation that is injective and has precisely the27compact operators as its range.  This is the unbundled form of a star28isomorphism with `K(H)`. -/29def IsCompactOperatorModel [NonUnitalCStarAlgebra A]30    (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : Prop :=31  Function.Injective e ∧32    (∀ a : A, IsCompactOperator (e a)) ∧33    ∀ T : H →L[ℂ] H, IsCompactOperator T → ∃ a : A, e a = T3435omit [CompleteSpace H] in36/-- Rank-one operators are compact, proved by factoring through the37one-dimensional scalar field. -/38theorem isCompactOperator_rankOne (x y : H) :39    IsCompactOperator (InnerProductSpace.rankOne ℂ x y) := by40  rw [InnerProductSpace.rankOne_def']41  exact (isCompactOperator_of_locallyCompactSpace_dom42    (innerSL ℂ y)).clm_comp43      (ContinuousLinearMap.toSpanSingleton ℂ x)4445theorem map_one_eq_one_of_isCompactOperatorModel [Nontrivial H]46    [CStarAlgebra A]47    (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) (he : IsCompactOperatorModel e) : e 1 = 1 := by48  apply ContinuousLinearMap.ext49  intro x50  change e 1 x = x51  obtain ⟨y, hy⟩ := exists_norm_ne_zero H52  let z : H := ‖y‖⁻¹ • y53  have hz : ‖z‖ = 1 := by54    dsimp [z]55    simp [norm_smul, inv_mul_cancel₀ hy]56  let T : H →L[ℂ] H := InnerProductSpace.rankOne ℂ x z57  obtain ⟨a, ha⟩ := he.2.2 T (isCompactOperator_rankOne x z)58  have hleft : e 1 * T = T := by59    rw [← ha, ← map_mul, one_mul]60  have hTz : T z = x := by61    simp [T, InnerProductSpace.rankOne_apply,62      inner_self_eq_norm_sq_to_K, hz]63  calc64    e 1 x = e 1 (T z) := congrArg (e 1) hTz.symm65    _ = (e 1 * T) z := rfl66    _ = T z := congrArg (fun S : H →L[ℂ] H => S z) hleft67    _ = x := hTz6869/-- A nonzero unital infinite-dimensional C-star algebra cannot be70star-isomorphic to the compact operators on any Hilbert space, including the71zero Hilbert space. -/72theorem not_isCompactOperatorModel_of_infiniteDimensional73    [CStarAlgebra A] [Nontrivial A] (hA : ¬ FiniteDimensional ℂ A)74    (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : ¬ IsCompactOperatorModel e := by75  intro he76  have hH : ¬ Subsingleton H := by77    intro hsub78    letI : Subsingleton H := hsub79    have hmap : e (1 : A) = e 0 := Subsingleton.elim _ _80    exact one_ne_zero (he.1 hmap)81  letI : Nontrivial H := not_subsingleton_iff_nontrivial.mp hH82  have hone := map_one_eq_one_of_isCompactOperatorModel e he83  have hcompact_one : IsCompactOperator ((1 : H →L[ℂ] H) : H → H) := by84    rw [← hone]85    exact he.2.1 186  haveI : FiniteDimensional ℂ H := by87    apply FiniteDimensional.of_isCompactOperator_id88    change IsCompactOperator (fun x : H => x)89    exact hcompact_one90  haveI : FiniteDimensional ℂ (H →L[ℂ] H) :=91    ContinuousLinearMap.finiteDimensional92  exact hA93    (FiniteDimensional.of_injective (LinearMapClass.linearMap e) he.1)9495end MathlibAnnex.Analysis.CStarAlgebra