OAI/Analysis/KadisonKastler/FaithfulCyclicConstruction.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

A faithful cyclic representation from a countable amplification

The weighted dense vector is separating for the diagonal action. Its closed orbit gives a faithful cyclic restriction. Kaplansky density and weak compactness of the original operator ball show that the restricted image is already a von Neumann algebra.

  1. def OAI.KadisonKastler.countableDiagonalHom line 28
  2. abbrev OAI.KadisonKastler.faithfulCyclicSpace line 32
  3. def OAI.KadisonKastler.faithfulCyclicVector line 35
  4. theorem OAI.KadisonKastler.norm_faithfulCyclicVector line 38
  5. instance OAI.KadisonKastler.faithfulCyclicSpace_nontrivial line 41
  6. def OAI.KadisonKastler.faithfulCyclicHom line 49
  7. theorem OAI.KadisonKastler.faithfulCyclicHom_apply line 56
  8. theorem OAI.KadisonKastler.faithfulCyclicHom_separating line 63
  9. theorem OAI.KadisonKastler.faithfulCyclicHom_injective line 76
  10. theorem OAI.KadisonKastler.faithfulCyclicHom_norm line 81
  11. theorem OAI.KadisonKastler.faithfulCyclicHom_cyclic line 88
  12. theorem OAI.KadisonKastler.faithfulCyclicHom_tendsto_weak line 104
  13. def OAI.KadisonKastler.faithfulCyclicAlgebra line 114
  14. theorem OAI.KadisonKastler.faithfulCyclicHom_surjective_unitBall line 119

    Source documentation

    The full unit ball of the generated algebra is already the restricted image.

    theorem faithfulCyclicHom_surjective_unitBall (M : VonNeumannAlgebra H)
    (T : faithfulCyclicSpace M →L[ℂ] faithfulCyclicSpace M)
    (hT : T ∈ faithfulCyclicAlgebra M) (hnT : ‖T‖ ≤ 1) :
    ∃ a : Algebra M, ‖a‖ ≤ 1 ∧ faithfulCyclicHom M a = T := by
…

    Mentions: OAI.KadisonKastler.faithfulCyclicSpace, OAI.KadisonKastler.faithfulCyclicAlgebra, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.faithfulCyclicHom

  15. theorem OAI.KadisonKastler.faithfulCyclicHom_surjective line 154
  16. def OAI.KadisonKastler.faithfulCyclicEquiv line 175
  17. theorem OAI.KadisonKastler.faithfulCyclicEquiv_coe line 189
  18. theorem OAI.KadisonKastler.faithfulCyclicAlgebra_separating line 192
  19. theorem OAI.KadisonKastler.publishedFaithfulCyclicRepresentation line 207

    Source documentation

    Blackadar's faithful cyclic representation input, proved for the required separably acting case by an explicit countable amplification.

    theorem publishedFaithfulCyclicRepresentation : PublishedFaithfulCyclicRepresentation.{u} := by
…