OAI/Analysis/BoundedHochschild/UniversalGNSRepresentation.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

A faithful Hilbert-space realization for the operator-valued averaging argument. It uses only the already proved separation by positive functionals.

  1. abbrev OAI.BoundedHochschild.KadisonRingrose.UniversalGNS line 20

    Source documentation

    The Hilbert sum of the cyclic representations of all positive functionals.

    abbrev UniversalGNS (M : Type*) [CStarAlgebra M] [PartialOrder M] [StarOrderedRing M] :=
…
  2. def OAI.BoundedHochschild.KadisonRingrose.universalGNSAction line 23
  3. lemma OAI.BoundedHochschild.KadisonRingrose.universalGNSAction_apply line 32
  4. lemma OAI.BoundedHochschild.KadisonRingrose.universalGNSAction_norm line 35
  5. def OAI.BoundedHochschild.KadisonRingrose.universalGNSOperator line 47
  6. lemma OAI.BoundedHochschild.KadisonRingrose.universalGNSOperator_apply line 54
  7. def OAI.BoundedHochschild.KadisonRingrose.universalGNSRepresentation line 58

    Source documentation

    Every C*-algebra acts on the Hilbert sum of its positive cyclic representations.

    def universalGNSRepresentation : M →⋆ₐ[ℂ] (UniversalGNS M →L[ℂ] UniversalGNS M) where
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.UniversalGNS

  8. lemma OAI.BoundedHochschild.KadisonRingrose.universalGNSRepresentation_apply line 77
  9. lemma OAI.BoundedHochschild.KadisonRingrose.eq_zero_of_all_positive_functionals line 81
  10. theorem OAI.BoundedHochschild.KadisonRingrose.universalGNSRepresentation_injective line 90

    Source documentation

    The cyclic representations together separate the original algebra.

    theorem universalGNSRepresentation_injective :
    Function.Injective (universalGNSRepresentation (M := M)) := by
…

    Mentions: OAI.BoundedHochschild.KadisonRingrose.universalGNSRepresentation

  11. theorem OAI.BoundedHochschild.KadisonRingrose.universalGNSRepresentation_norm line 107