OAI/Analysis/KadisonSimilarity/FreeProduct/FreeCentralWords.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Central pairings vanish on free words with a centered terminal letter. The proof uses an actual infinite family of orthogonal unitary conjugates.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.central_trace_centered_pair_word line 20

    Source documentation

    The conjugates of a reduced word force its pairing with every central element to vanish. Only the terminal A letter is required to be centered.

    theorem central_trace_centered_pair_word
    (h1 : G.trace 1 = 1) (hfree : ScalarFree G.trace A D)
    (u : ℕ → unitary P) (hu : ∀ n, (u n : P) ∈ D)
    (hu0 : ∀ n, G.trace (u n : P) = 0)
    (huv : ∀ i j, G.trace ((u i : P) * star (u j : P)) = if i = j then 1 else 0)
    (c : P) (hc : ∀ a : P, a * c = c * a)
    {xs : List P} (hxs : CenteredPairWord G.trace A D xs)
    {d b : P} (hd : d ∈ D) (hb : b ∈ A) (hb0 : G.trace b = 0) :
    G.trace (c * (d * xs.prod * b)) = 0 := by
…

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