OriginalIrreducibleSubfactor.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Pulling the increasing matrix construction to the original representation

The original representation need not possess a tracial vector. We construct the matrix stages on the canonical separable trace Hilbert space, pull each finite stage back algebraically, and take its actual original weak closure. Commutation with that closure implies commutation with every pulled-back stage and hence with the irreducible algebra in the trace representation. Injectivity of the closure of the increasing matrix algebras is a hypothesis.

theorem OAI.KadisonKastler.mapped_matrixUnits_hom line 29
theorem OAI.KadisonKastler.mem_inverse_mapped_matrixUnits line 34

theorem OAI.KadisonKastler.commutes_generated_of_commutes_stages line 62

Source documentation

Membership in the commutant of every increasing stage gives commutation with the actual generated von Neumann algebra.

theorem commutes_generated_of_commutes_stages (A : ℕ → FiniteMatrixStage N)
    (hA : Monotone (fun j => (A j).units.concreteAlgebra)) (c : K →L[ℂ] K)
    (hc : ∀ j x, x ∈ (A j).units.concreteAlgebra → x * c = c * x)
    (x : Algebra (FiniteMatrixStage.generatedVonNeumann A)) :
    (x : K →L[ℂ] K) * c = c * (x : K →L[ℂ] K) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_original_irreducible_matrix_algebra line 90

Source documentation

An irreducible, increasing matrix-generated subalgebra in the original representation. No tracial vector in that representation is assumed.

theorem exists_original_irreducible_matrix_algebra
    (hM : IsII1Factor M.toStarSubalgebra) :
    ∃ A : ℕ → FiniteMatrixStage M,
      Monotone (fun j => (A j).units.concreteAlgebra) ∧
      (∀ j, FiniteDimensional ℂ (A j).units.concreteAlgebra) ∧
      (∀ b : Algebra M,
        (∀ r : Algebra (FiniteMatrixStage.generatedVonNeumann A),
          coordinateInclusion (FiniteMatrixStage.generatedVonNeumann_le A) r * b =
            b * coordinateInclusion (FiniteMatrixStage.generatedVonNeumann_le A) r) →
        ∃ c : ℂ, b = c • (1 : Algebra M)) := by
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_original_irreducible_injective_subalgebra line 155
Source documentation
The injective common subalgebra needed in the finite-factor perturbation proof exists in the original Hilbert representation.
```
theorem exists_original_irreducible_injective_subalgebra
    (hpub : PublishedIncreasingMatrixInjectivity (H := H))
…
```
Mentions: OAI.KadisonKastler.PublishedIncreasingMatrixInjectivity