TracialMatrixInjectivity.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of a tracial increasing matrix closure

The finite-stage ambient retractions preserve the given trace. Their restrictions therefore converge in trace norm to the identity on the weak closure. A pointwise weak limit is the required ambient projection.

theorem OAI.KadisonKastler.matrixExpectations_tendsto line 25

Source documentation

Increasing matrix-stage expectations converge on their weak closure.

theorem matrixExpectations_tendsto (τ : TracialRepresentation N)
    (A : ℕ → FiniteMatrixStage N)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (x : Algebra N) (hx : x.val ∈ FiniteMatrixStage.generated A) :
    Tendsto (fun n => τ.norm₂
      (conditionalExpectation τ
        (matrixUnitConcreteAlgebra_le (A n).units) x - x))
      atTop (𝓝 0) := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixUnitConcreteAlgebra_le

def OAI.KadisonKastler.matrixTraceAmbientRetraction line 58

Source documentation

The finite matrix retraction, with codomain viewed in ambient operators.

def matrixTraceAmbientRetraction [Nontrivial H] (τ : TracialRepresentation N)
    {ι : Type*} [Fintype ι] [DecidableEq ι] [Nonempty ι]
    (E : MatrixUnitSystem ι (Algebra N)) (o : ι) :
    (H →L[ℂ] H) →L[ℂ] (H →L[ℂ] H) :=
…

Mentions: OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.isInjective_tracial_matrix_closure_of_nontrivial line 67

Source documentation

The weak closure of increasing full matrix algebras is injective in a faithful tracial representation.

theorem isInjective_tracial_matrix_closure_of_nontrivial [Nontrivial H]
    (τ : TracialRepresentation N) (A : ℕ → FiniteMatrixStage N)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra)) :
    IsInjective (FiniteMatrixStage.generatedVonNeumann A) := by
…

Mentions: OAI.KadisonKastler.IsInjective

theorem OAI.KadisonKastler.isInjective_tracial_matrix_closure line 99

Source documentation

A faithful unit trace vector itself supplies nontriviality of the Hilbert space.

theorem isInjective_tracial_matrix_closure
    (τ : TracialRepresentation N) (A : ℕ → FiniteMatrixStage N)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra)) :
    IsInjective (FiniteMatrixStage.generatedVonNeumann A) := by
…

Mentions: OAI.KadisonKastler.IsInjective

theorem OAI.KadisonKastler.exists_irreducible_injective_subfactor_tracial line 113

Source documentation

A separably represented II₁ factor has an irreducible injective tracial subfactor.

theorem exists_irreducible_injective_subfactor_tracial
    [TopologicalSpace.SeparableSpace H]
    (τ : TracialRepresentation M) (hM : IsII1Factor M.toStarSubalgebra) :
    ∃ (R : VonNeumannAlgebra H) (hRM : R ≤ M),
      IsII1Factor R.toStarSubalgebra ∧ IsInjective R ∧
      (∀ b : Algebra M,
        (∀ r : Algebra R, coordinateInclusion hRM r * b = b * coordinateInclusion hRM r) →
        ∃ c : ℂ, b = c • (1 : Algebra M)) := by
…

Mentions: OAI.KadisonKastler.IsInjective, OAI.KadisonKastler.Algebra