TracialProjectionConjugacy.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Equal-trace projection conjugacy in a concrete finite factor

theorem OAI.KadisonKastler.tracial_isometry_coisometry line 19
Source documentation
Faithfulness of a represented trace makes every isometry unitary.
```
theorem tracial_isometry_coisometry (τ : TracialRepresentation M)
    (a : Algebra M) (ha : star a * a = 1) : a * star a = 1 := by
…
```
Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_tracial_projection_conjugacy line 32

Source documentation

Equal trace projections are conjugate by an actual unitary of the factor.

theorem exists_tracial_projection_conjugacy (τ : TracialRepresentation M)
    (hfactor : ∀ c : Algebra M, (∀ a : Algebra M, a * c = c * a) →
      ∃ z : ℂ, c = z • (1 : Algebra M))
    (p q : AlgebraProjection M) (ht : τ.trace p.val = τ.trace q.val) :
    ∃ u : unitary (Algebra M), (u : Algebra M) * p.val * star (u : Algebra M) = q.val := by
…

Mentions: OAI.KadisonKastler.Algebra