RowCompletionBuffer.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Completions in the first buffer commutant

The relative path data records the fixed complement at every time. The second buffer is constructed by the explicit central-row theorem inside the norm ultrapower; its target family consists of elements of the first buffer commutant. No commuting-row existence is assumed.

structure OAI.WeakPureInfiniteness.RelativeBinaryCompletion line 25

lemma OAI.WeakPureInfiniteness.exists_relative_connected_binary_completion line 40

Source documentation

A relative completion whose whole connecting path fixes the external complement, obtained by doing the three connected moves in the corner.

lemma exists_relative_connected_binary_completion {n : ℕ}
    (q : E) (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (x : Fin (n + 2) → E)
    (hxs : ∀ i, q * x i = x i ∧ x i * q = x i)
    (hx : ∀ i j, star (x i) * x j = if i = j then q else 0)
    (b : Fin 2 → E)
    (hb : ∀ i j, star (b i) * b j = if i = j then q else 0)
    (hbs : (∑ i, b i * star (b i)) = q)
    (r : Fin 3 → E)
    (hrs : ∀ i, q * r i = r i ∧ r i * q = r i)
    (hr : ∀ i j, star (r i) * r j = if i = j then q else 0)
    (her : Commute (star (r 0)) (x (Fin.last (n + 1))))
…

def OAI.WeakPureInfiniteness.rowCentralizerDiagonalHom line 119

Source documentation

Diagonalizing an element of the first row commutant preserves that membership in the next norm ultrapower.

def rowCentralizerDiagonalHom (U : Ultrafilter ℕ) (R : ℕ → E) :
    StarSubalgebra.centralizer ℂ (Set.range R) →⋆ₐ[ℂ]
      StarSubalgebra.centralizer ℂ
        (Set.range (fun i => NormUltra.QuotientAlgebra.diagonalHom U (R i))) := by
…

Mentions: OAI.NormUltra.QuotientAlgebra.diagonalHom

lemma OAI.WeakPureInfiniteness.exists_normUltrapower_row_in_commutant line 141

Source documentation

The second proper row is actually built. Its entries remain in the first row's commutant and commute with every member of the chosen target family and its adjoint.

lemma exists_normUltrapower_row_in_commutant [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)] (R : ℕ → E)
    (hR : ∀ i j, star (R i) * R j = if i = j then 1 else 0)
    (t : ℕ → StarSubalgebra.centralizer ℂ (Set.range R)) :
    ∃ z : ℕ → StarSubalgebra.centralizer ℂ
        (Set.range (fun i => NormUltra.QuotientAlgebra.diagonalHom U (R i))),
      (∀ i j, star (z i) * z j = if i = j then 1 else 0) ∧
      ∀ i j, Commute (z i) (rowCentralizerDiagonalHom U R (t j)) ∧
        Commute (z i) (star (rowCentralizerDiagonalHom U R (t j))) := by
…

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

lemma OAI.WeakPureInfiniteness.rowCentralizerDiagonal_norm line 179

lemma OAI.WeakPureInfiniteness.exists_buffer_preserving_pair_completions line 190

Source documentation

The same reference completion is available for both proper finite rows after the second, explicitly constructed buffer. All resulting data belong to the first buffer commutant.

lemma exists_buffer_preserving_pair_completions [Nontrivial E]
    (U : Ultrafilter ℕ) [Fact ((U : Filter ℕ) ≤ atTop)]
    (R : ℕ → E) (hR : ∀ i j, star (R i) * R j = if i = j then 1 else 0)
    (q : StarSubalgebra.centralizer ℂ (Set.range R))
    (hq : star q = q) (hqq : q * q = q) (hq0 : q ≠ 0)
    (n : ℕ) (x y : Fin (n + 2) → StarSubalgebra.centralizer ℂ (Set.range R))
    (hxs : ∀ i, q * x i = x i ∧ x i * q = x i)
    (hys : ∀ i, q * y i = y i ∧ y i * q = y i)
    (hx : ∀ i j, star (x i) * x j = if i = j then q else 0)
    (hy : ∀ i j, star (y i) * y j = if i = j then q else 0)
    (b : Fin 2 → StarSubalgebra.centralizer ℂ (Set.range R))
    (hb : ∀ i j, star (b i) * b j = if i = j then q else 0)
…