OAI/Analysis/KadisonKastler/MatrixCommonPositionConstruction.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Constructed common tracial position for an increasing matrix subfactor

This proves the instance of CCSSWW, Lemma 4.10, used by the finite-factor application. The common algebra is the actual increasing full-matrix closure.

  1. theorem OAI.KadisonKastler.exists_commonTracialPosition_of_matrixStages line 26