The normal GNS space of a nontrivial von Neumann algebra is nontrivial
ProvedOAI.BoundedHochschild.KadisonRingrose.normalGNS_nontrivialThroughout, is a unital C*-algebra with a partial order making it star-ordered, is a complex Banach space, and is an isometric conjugate-linear isomorphism, so is a von Neumann algebra with predual (the Lean hypothesis e). The normal GNS space NormalGNS e is the subspace of normal vectors of the universal GNS representation of . If is nontrivial, then NormalGNS e is nontrivial.
Formalization Note The statement is verbatim from OpenAI's Lean development, with the listed Definitions imported in place of the upstream modules; the definitions are supporting code for this statement. Only the keyword lemma, where used upstream, becomes theorem, and a leading include ... in or omit ... in moves to the preamble. It is a step of the Lean proof of the vanishing of higher bounded Hochschild cohomology.
import Mathlib
import Definitions.Def_KadisonRingroseSupport2
namespace OAI
noncomputable section
open scoped ComplexOrder InnerProductSpace
namespace BoundedHochschild.KadisonRingrose
universe u
variable {M X : Type u} [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M]
[NormedAddCommGroup X] [NormedSpace ℂ X] [CompleteSpace X]
theorem normalGNS_nontrivial [Nontrivial M] (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) :
Nontrivial (NormalGNS e) := by
sorry
end BoundedHochschild.KadisonRingrose
end
end OAI