OAI/Analysis/KadisonKastler/SimpleIrreducibleRepresentation.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A faithful irreducible representation for Sakai's construction

Compactness of the state space gives a pure state. Its GNS representation is irreducible, and simplicity makes the representation faithful. These steps use the existing state-space and GNS proofs, with no representation existence hypothesis.

  1. theorem OAI.KadisonKastler.exists_pure_state line 24
  2. theorem OAI.KadisonKastler.exists_simple_irreducible_representation line 37