OAI/Analysis/KadisonKastler/ConjugateVectorSupport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Conjugate supports of a symmetric vector

For a conjugation interchanging an algebra and its commutant, the two support projections of a fixed vector are conjugate. This is the support identity used when passing the central-vector construction to a full corner.

  1. def OAI.KadisonKastler.conjugateAlgebraProjection line 20
  2. theorem OAI.KadisonKastler.conjugateAlgebraProjection_fixes line 38
  3. theorem OAI.KadisonKastler.vectorSupportProjection_conjugate line 46