CountableColumnRegrouping.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Finite unital matrix columns by regrouping a countable column system.

lemma OAI.BoundedHochschild.KadisonRingrose.projection_eq_one_of_column_bounds line 20

theorem OAI.BoundedHochschild.KadisonRingrose.finite_columns_of_countable line 32

Source documentation

Splitting countably many columns into n infinite classes gives n unital orthogonal isometries. The proof uses actual sums of transitions.

theorem finite_columns_of_countable (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (c : ℕ → PartialIso M) (hi : ∀ i, (c i).initial = 1)
    (ho : ∀ i j, i ≠ j → (c i).final * (c j).final = 0)
    (ht : PredualTendsto e (fun s : Finset ℕ => ∑ i ∈ s, (c i).final) atTop 1)
    (n : ℕ) [NeZero n] :
    ∃ v : Fin n → PartialIso M, (∀ j, (v j).initial = 1) ∧
      (∀ j k, j ≠ k → (v j).final * (v k).final = 0) ∧ ∑ j, (v j).final = 1 := by
…

Mentions: OAI.BoundedHochschild.PredualTendsto

theorem OAI.BoundedHochschild.KadisonRingrose.exists_properlyInfinite_matrix_columns line 97

Source documentation

Arbitrary finite unital column systems inside a properly infinite algebra.

theorem exists_properlyInfinite_matrix_columns (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hno : NoFiniteCentralSummand M) (n : ℕ) [NeZero n] :
    ∃ v : Fin n → PartialIso M, (∀ j, (v j).initial = 1) ∧
      (∀ j k, j ≠ k → (v j).final * (v k).final = 0) ∧ ∑ j, (v j).final = 1 := by
…

Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand