WStarAlgebra.exists_predual
theorem WStarAlgebra.exists_predual :
∀ {M : Type u} [inst : NormedRing M] [inst_1 : StarRing M] [inst_2 : CstarRing M] [inst_3 : Module ℂ M]
[inst_4 : NormedAlgebra ℂ M] [inst_5 : StarModule ℂ M] [self : WStarAlgebra M],
∃ X x x_1, ∃ (_ : CompleteSpace X), Nonempty (NormedSpace.Dual ℂ X ≃ₗᵢ⋆[ℂ] M)
The theorem states that for any Banach space `M` that satisfies several properties -- specifically, being a normed ring, a star ring, a C*-ring, a complex module, a normed algebra over the complex numbers, a star module, and a W*-algebra -- there exists a Banach space `X` such that the topological dual of `X` is conjugate linearly isometrically isomorphic to `M`. In simpler terms, the theorem says that for a specific kind of complex Banach space (satisfying all these conditions), there is another Banach space whose dual behaves exactly like the original space in terms of its structure and norms. This is under the isomorphism that preserves the structure and the norms (with possibly a conjugate linear transformation).
More concisely: For any complex Banach space `M` that is a normed ring, star ring, C*-ring, complex module, normed algebra over the complex numbers, star module, and W*-algebra, there exists a conjugate linearly isomorphic Banach space `X` such that their topological duals are isometric.
|
VonNeumannAlgebra.centralizer_centralizer'
theorem VonNeumannAlgebra.centralizer_centralizer' :
∀ {H : Type u} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
(self : VonNeumannAlgebra H), self.carrier.centralizer.centralizer = self.carrier
This theorem states that for any Von Neumann algebra (a kind of *-algebra of bounded operators on a Hilbert space), its double commutant, also known as the centralizer of its centralizer, is equal to the algebra itself. Here, the centralizer of a set of operators is the set of all operators that commute with every operator in the original set. The theorem is valid for any Hilbert space `H` that is a complete inner product space over the complex numbers and a normed additive commutative group.
More concisely: For any Von Neumann algebra on a Hilbert space, its double commutant equals the algebra itself.
|