OAI/Analysis/KadisonKastler/ScalarMatrixTrace.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The canonical traces of the finite matrix-model coordinates

  1. def OAI.KadisonKastler.scalarTrace line 15

    Source documentation

    The normalized trace on the scalar algebra.

    def scalarTrace : FaithfulTracialState ℂ where
…

    Mentions: OAI.KadisonKastler.FaithfulTracialState

  2. abbrev OAI.KadisonKastler.FiniteMatrixModel line 30

    Source documentation

    The coordinate algebra M_n(M_(j+1)(C)) in the finite-matrix model.

    abbrev FiniteMatrixModel (n j : ℕ) :=
…
  3. def OAI.KadisonKastler.finiteMatrixModelTrace line 34

    Source documentation

    The normalized trace on the finite-matrix-model coordinate.

    def finiteMatrixModelTrace (n : ℕ) [NeZero n] (j : ℕ) :
    FaithfulTracialState (FiniteMatrixModel n j) := matrixTrace (matrixTrace scalarTrace)
…

    Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.matrixTrace, OAI.KadisonKastler.scalarTrace