TracialAutomorphisms.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Hilbert-space implementation of trace-preserving automorphisms. The implementation and its covariance are constructed from dense algebra vectors.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.automorphism_vector_norm line 20
def OAI.KadisonSimilarity.TracialCornerGeometry.automorphismIsometry line 26
Source documentation
Extension of the automorphism on bounded algebra vectors.
```
def automorphismIsometry : H →ₗᵢ[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.automorphismIsometry_vector line 30
theorem OAI.KadisonSimilarity.TracialCornerGeometry.trace_symm_automorphism line 35
theorem OAI.KadisonSimilarity.TracialCornerGeometry.automorphismIsometry_surjective line 38
def OAI.KadisonSimilarity.TracialCornerGeometry.automorphismUnitary line 46
Source documentation
The actual unitary implementation of a trace-preserving automorphism.
```
def automorphismUnitary : H ≃ₗᵢ[ℂ] H :=
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.automorphismUnitary_vector line 50
theorem OAI.KadisonSimilarity.TracialCornerGeometry.automorphismUnitary_left line 55
Source documentation
Multiplication covariance extends from the algebra to the whole Hilbert space.
```
theorem automorphismUnitary_left (a : P) (x : H) :
    G.automorphismUnitary θ hθ (G.left a x) =
      G.left (θ a) (G.automorphismUnitary θ hθ x) := by
…
```
theorem OAI.KadisonSimilarity.TracialCornerGeometry.automorphismUnitary_fixes_base line 62

def OAI.KadisonSimilarity.TracialCornerGeometry.automorphismRepresentation line 71

Source documentation

A trace-preserving algebraic group action gives a unitary representation.

def automorphismRepresentation {Γ : Type*} [Group Γ]
    (α : Γ →* (P ≃⋆ₐ[ℂ] P)) (hα : ∀ g a, G.trace (α g a) = G.trace a) :
    Γ →* unitary (H →L[ℂ] H) where
…

theorem OAI.KadisonSimilarity.TracialCornerGeometry.automorphismRepresentation_vector line 96