OAI/Analysis/KadisonKastler/RelativeCentralStandardSpace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

The concrete standard space for a finite matrix relative commutant

The relative algebra's cyclic orbit is exactly the matrix central-vector space. The original conjugation restricts to this same Hilbert subspace.

  1. def OAI.KadisonKastler.centralSpaceConjugation line 22

    Source documentation

    The antiunitary on the actual central-vector subspace.

    def centralSpaceConjugation (N : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H)
    (hJ : Function.Involutive J) :
    centralVectorSpace N J ≃ₗᵢ⋆[ℂ] centralVectorSpace N J where
…

    Mentions: OAI.KadisonKastler.centralVectorSpace

  2. theorem OAI.KadisonKastler.centralSpaceConjugation_coe line 33
  3. theorem OAI.KadisonKastler.centralSpaceConjugation_involutive line 38
  4. theorem OAI.KadisonKastler.relative_cyclicOrbitSpace_eq line 50
  5. theorem OAI.KadisonKastler.relative_cyclicOrbit_projection_eq line 59
  6. theorem OAI.KadisonKastler.relative_vector_separating line 67
  7. theorem OAI.KadisonKastler.matrixCentralProjection_cyclic line 79
  8. theorem OAI.KadisonKastler.relative_averaged_cyclicOrbitSpace_eq line 95