OriginalMatrixInjectivity.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Injectivity of matrix closures in the original finite-factor representation

The scalar trace is extended to the ambient operators and its GNS space supplies a contractive extension of the trace representation. Finite matrix retractions are transported through this extension. The finite-vector trace formula proves convergence on the original representation.

theorem OAI.KadisonKastler.isInjective_matrix_closure_of_trace_extension line 29

Source documentation

A trace-representation extension suffices for the original matrix closure.

theorem isInjective_matrix_closure_of_trace_extension
    (σ : FaithfulTracialState (Algebra M)) (hσ : FiniteVectorTrace σ)
    (τ : TracialRepresentation N) (e : Algebra M ≃⋆ₐ[ℂ] Algebra N)
    (he : ∀ a : Algebra M, τ.norm₂ (e a) = traceTwoNorm σ a)
    (R : (H →L[ℂ] H) →ₗ[ℂ] (K →L[ℂ] K))
    (hR : ∀ T, ‖R T‖ ≤ ‖T‖) (hRa : ∀ a : Algebra M, R a.val = (e a).val)
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra)) :
    IsInjective (FiniteMatrixStage.generatedVonNeumann A) := by
…

Mentions: OAI.KadisonKastler.FaithfulTracialState, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteVectorTrace, OAI.KadisonKastler.traceTwoNorm, OAI.KadisonKastler.IsInjective

theorem OAI.KadisonKastler.isInjective_original_matrix_closure line 103
Source documentation
The original representation of any increasing matrix closure in a finite factor is injective.
```
theorem isInjective_original_matrix_closure
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra)) :
    IsInjective (FiniteMatrixStage.generatedVonNeumann A) := by
…
```
Mentions: OAI.KadisonKastler.IsInjective

theorem OAI.KadisonKastler.exists_original_irreducible_injective_subalgebra_proved line 126

Source documentation

The finite-factor proof needs no published increasing-matrix injectivity premise.

theorem exists_original_irreducible_injective_subalgebra_proved
    [TopologicalSpace.SeparableSpace H] :
    ∃ (Q : VonNeumannAlgebra H) (hQM : Q ≤ M), IsInjective Q ∧
      (∀ b : Algebra M,
        (∀ q : Algebra Q, coordinateInclusion hQM q * b = b * coordinateInclusion hQM q) →
        ∃ c : ℂ, b = c • (1 : Algebra M)) := by
…

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