OAI/Analysis/BoundedHochschild/UnitaryPredualAction.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

The isometric unitary action on a von Neumann predual.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPullback_one line 21
  2. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPullback_mul line 25
  3. def OAI.BoundedHochschild.KadisonRingrose.unitaryDualEquiv line 31

    Source documentation

    Unitary conjugation acts isometrically on bounded scalar functionals.

    def unitaryDualEquiv (u : unitary M) : StrongDual ℂ M ≃ₗᵢ[ℂ] StrongDual ℂ M where
…
  4. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPullback_normal line 49
  5. def OAI.BoundedHochschild.KadisonRingrose.normalUnitaryEquiv line 56

    Source documentation

    The same action restricted to normal functionals.

    def normalUnitaryEquiv (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (u : unitary M) :
    normalDual e ≃ₗᵢ[ℂ] normalDual e where
…
  6. def OAI.BoundedHochschild.KadisonRingrose.predualNormalEquiv line 67

    Source documentation

    Identification of the predual with the normal functionals.

    def predualNormalEquiv (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) : X ≃ₗᵢ⋆[ℂ] normalDual e :=
…
  7. lemma OAI.BoundedHochschild.KadisonRingrose.predualNormalEquiv_coe line 71
  8. def OAI.BoundedHochschild.KadisonRingrose.unitaryPredualAction line 75

    Source documentation

    Pullback by the inverse unitary gives a left group action on the predual.

    def unitaryPredualAction (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M) (u : unitary M) : X ≃ₗᵢ[ℂ] X :=
…
  9. lemma OAI.BoundedHochschild.KadisonRingrose.predualEmbedding_unitaryAction line 79
  10. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPredualAction_one line 87
  11. lemma OAI.BoundedHochschild.KadisonRingrose.unitaryPredualAction_mul line 92