OAI/Analysis/KadisonSimilarity/Tracial/ConcreteFiniteFactorModel.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Construct the finite-factor model from a concrete subfactor and its matrix presentation. The source trace and both GNS normality proofs are derived from the ambient normal trace.

  1. theorem OAI.KadisonSimilarity.includedPositiveTrace_one line 24
  2. theorem OAI.KadisonSimilarity.includedPositiveTrace_tracial line 27
  3. theorem OAI.KadisonSimilarity.includedPositiveTrace_faithful line 32
  4. def OAI.KadisonSimilarity.concreteFiniteFactorModel line 56

    Source documentation

    The finite-factor presentation has no separate trace-normality or source-trace existence premise.

    def concreteFiniteFactorModel : FiniteFactorModel P where
…

    Mentions: OAI.KadisonSimilarity.FiniteFactorModel

  5. theorem OAI.KadisonSimilarity.concrete_finite_factor_estimate line 79