OAI/Analysis/KadisonSimilarity/Tracial/GeneratedFiniteFactorModel.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The constructed matrix subfactor in a normal trace representation supplies the finite-factor model in the original representation. Only the prescribed ultrapower free position remains a local input.

  1. def OAI.KadisonSimilarity.generatedOriginalInclusion line 24
  2. theorem OAI.KadisonSimilarity.generatedOriginalInclusion_trace line 29
  3. def OAI.KadisonSimilarity.generatedFiniteFactorModel line 54

    Source documentation

    No matrix presentation, matrix-size divergence, or source-trace properties are assumed separately from the constructed diffuse subfactor.

    def generatedFiniteFactorModel : FiniteFactorModel P where
…

    Mentions: OAI.KadisonSimilarity.FiniteFactorModel