OAI/Analysis/KadisonKastler/NormalizedUltrapower.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Using the canonical ultrapower with an explicit normalized trace

  1. theorem OAI.KadisonKastler.publishedTracialUltrapower_for_trace line 22

    Source documentation

    The published canonical construction also applies to an explicitly constructed normalized faithful trace, since uniqueness identifies it with the canonical trace on the same finite factor.

    theorem publishedTracialUltrapower_for_trace
    (hpub : PublishedTracialUltrapower.{u})
    (hM : Generator.IsII1Factor M.toStarSubalgebra)
    (τ : FaithfulTracialState (Algebra M))
    (ω : Ultrafilter ℕ) (hω : (ω : Filter ℕ) ≤ atTop) :
    Nonempty (TracialUltrapower τ ω) := by
…

    Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.TracialUltrapower