FreeConjugateWords.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Orthogonal conjugates of reduced words. These are the finite-word calculations used to identify the center of the generated free algebra.

theorem OAI.KadisonSimilarity.CenteredPairWord.append_pair line 15

theorem OAI.KadisonSimilarity.CenteredPairWord.nil_or_snoc line 24

Source documentation

A nonempty pair word has a last centered pair.

theorem CenteredPairWord.nil_or_snoc {xs : List R}
    (hxs : CenteredPairWord τ A D xs) :
    xs = [] ∨ ∃ ys a d, CenteredPairWord τ A D ys ∧ a ∈ A ∧ d ∈ D ∧
      τ a = 0 ∧ τ d = 0 ∧ xs = ys ++ [a, d] := by
…

Mentions: OAI.KadisonSimilarity.CenteredPairWord

theorem OAI.KadisonSimilarity.centeredWordPairing_append_pair line 39

theorem OAI.KadisonSimilarity.ScalarFree.trace_conjugate_words_zero line 50

Source documentation

Conjugating a reduced word by orthogonal centered unitaries gives orthogonal words, even when its first other-factor endpoint is unrestricted.

theorem ScalarFree.trace_conjugate_words_zero (hf : ScalarFree τ A D)
    (hstar : ∀ x, τ (star x) = star (τ x)) (h1 : τ 1 = 1)
    {xs : List R} (hxs : CenteredPairWord τ A D xs)
    {b d u v : R} (hb : b ∈ A) (hb0 : τ b = 0) (hd : d ∈ D)
    (hu : u ∈ D) (hv : v ∈ D) (hu0 : τ u = 0) (hv0 : τ v = 0)
    (huv : τ (u * star v) = 0) :
    τ (star (u * d * xs.prod * b * star u) *
      (v * d * xs.prod * b * star v)) = 0 := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.CenteredPairWord

theorem OAI.KadisonSimilarity.trace_central_conjugate line 69

Source documentation

A central trace pairing is unchanged by unitary conjugation.

theorem trace_central_conjugate
    (htr : ∀ a b, τ (a * b) = τ (b * a))
    (c w : R) (u : unitary R) (hc : star c * (u : R) = (u : R) * star c) :
    τ (star c * ((u : R) * w * star (u : R))) = τ (star c * w) := by
…

theorem OAI.KadisonSimilarity.trace_unitary_conjugate line 82

Source documentation

Cyclicity alone makes a trace invariant under unitary conjugation.

theorem trace_unitary_conjugate
    (htr : ∀ a b, τ (a * b) = τ (b * a)) (w : R) (u : unitary R) :
    τ ((u : R) * w * star (u : R)) = τ w := by
…