ProjectionModuleMaps.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Norm spectral approximation reduces right modularity to projection tests.

theorem OAI.KadisonKastler.selfAdjoint_mem_closed_algebra_projection_span line 23
theorem OAI.KadisonKastler.algebra_closed_projection_span_eq_top line 37
theorem OAI.KadisonKastler.right_module_of_projection_tests line 48
Source documentation
A bounded map is right modular as soon as it is fixed by each projection pinching. No continuity in the weak topology is required.
```
theorem right_module_of_projection_tests (M : VonNeumannAlgebra H)
    (F : Algebra M →L[ℂ] Algebra M)
    (hF : ∀ p : Algebra M, IsStarProjection p → ∀ x, F (x * p) = F x * p) :
    ∀ x y, F (x * y) = F x * y := by
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.right_module_iff_projectionAverage_fixed line 77

theorem OAI.KadisonKastler.right_module_eq_left_multiplication line 89

Source documentation

The value at the identity determines a right module map.

theorem right_module_eq_left_multiplication {A : Type*} [CStarAlgebra A]
    (F : A →ₗ[ℂ] A) (hF : ∀ x y, F (x * y) = F x * y) (x : A) :
    F x = F 1 * x := by simpa only [one_mul] using hF 1 x
…