FiniteProjectionEquivalence.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Unitary equivalence of finite projections

In a finite von Neumann algebra a partial isometry extends to a unitary. The proof uses trace-free central comparison of the complementary projections and finiteness of central corners. No scalar trace is used.

def OAI.BoundedHochschild.KadisonRingrose.adjointPartialIso line 25
lemma OAI.BoundedHochschild.KadisonRingrose.adjointPartialIso_initial line 30
lemma OAI.BoundedHochschild.KadisonRingrose.adjointPartialIso_final line 34

def OAI.BoundedHochschild.KadisonRingrose.centralCutPartialIso line 38

Source documentation

Restrict a partial isometry to a central summand.

def centralCutPartialIso (z : M) (hz : IsStarProjection z)
    (hc : ∀ a : M, z * a = a * z) (v : PartialIso M) : PartialIso M where
…

lemma OAI.BoundedHochschild.KadisonRingrose.centralCutPartialIso_initial line 48
lemma OAI.BoundedHochschild.KadisonRingrose.centralCutPartialIso_final line 56
lemma OAI.BoundedHochschild.KadisonRingrose.finite_central_initial_iff_final line 66
Source documentation
A central cut of a partial isometry exhausts its initial projection exactly when it exhausts its final projection in a finite algebra.
```
lemma finite_central_initial_iff_final (hfinite : FiniteAlgebra M)
    (z : M) (hz : IsStarProjection z) (hc : ∀ a : M, z * a = a * z)
    (v : PartialIso M) : z * v.initial = z ↔ z * v.final = z := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra
theorem OAI.BoundedHochschild.KadisonRingrose.finite_partialIso_extends_unitary line 87
Source documentation
A partial isometry in a finite von Neumann algebra extends to a unitary.
```
theorem finite_partialIso_extends_unitary (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (v : PartialIso M) :
    ∃ u : unitary M, (u : M) * v.initial = v := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra
theorem OAI.BoundedHochschild.KadisonRingrose.finite_equivalent_unitarily_conjugate line 136
Source documentation
Equivalent projections in a finite von Neumann algebra are unitarily conjugate.
```
theorem finite_equivalent_unitarily_conjugate (e : StrongDual ℂ X ≃ₗᵢ⋆[ℂ] M)
    (hfinite : FiniteAlgebra M) (v : PartialIso M) :
    ∃ u : unitary M, (u : M) * v.initial * star (u : M) = v.final := by
…
```
Mentions: OAI.BoundedHochschild.KadisonRingrose.FiniteAlgebra