ConcreteIrreducibleSubfactor.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Irreducible increasing matrix subfactors in the normal tracial GNS representation. The matrix refinement theorem is applied after deriving separability of that representation from the given predual.

theorem OAI.KadisonSimilarity.scalar_center_of_starEquiv line 17
theorem OAI.KadisonSimilarity.diffuse_projections_of_starEquiv line 35

theorem OAI.KadisonSimilarity.exists_gns_irreducible_matrix_subfactor line 63

Source documentation

The irreducible hyperfinite presentation is constructed in the faithful normal GNS representation of a diffuse finite factor.

theorem exists_gns_irreducible_matrix_subfactor
    (h1 : τ 1 = 1) (htr : ∀ a b, τ (a * b) = τ (b * a))
    (hf : ∀ a, τ (star a * a) = 0 → a = 0)
    (hnormal : BoundedHochschild.TraceInPredual e τ)
    (hfactor : ∀ c : A, (∀ a, a * c = c * a) → ∃ z : ℂ, c = z • (1 : A))
    (hdiff : ∀ p : A, IsStarProjection p → p ≠ 0 →
      ∃ q : A, IsStarProjection q ∧ q ≠ 0 ∧ q ≠ p ∧ p * q = q ∧ q * p = q) :
    let N := representationVonNeumannAlgebra τ.gnsStarAlgHom
…

Mentions: OAI.BoundedHochschild.TraceInPredual, OAI.KadisonSimilarity.representationVonNeumannAlgebra