InfiniteMatrixColumns.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A unital countable system of equivalent orthogonal projections

Two orthogonal isometries give a countable shift. Its residual projection is absorbed into the first column, so the finite diagonal sums converge weak-star to the unit, without a countability assumption on the predual.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_countable_isometries_of_two line 29

Source documentation

The concrete countable column system needed in the properly infinite cohomology argument. All columns are isometries and their ranges sum to one.

theorem exists_countable_isometries_of_two (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {v w : M} (hv : star v * v = 1) (hw : star w * w = 1) (hvw : star v * w = 0) :
    ∃ c : ℕ → PartialIso M, (∀ i, (c i).initial = 1) ∧
      (∀ i j, i ≠ j → (c i).final * (c j).final = 0) ∧
      PredualTendsto e (fun s : Finset ℕ => ∑ i ∈ s, (c i).final) atTop 1 := by
…

Mentions: OAI.BoundedHochschild.PredualTendsto

theorem OAI.BoundedHochschild.KadisonRingrose.exists_countable_isometries line 125

Source documentation

Every algebra with no finite central summand has a unital countable matrix column system.

theorem exists_countable_isometries (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hno : NoFiniteCentralSummand M) :
    ∃ c : ℕ → PartialIso M, (∀ i, (c i).initial = 1) ∧
      (∀ i j, i ≠ j → (c i).final * (c j).final = 0) ∧
      PredualTendsto e (fun s : Finset ℕ => ∑ i ∈ s, (c i).final) atTop 1 := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand, OAI.BoundedHochschild.PredualTendsto