ProperlyInfiniteMatrixSystems.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Finite self-similar matrix systems in a properly infinite algebra

Every positive finite matrix size occurs unitally, and its commutant is isomorphic to the original algebra. These are concrete matrix systems for the properly infinite amplification argument.

theorem OAI.BoundedHochschild.KadisonRingrose.exists_self_commutant_matrixSystem line 27
Source documentation
Unital matrix systems of arbitrary finite size, with their actual commutants identified with the given algebra.
```
theorem exists_self_commutant_matrixSystem (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hno : NoFiniteCentralSummand M) (n : ℕ) [NeZero n] :
    ∃ E : MatrixSystem M n, Nonempty (M ≃⋆ₐ[ℂ] E.commutant) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand