Banach and operator algebras

Banach algebras and C*- and von Neumann algebras: exponentials and product formulas in Banach algebras, GNS, Gelfand–Naimark, bicommutant, Kaplansky density, Russo–Dye, Stinespring, Kadison–Singer and the Marcus–Spielman–Srivastava theorem.

• Exponential limits and the Lie–Trotter formula
• GNS construction
• Inverses as limits of polynomials in Banach algebras
• Kadison–Singer problem
• Kaplansky density theorem
• Von Neumann bicommutant theorem

TheoremGelfand–Naimark theorem#✓fully proved

For every unital C*-algebra \(A\) there are a complex Hilbert space \(H\) and a unital \(*\)-homomorphism \(\pi : A \to B(H)\) into the algebra of bounded operators on \(H\) such that \(\pi\) is injective and isometric: \(\|\pi(a)\| = \|a\|\) for every \(a \in A\).

theorem cStarAlgebra_gelfandNaimark
    (A : Type u) [CStarAlgebra A] :
    ∃ (H : Type u) (hH1 : NormedAddCommGroup H)
      (hH2 : InnerProductSpace ℂ H) (hH3 : CompleteSpace H)
      (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)),
      Function.Injective π ∧ ∀ a : A, ‖π a‖ = ‖a‖

Sources

• Gelfand–Naimark theorem, I. M. Gelfand–M. A. Naimark, Mat. Sb. 12 (1943); see Murphy, C*-Algebras and Operator Theory, A Course in Operator Theory; Lean is isometric injective star-homomorphism into B(H) form.

TheoremRusso–Dye theorem#✓fully proved

In a unital C*-algebra \(A\), the norm closure of the convex hull of the unitary elements of \(A\) equals the closed unit ball \(\{a \in A : \|a\| \le 1\}\).

theorem cStarAlgebra_russoDye
    (A : Type u) [CStarAlgebra A] :
    closure (convexHull ℝ (unitary A : Set A)) = Metric.closedBall (0 : A) 1

Sources

• Russo–Dye theorem, B. Russo–H. Dye, Duke Math. J. 33 (1966); see Takesaki I; Lean is norm-closure of convex hull of unitaries equals closed unit ball.

TheoremStinespring dilation theorem#✓fully proved

Let \(A\) be a unital C*-algebra with its standard order, let \(H\) be a complex Hilbert space, and let \(\varphi : A \to B(H)\) be a completely positive map. Then there are a complex Hilbert space \(K\), a unital \(*\)-homomorphism \(\pi : A \to B(K)\) and a bounded linear map \(V : H \to K\) such that \(\varphi(a) = V^* \pi(a) V\) for every \(a \in A\), where \(V^*\) is the adjoint of \(V\).

theorem stinespring_dilation
    {A H : Type u} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A]
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    (φ : A →CP (H →L[ℂ] H)) :
    ∃ (K : Type u) (_ : NormedAddCommGroup K) (_ : InnerProductSpace ℂ K)
        (_ : CompleteSpace K) (π : A →⋆ₐ[ℂ] (K →L[ℂ] K)) (V : H →L[ℂ] K),
      ∀ (a : A) (x : H), (φ a) x = (V†) ((π a) (V x))

Sources

• Stinespring dilation theorem, W. F. Stinespring, Proc. Amer. Math. Soc. 6 (1955); see Paulsen, Completely Bounded Maps; Lean is general CP map A →CP B(H) dilation V† π(a) V, not finite-dimensional Kraus form.

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.