OAI/Analysis/KadisonKastler/CentralVectorMatrixLimit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Central vectors of an increasing matrix sequence

The decreasing central-vector projections have an actual strong limit. When their common range is a separating line, the state and commutant identities supply the exact expected-subfactor model.

  1. def OAI.KadisonKastler.matrixCentralVectorSpace line 24
  2. theorem OAI.KadisonKastler.matrixCentralVectorSpace_isClosed line 27
  3. instance OAI.KadisonKastler.matrixCentralVectorSpace_complete line 33
  4. theorem OAI.KadisonKastler.matrixCentralVectorSpace_le line 38
  5. theorem OAI.KadisonKastler.matrixCentralVectorSpace_tendsto line 43
  6. theorem OAI.KadisonKastler.matrixCentralVectorSpace_centralizes line 60
  7. theorem OAI.KadisonKastler.matrixClosure_irreducible_of_centralVectorSpace line 74

    Source documentation

    The rank-one central-vector conclusion gives irreducibility.

    theorem matrixClosure_irreducible_of_centralVectorSpace
    (A : ℕ → FiniteMatrixStage M) (J : H ≃ₗᵢ⋆[ℂ] H)
    (hright : ∀ a : Algebra M, conjugationOperator J a.val ∈ M.commutant)
    (ξ : H) (hξ : ξ ∈ matrixCentralVectorSpace A J)
    (hline : matrixCentralVectorSpace A J ≤ Submodule.span ℂ {ξ})
    (hsep : Function.Injective (algebraVectorMap M ξ)) :
    ∀ T ∈ M,
      (∀ r ∈ FiniteMatrixStage.generatedVonNeumann A, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H) := by
…

    Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.matrixCentralVectorSpace, OAI.KadisonKastler.algebraVectorMap

  8. theorem OAI.KadisonKastler.expectedMatrixSubfactorModel_of_central_line line 102

    Source documentation

    A separating central line yields the expectation data.

    theorem expectedMatrixSubfactorModel_of_central_line [Nontrivial H]
    (A : ℕ → FiniteMatrixStage M)
    (hA : Monotone (fun n => (A n).units.concreteAlgebra))
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (hright : ∀ a : Algebra M, conjugationOperator J a.val ∈ M.commutant)
    (ξ : H) (hunit : ‖ξ‖ = 1)
    (hcyc : DenseRange (algebraVectorMap M ξ))
    (hsep : Function.Injective (algebraVectorMap M ξ))
    (hξ : ξ ∈ matrixCentralVectorSpace A J)
    (hline : matrixCentralVectorSpace A J ≤ Submodule.span ℂ {ξ}) :
    Nonempty (ExpectedMatrixSubfactorModel M) :=
…

    Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.matrixCentralVectorSpace, OAI.KadisonKastler.ExpectedMatrixSubfactorModel