OAI/Analysis/KadisonKastler/SharedTracialRightAction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A shared tracial right action determines the neighboring vector state

  1. theorem OAI.KadisonKastler.StandardTracialPosition.common_right_representatives line 16
  2. theorem OAI.KadisonKastler.StandardTracialPosition.neighbor_trace line 39

    Source documentation

    Once the right action is aligned, the same unit vector implements the neighboring factor's trace.

    theorem StandardTracialPosition.neighbor_trace
    {M N R : VonNeumannAlgebra H} (p : StandardTracialPosition M)
    (hRM : R ≤ M) (hRN : R ≤ N)
    (hN : Generator.IsII1Factor N.toStarSubalgebra)
    (hirr : ∀ a : Algebra N, a.val ∈ R.commutant → ∃ c : ℂ, a = c • 1)
    (hright : conjugateRightAlgebra p.conjugation p.conjugation_involutive R ≤ N.commutant)
    (x : Algebra N) :
    inner ℂ p.vector (x.val p.vector) = (concreteFactorTrace hN).toLinearMap x :=
…

    Mentions: OAI.KadisonKastler.StandardTracialPosition, OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugateRightAlgebra, OAI.KadisonKastler.concreteFactorTrace