OAI/Analysis/KadisonKastler/FiniteFactorPrime.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Primeness of finite factors from trace averaging

The scalar relative orbit average gives the prime-algebra property needed for Jordan orientation, without introducing central-support machinery.

  1. theorem OAI.KadisonKastler.finiteFactor_isPrimeAlgebra line 21

    Source documentation

    A finite factor is prime: annihilating all middle factors forces one of the two outside factors to vanish.

    theorem finiteFactor_isPrimeAlgebra
    (hM : Generator.IsII1Factor M.toStarSubalgebra) : IsPrimeAlgebra (Algebra M) := by
…

    Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.IsPrimeAlgebra, OAI.KadisonKastler.Algebra