OAI/Analysis/KadisonSimilarity/Representation/NormalFactorGeneration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Tracial generation by two factors implies generation of the concrete von Neumann range by their norm-closed algebra.

  1. theorem OAI.KadisonSimilarity.TracialCornerGeometry.normal_range_eq_generated line 22
  2. theorem OAI.KadisonSimilarity.TracialCornerGeometry.map_generated_mem line 60
  3. theorem OAI.KadisonSimilarity.TracialCornerGeometry.normal_range_map_mem line 81

    Source documentation

    It suffices to check the two factors when conjugating the entire normal range.

    theorem normal_range_map_mem (h1 : G.trace 1 = 1)
    (hf : Function.Injective G.vector) (M : VonNeumannAlgebra H)
    (hrange : G.left.range = M.toStarSubalgebra)
    (hgen : G.FactorsTraciallyGenerate A D)
    (θ : (H →L[ℂ] H) ≃⋆ₐ[ℂ] (H →L[ℂ] H))
    (hA : ∀ a : A, θ (G.left (a : P)) ∈ M)
    (hD : ∀ d : D, θ (G.left (d : P)) ∈ M) (x : P) :
    θ (G.left x) ∈ M := by
…