PublishedUltrapower.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The published tracial-ultraproduct construction

Popa, Independence properties in subalgebras of ultraproduct II₁ factors, J. Funct. Anal. 266 (2014), §1.6 (arXiv:1308.3982v3, printed pp. 7–8), recalls the tracial ultraproduct as a finite von Neumann algebra, with trace the ultralimit of the coordinate traces. For a constant sequence of II₁ factors it is again a II₁ factor.

The input below contains exactly that construction. The two-norm kernel property used by clipping is derived afterwards from faithfulness and the trace formula; it is not an additional input.

structure OAI.KadisonKastler.TracialUltrapower line 31
Source documentation
A represented tracial ultrapower, with the published coordinate trace formula. The quotient is a concrete von Neumann algebra.
```
structure TracialUltrapower (τ : FaithfulTracialState B) (ω : Ultrafilter ℕ) where
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState
def OAI.KadisonKastler.TracialUltrapower.trace line 48
Source documentation
The canonical faithful normal trace of the represented II₁ factor.
```
def TracialUltrapower.trace {τ : FaithfulTracialState B} {ω : Ultrafilter ℕ}
    (Q : TracialUltrapower τ ω) : FaithfulTracialState (Algebra Q.algebra) :=
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TracialUltrapower, OAI.KadisonKastler.Algebra
def OAI.KadisonKastler.PublishedTracialUltrapower line 54
Source documentation
Popa §1.6, specialized to the constant sequence of the given II₁ factor with its already constructed faithful normal trace.
```
def PublishedTracialUltrapower : Prop :=
…
```
theorem OAI.KadisonKastler.TracialUltrapower.traceTwoNorm_sq_limit line 61
Source documentation
The trace formula commutes with the squared tracial norm.
```
theorem TracialUltrapower.traceTwoNorm_sq_limit {τ : FaithfulTracialState B}
    {ω : Ultrafilter ℕ} (Q : TracialUltrapower τ ω) (x : BoundedSequence B) :
    Tendsto (fun j => traceTwoNorm τ (x j) ^ 2) (ω : Filter ℕ)
      (𝓝 (traceTwoNorm Q.trace (Q.quotient x) ^ 2)) := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TracialUltrapower, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.traceTwoNorm
theorem OAI.KadisonKastler.TracialUltrapower.isTraceQuotient line 71
Source documentation
Faithfulness identifies the clipping kernel with the two-null sequences. This is proved from the published trace formula.
```
theorem TracialUltrapower.isTraceQuotient {τ : FaithfulTracialState B}
    {ω : Ultrafilter ℕ} (Q : TracialUltrapower τ ω) :
    IsTraceQuotient τ (ω : Filter ℕ) Q.quotient := by
…
```
Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.TracialUltrapower, OAI.KadisonKastler.IsTraceQuotient