NormalSupportTransport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Range supports are preserved by star isomorphisms between concrete von Neumann algebras. The proof uses their algebraic least-support property, so no continuity in the weak operator topology is assumed.

theorem OAI.KadisonSimilarity.rangeSupport_least_left line 17
Source documentation
Any left identity on an operator is a left identity on its range support.
```
theorem rangeSupport_least_left (B p : H →L[ℂ] H) (h : p * B = B) :
    p * rangeSupport B = rangeSupport B := by
…
```
Mentions: OAI.KadisonSimilarity.rangeSupport
def OAI.KadisonSimilarity.normalRangeSupport line 25
Source documentation
The range support viewed as an element of its original normal algebra.
```
def normalRangeSupport (M : VonNeumannAlgebra H) (a : M.toStarSubalgebra) :
    M.toStarSubalgebra := ⟨rangeSupport (a : H →L[ℂ] H), rangeSupport_mem M a a.property⟩
```
Mentions: OAI.KadisonSimilarity.rangeSupport, OAI.KadisonSimilarity.rangeSupport_mem
theorem OAI.KadisonSimilarity.normalRangeSupport_isStarProjection line 28
theorem OAI.KadisonSimilarity.normalRangeSupport_mul line 36
theorem OAI.KadisonSimilarity.normalRangeSupport_least line 41

theorem OAI.KadisonSimilarity.normalRangeSupport_map line 49

Source documentation

Isomorphisms preserve support projections by their leastness in the algebraic projection order.

theorem normalRangeSupport_map
    (M : VonNeumannAlgebra H) (N : VonNeumannAlgebra K)
    (e : M.toStarSubalgebra ≃⋆ₐ[ℂ] N.toStarSubalgebra) (a : M.toStarSubalgebra) :
    e (normalRangeSupport M a) = normalRangeSupport N (e a) := by
…

Mentions: OAI.KadisonSimilarity.normalRangeSupport