Kaplansky density theorem

AbbreviationStrong-operator operators as bounded operators#✓fully proved

For a complex Hilbert space \(H\), this sends a bounded linear operator on \(H\), viewed in the space of operators with the strong operator topology (pointwise convergence on \(H\)), to the same operator viewed in \(B(H)\) with the operator norm. It is the identity on underlying maps.

noncomputable abbrev toBounded {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] (x : H →Lₚₜ[ℂ] H) : H →L[ℂ] H :=
  (ContinuousLinearMap.toUniformConvergenceCLM (RingHom.id ℂ) H {s : Set H | Finite s}).symm x

Used by 1

Used byKaplansky density theorem

TheoremKaplansky density theorem#✓fully proved

Let \(H\) be a complex Hilbert space and let \(S\) be a unital \(*\)-subalgebra of the algebra \(B(H)\) of bounded operators on \(H\), with operator norm \(\|\cdot\|\). Take closures in the strong operator topology on \(B(H)\), the topology of pointwise convergence on \(H\), and write \(\overline{S}\) for the strong closure of \(S\). Then the strong closure of the unit ball \(\{x \in S : \|x\| \le 1\}\) of \(S\) equals the unit ball \(\{y \in \overline{S} : \|y\| \le 1\}\) of \(\overline{S}\).

public theorem kaplansky_density_theorem
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (S : StarSubalgebra ℂ (H →L[ℂ] H)) :
    closure ({x : H →Lₚₜ[ℂ] H | toBounded x ∈ (S : Set (H →L[ℂ] H)) ∧ ‖toBounded x‖ ≤ 1} :
      Set (H →Lₚₜ[ℂ] H))
    = {y : H →Lₚₜ[ℂ] H | y ∈ closure ({p : H →Lₚₜ[ℂ] H | toBounded p ∈ (S : Set (H →L[ℂ] H))} :
      Set (H →Lₚₜ[ℂ] H)) ∧ ‖toBounded y‖ ≤ 1}

Sources

• Kaplansky density theorem, I. Kaplansky, Pacific J. Math. 1 (1951), 227–232; see Takesaki, Theory of Operator Algebras I, Density Theorem and Kadison–Ringrose Vol I; Lean is SOT-closure equality of unit balls via toBounded conversion, full infinite-dimensional form.

Uses 1

Statement usesStrong-operator operators as bounded operators

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.