Email Gateway (Jun 01 2026 at 16:04): Email Gateway (Jun 01 2026 at 16:04):From: Manuel Eberl <manuel@pruvisto.org>
The Gelfand–Naimark–Segal Construction
by Richard Schmoetten and Jacques D. Fleuriot
Abstract: This entry formalises complete normed algebras equipped with
an involution, so-called C*-algebras. We provide both a class
definition, and a locale for C*-algebras on carrier sets in the spirit
of existing developments of linear algebra and smooth manifolds. Bounded
operators on a complex Hilbert space, with the operator norm and
adjoints, form such an algebra. The main theorem of this entry is a
result in the converse direction: the Gelfand–Naimark–Segal (GNS)
construction, which starts with a single suitable functional on a
C*-algebra in order to obtain both a Hilbert space and a representation
of the algebra in terms of bounded operators on that space. This is
implemented as a type construction in Isabelle/HOL, taking advantage of
existing mechanisms for quotient types, and integrating with existing
type classes for Hilbert spaces and Cauchy completions.
https://isa-afp.org/entries/Gelfand_Naimark_Segal.html
Enjoy,
Manuel
Last updated: Jun 12 2026 at 04:13 UTC