ProperlyInfiniteIsometries.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Two isometries in an algebra without finite central summands

Comparison embeds the finite complement of a maximal properly infinite projection into that projection. Its two orthogonal copies then absorb the complement and give isometries with initial projection one.

lemma OAI.BoundedHochschild.KadisonRingrose.finite_complement_embeds_properlyInfinite line 25
theorem OAI.BoundedHochschild.KadisonRingrose.properlyInfinite_one line 53
Source documentation
The unit is properly infinite when no nonzero central corner is finite.
```
theorem properlyInfinite_one (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hno : NoFiniteCentralSummand M) : ProperlyInfiniteProjection (1 : M) := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand, OAI.BoundedHochschild.KadisonRingrose.ProperlyInfiniteProjection
theorem OAI.BoundedHochschild.KadisonRingrose.exists_two_orthogonal_isometries line 82
Source documentation
Actual orthogonal isometries, with no trace, separability, or factor assumption.
```
theorem exists_two_orthogonal_isometries (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hno : NoFiniteCentralSummand M) :
    ∃ v w : M, star v * v = 1 ∧ star w * w = 1 ∧ star v * w = 0 := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.NoFiniteCentralSummand