ConjugateMatrixStages.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Actual matrix stages in the conjugate right algebra

Conjugation changes the scalar coefficients by complex conjugation, while the conjugated matrix-unit entries retain their usual product laws. Thus the right algebra is generated by actual increasing full matrix stages. This lets the same finite averaging argument transfer its irreducibility to a nearby commutant.

theorem OAI.KadisonKastler.conjugationOperator_zero line 24
theorem OAI.KadisonKastler.conjugationOperator_sum line 30
Distinct definitions of this name: OAI/Analysis/KadisonKastler/RelativeMatrixCone.lean:122 (different declaration text). Qualify references as OAI.KadisonKastler.conjugationOperator_sum@path.

def OAI.KadisonKastler.conjugateMatrixUnits line 40

Source documentation

Actual full matrix units in the conjugate right algebra.

def conjugateMatrixUnits (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    {ι : Type*} [Fintype ι] [DecidableEq ι]
    (E : MatrixUnitSystem ι (H →L[ℂ] H)) : MatrixUnitSystem ι (H →L[ℂ] H) where
…

theorem OAI.KadisonKastler.conjugateMatrixUnits_entry line 52
theorem OAI.KadisonKastler.conjugateMatrixUnits_hom line 57
theorem OAI.KadisonKastler.conjugation_mem_conjugateMatrixUnits line 67
theorem OAI.KadisonKastler.conjugateMatrixUnits_mono line 74

theorem OAI.KadisonKastler.conjugateRightAlgebra_generated_matrixStages line 87

Source documentation

The weakly generated right algebra is exactly generated by the conjugated finite matrix stages.

theorem conjugateRightAlgebra_generated_matrixStages
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (d : ℕ → ℕ) (E : ∀ n, MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H)) :
    conjugateRightAlgebra J hJ (generatedVonNeumannAlgebra (⨆ n, (E n).algebra)) =
      generatedVonNeumannAlgebra (⨆ n, (conjugateMatrixUnits J hJ (E n)).algebra) := by
…

Mentions: OAI.KadisonKastler.conjugateRightAlgebra, OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.conjugateMatrixUnits

theorem OAI.KadisonKastler.preparedRight_cyclic_separating_of_matrix_gaps line 123

Source documentation

Small gaps on both sides transfer the two relative irreducibility statements. Together with the common left/right vector action this proves cyclicity and separation in the actual neighboring representation.

theorem preparedRight_cyclic_separating_of_matrix_gaps
    (M N R : VonNeumannAlgebra H)
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (hJM : conjugateRightAlgebra J hJ M = M.commutant)
    (d : ℕ → ℕ) (E : ∀ n, MatrixUnitSystem (Fin (d n)) (H →L[ℂ] H))
    (hmono : Monotone (fun n => (E n).algebra))
    (hR : R = generatedVonNeumannAlgebra (⨆ n, (E n).algebra))
    (hRM : R ≤ M) (hRN : R ≤ N)
    (hSN : conjugateRightAlgebra J hJ R ≤ N.commutant)
    (hirr : ∀ T ∈ M, (∀ r ∈ R, r * T = T * r) →
      ∃ z : ℂ, T = z • (1 : H →L[ℂ] H))
    (hgap : kkDistance M N < 1 / 2)
…

Mentions: OAI.KadisonKastler.conjugateRightAlgebra, OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.kkDistance