TomiyamaProjection.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

A unital contractive retraction onto a C-star subalgebra respects left and right multiplication by projections in that subalgebra.

theorem OAI.KadisonKastler.tomiyama_map_one line 28
theorem OAI.KadisonKastler.tomiyama_mono line 33
theorem OAI.KadisonKastler.tomiyama_corner_supported line 39
Source documentation
Positivity ensures that the image of a diagonal corner stays in that corner.
```
theorem tomiyama_corner_supported (e : B) (he : IsStarProjection e) (x : A) :
    e * P (φ e * x * φ e) * e = P (φ e * x * φ e) := by
…
```
theorem OAI.KadisonKastler.tomiyama_compressed_zero_of_bounds line 66
theorem OAI.KadisonKastler.tomiyama_compressed_zero_of_mul_right_zero line 91
Source documentation
A source block orthogonal on the right has zero diagonal image.
```
theorem tomiyama_compressed_zero_of_mul_right_zero (e : B) (he : IsStarProjection e)
    (z : A) (hz : z * φ e = 0) : e * P z * e = 0 := by
…
```
theorem OAI.KadisonKastler.tomiyama_compressed_zero_of_mul_left_zero line 101
Source documentation
The analogous statement for a source block orthogonal on the left.
```
theorem tomiyama_compressed_zero_of_mul_left_zero (e : B) (he : IsStarProjection e)
    (z : A) (hz : φ e * z = 0) : e * P z * e = 0 := by
…
```