IrreducibleMatrixSubfactor.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The irreducible matrix-generated subfactor

In a separable tracial representation, the existing matrix refinement construction supplies the subfactor used in the finite stability argument. No extra published existence hypothesis is introduced.

theorem OAI.KadisonKastler.exists_irreducible_matrix_subfactor line 25

Source documentation

A concrete separable II₁ factor with its faithful vector trace contains an irreducible II₁ subfactor generated by an increasing sequence of full matrix algebras.

theorem exists_irreducible_matrix_subfactor
    (τ : UltrapowerBridge.TracialRepresentation M)
    (hM : IsII1Factor M.toStarSubalgebra) :
    ∃ (R : VonNeumannAlgebra H) (hRM : R ≤ M),
      IsII1Factor R.toStarSubalgebra ∧
      (∀ b : Algebra M,
        (∀ r : Algebra R, coordinateInclusion hRM r * b = b * coordinateInclusion hRM r) →
        ∃ c : ℂ, b = c • (1 : Algebra M)) ∧
      ∃ A : ℕ → FiniteMatrixStage M,
        R = FiniteMatrixStage.generatedVonNeumann A ∧
        Monotone (fun n => (A n).units.concreteAlgebra) ∧
        (∀ n, FiniteDimensional ℂ (A n).units.concreteAlgebra) := by
…

Mentions: OAI.UltrapowerBridge.TracialRepresentation, OAI.KadisonKastler.Algebra