FreeFactorCenter.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

An actual orthogonal unitary sequence and a dense matrix tower in one free factor force the center of the generated tracial algebra to be scalar.

theorem OAI.KadisonSimilarity.TracialCornerGeometry.central_trace_pair_word line 19

Source documentation

Centering the last endpoint and cyclically moving the last other-factor letter reduce every word to the centered terminal case.

theorem central_trace_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)
    (hD : ∀ d ∈ D, G.trace (c * d) = 0)
    {xs : List P} (hxs : CenteredPairWord G.trace A D xs)
    {d b : P} (hd : d ∈ D) (hb : b ∈ A) :
    G.trace (c * (d * xs.prod * b)) = 0 := by
…

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

theorem OAI.KadisonSimilarity.TracialCornerGeometry.scalar_center_of_free_matrix_factor line 63

Source documentation

The generated free algebra has scalar center, proved using finite trace pairings and Hilbert-space density.

theorem scalar_center_of_free_matrix_factor
    (h1 : G.trace 1 = 1) (hf : Function.Injective G.vector)
    (hfree : ScalarFree G.trace A D) (hgen : ReducedWordGenerated G 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, (∀ a : P, a * c = c * a) → ∃ z : ℂ, c = z • (1 : P) := by
…

Mentions: OAI.KadisonSimilarity.ScalarFree, OAI.KadisonSimilarity.ReducedWordGenerated