TraceConjugationAction.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The trace conjugation representation of the countable group

def OAI.KadisonKastler.concreteTraceConjugationUnitary line 15
Source documentation
Conjugation by a unitary, acting on the canonical trace Hilbert space.
```
def concreteTraceConjugationUnitary
    (hM : Generator.IsII1Factor M.toStarSubalgebra) (u : unitary (Algebra M)) :
    unitary (ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM) :=
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert
theorem OAI.KadisonKastler.concreteTraceConjugationUnitary_embedding line 20
def OAI.KadisonKastler.concreteTraceConjugationAction line 32
Source documentation
The multiplication law follows on the dense bounded algebra vectors.
```
def concreteTraceConjugationAction
    (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    unitary (Algebra M) →*
      unitary (ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM) where
…
```
Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert

theorem OAI.KadisonKastler.exists_countable_trace_conjugation_representation line 70

Source documentation

A countable trace-dense group gives an actual unitary representation whose fixed vectors are precisely the scalar trace vectors.

theorem exists_countable_trace_conjugation_representation
    (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    ∃ G : Subgroup (unitary (Algebra M)),
      (G : Set (unitary (Algebra M))).Countable ∧
      ∃ σ : G →* unitary (ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM),
        (∀ g, σ g = concreteTraceConjugationUnitary hM g.val) ∧
        (∀ v : ConcreteTraceHilbert hM,
          (∀ g, (σ g : ConcreteTraceHilbert hM →L[ℂ] ConcreteTraceHilbert hM) v = v) →
          ∃ z : ℂ, v = z • concreteTraceEmbedding hM 1) := by
…

Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.ConcreteTraceHilbert, OAI.KadisonKastler.concreteTraceConjugationUnitary, OAI.KadisonKastler.concreteTraceEmbedding