OAI/Analysis/KadisonKastler/FaithfulTensorRange.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The tensor isomorphism for the explicit faithful cyclic representation

Only this representation change is needed by fixed-factor preparation. The range is identified with the spatial product by its two generating legs and bounded weak continuity, without an arbitrary-isomorphism input.

  1. theorem OAI.KadisonKastler.faithfulTensorHom_boundedWeakNormal line 26
  2. theorem OAI.KadisonKastler.faithfulTensorHom_generators_map_le line 33
  3. theorem OAI.KadisonKastler.faithfulTensorHom_mem line 60
  4. theorem OAI.KadisonKastler.faithfulTensorHom_generated_range line 78
  5. def OAI.KadisonKastler.faithfulTensorEquiv line 98
  6. def OAI.KadisonKastler.tensorCompatibleCyclicRepresentation line 107

    Source documentation

    The particular cyclic representation for which the tensor extension has just been constructed.

    def tensorCompatibleCyclicRepresentation (M : VonNeumannAlgebra H) :
    FaithfulCyclicRepresentation M where
…

    Mentions: OAI.KadisonKastler.FaithfulCyclicRepresentation