OAI/Analysis/KadisonKastler/TomitaAdjointCore.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The commutant core lies in the adjoint Tomita domain

The closed-graph coefficient identity identifies the adjoint on the dense commutant orbit. In particular the adjoint operator is densely defined.

  1. theorem OAI.KadisonKastler.tomitaAdjoint_coefficient line 18
  2. theorem OAI.KadisonKastler.tomitaAdjoint_commutant_mem line 31
  3. theorem OAI.KadisonKastler.tomitaAdjoint_commutant_apply line 37
  4. theorem OAI.KadisonKastler.tomitaAdjoint_dense line 46

    Source documentation

    Separation makes the commutant orbit dense, hence the adjoint domain dense.

    theorem tomitaAdjoint_dense (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H)
    (hsep : Function.Injective (algebraVectorMap M Ω)) :
    Dense ((tomitaClosedLinearOperator M J Ω 1).adjoint.domain : Set H) := by
…

    Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.tomitaClosedLinearOperator