OAI/Analysis/KadisonKastler/QuotientSeparability.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Separability of the constant algebra in a trace quotient

  1. theorem OAI.KadisonKastler.TraceQuotientMap.constant_traceSeparable line 20

    Source documentation

    A separably acting finite-vector trace supplies the separability premise for the constant subalgebra of the represented ultrapower.

    theorem TraceQuotientMap.constant_traceSeparable (Q : TraceQuotientMap τ σ ω)
    (hτ : FiniteVectorTrace τ) :
    TraceSeparable σ (Q.constant.range : Set C) := by
…

    Mentions: OAI.KadisonKastler.TraceQuotientMap, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.TraceSeparable