OAI/Analysis/KadisonKastler/SpatialProductSeparating.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Separating product vectors

The modular conjugations on the two original spaces supply dense commutant orbits. Their tensor product commutes with the generated spatial algebra, so its cyclic product vector separates that algebra.

  1. theorem OAI.KadisonKastler.ModularConjugationData.commutant_cyclic line 23
  2. theorem OAI.KadisonKastler.spatialProduct_commutants_le line 34
  3. theorem OAI.KadisonKastler.separating_spatialProduct_vector line 49

    Source documentation

    A cyclic vector in each original algebra is separating for their spatial product when each space carries its modular conjugation.

    theorem separating_spatialProduct_vector
    (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K) (Ω : H) (ξ : K)
    (hM : DenseRange (algebraVectorMap M Ω))
    (hD : DenseRange (algebraVectorMap D ξ))
    (dM : ModularConjugationData M Ω) (dD : ModularConjugationData D ξ) :
    Function.Injective (algebraVectorMap (spatialProductAlgebra M D) (tensorVector ξ Ω)) := by
…

    Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.ModularConjugationData, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.tensorVector