TracialCommutantTrace.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The vacuum trace on the left commutant, obtained directly from tracial conjugation and the dense algebra vectors.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.conjugation_involutive line 17
theorem OAI.KadisonSimilarity.TracialCornerGeometry.inner_conjugation_swap line 20
theorem OAI.KadisonSimilarity.TracialCornerGeometry.commutant_conjugation_vector line 29
Source documentation
A left-module endomorphism has its adjoint vacuum vector given by tracial conjugation.
```
theorem commutant_conjugation_vector (Z : H →L[ℂ] H)
    (hZ : ∀ a, Z.comp (G.left a) = (G.left a).comp Z) :
    G.conjugation (Z (G.vector 1)) = star Z (G.vector 1) := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.commutant_vector_trace line 45
def OAI.KadisonSimilarity.TracialCornerGeometry.leftCommutant line 61
theorem OAI.KadisonSimilarity.TracialCornerGeometry.mem_leftCommutant_iff line 63
theorem OAI.KadisonSimilarity.TracialCornerGeometry.leftCommutant_commutes line 74
def OAI.KadisonSimilarity.TracialCornerGeometry.commutantTracialRepresentation line 79
Source documentation
The left commutant carries the faithful normal vacuum trace.
```
def commutantTracialRepresentation (h1 : G.trace 1 = 1) :
    TracialRepresentation G.leftCommutant where
…
```