OAI/Analysis/OInfinity/CentralBuffer.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A third canonical row in the norm ultrapower

The representatives are the explicit approximately central canonical rows, with tolerance 1/(n+1) and the first n+1 source generators tested. Their norms are uniformly one; both Gram and commutation relations hold exactly in the quotient. No commuting-buffer existence is assumed.

  1. lemma OAI.WeakPureInfiniteness.exists_normUltrapower_central_cuntz_row line 24

    Source documentation

    A concrete third row centralizing the two constant canonical families.

    lemma exists_normUltrapower_central_cuntz_row
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (s t : ℕ → E)
    (hs : ∀ i j, star (s i) * s j = if i = j then 1 else 0)
    (hc : bergRowsCommute s t) :
    ∃ R : ℕ → NormUltra.QuotientAlgebra (fun _ : ℕ => E) U,
      (∀ j k, star (R j) * R k = if j = k then 1 else 0) ∧
      (∀ j i, Commute (R j) (NormUltra.QuotientAlgebra.diagonalHom U (s i)) ∧
        Commute (R j) (star (NormUltra.QuotientAlgebra.diagonalHom U (s i)))) ∧
      ∀ j i, Commute (R j) (NormUltra.QuotientAlgebra.diagonalHom U (t i)) ∧
        Commute (R j) (star (NormUltra.QuotientAlgebra.diagonalHom U (t i))) := by
…

    Mentions: OAI.WeakPureInfiniteness.bergRowsCommute, OAI.NormUltra.QuotientAlgebra, OAI.NormUltra.QuotientAlgebra.diagonalHom