ReducingCommutantCorner.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The commutant on a reducing subspace is the represented corner

theorem OAI.KadisonKastler.invariant_of_commutes_starProjection line 20
Source documentation
An operator commuting with the subspace projection preserves the subspace.
```
theorem invariant_of_commutes_starProjection (T : H →L[ℂ] H)
    (hT : E.starProjection * T = T * E.starProjection) :
    ∀ x ∈ E, T x ∈ E := by
…
```
theorem OAI.KadisonKastler.cornerExtension_mul_reducing line 31
theorem OAI.KadisonKastler.reducing_mul_cornerExtension line 43
theorem OAI.KadisonKastler.commutes_corner_iff line 55
def OAI.KadisonKastler.commutantReducingHom line 69
Source documentation
Restrict the original algebra to a subspace reduced by it.
```
def commutantReducingHom (M : VonNeumannAlgebra H)
    (hE : E.starProjection ∈ M.commutant) :
    Algebra M →⋆ₐ[ℂ] (E →L[ℂ] E) :=
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.commutantReducingHom_apply line 76
theorem OAI.KadisonKastler.commutant_reducingClosure line 82
Source documentation
The full commutant of the restricted algebra is exactly the corner of the original commutant, with extension by zero identifying operators.
```
theorem commutant_reducingClosure (M : VonNeumannAlgebra H)
    (hE : E.starProjection ∈ M.commutant) :
    (generatedVonNeumannAlgebra (commutantReducingHom E M hE).range).commutant =
      representedCorner E M.commutant hE := by
…
```
Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.commutantReducingHom, OAI.KadisonKastler.representedCorner

theorem OAI.KadisonKastler.commutantReducingHom_injective line 113

Source documentation

Full central support of the reducing projection makes restriction faithful.

theorem commutantReducingHom_injective (M : VonNeumannAlgebra H)
    (hE : E.starProjection ∈ M.commutant) (hE0 : E.starProjection ≠ 0)
    (hN : ScalarCenter M.commutant) :
    Function.Injective (commutantReducingHom E M hE) := by
…

Mentions: OAI.KadisonKastler.ScalarCenter, OAI.KadisonKastler.commutantReducingHom

theorem OAI.KadisonKastler.commutantReducingHom_boundedWeakNormal line 143
Source documentation
Restriction preserves bounded weak-operator limits coefficientwise.
```
theorem commutantReducingHom_boundedWeakNormal (M : VonNeumannAlgebra H)
    (hE : E.starProjection ∈ M.commutant) :
    BoundedWeakNormal M (commutantReducingHom E M hE) := by
…
```
Mentions: OAI.KadisonKastler.BoundedWeakNormal, OAI.KadisonKastler.commutantReducingHom