OAI/Analysis/KadisonKastler/TracialUltrapowerConstruction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The constant II₁ tracial ultrapower

This constructs the bounded-product quotient, its faithful trace and its finite factor representation, as in Popa, JFA 266 (2014), §1.6.

  1. def OAI.KadisonKastler.constructedTracialUltrapower line 25
  2. theorem OAI.KadisonKastler.publishedTracialUltrapower line 44

    Source documentation

    The constant-sequence tracial ultrapower of Popa §1.6.

    theorem publishedTracialUltrapower : PublishedTracialUltrapower.{u} := by
…