IsometryAbsorption.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Absorbing a projection around an isometry

If a projection contains the range of an isometry, it is equivalent to the unit. The countable shift proof is the particular projection comparison needed for a unital infinite matrix system.

theorem OAI.BoundedHochschild.KadisonRingrose.isometry_onto_projection line 26
Source documentation
The projection form of the countable shift argument: an isometry whose range lies under p extends to an equivalence between one and p.
```
theorem isometry_onto_projection (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    {v p : M} (hv : star v * v = 1) (hp : IsStarProjection p) (hpv : p * v = v) :
    ∃ w : PartialIso M, w.initial = 1 ∧ w.final = p := by
…
```