OAI/Analysis/KadisonKastler/TomitaGraphInvolution.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The involution on the closed Tomita graph

Taking adjoints on the algebraic core becomes a continuous conjugate-linear coordinate swap. Hence its involution identity survives graph closure.

  1. def OAI.KadisonKastler.tomitaGraphFlip line 20

    Source documentation

    Adjoint on graph vectors, with the fixed second-coordinate identification.

    def tomitaGraphFlip (J : H ≃ₗᵢ⋆[ℂ] H) : TomitaGraphHilbert H ≃ₗᵢ⋆[ℂ] TomitaGraphHilbert H where
…

    Mentions: OAI.KadisonKastler.TomitaGraphHilbert

  2. theorem OAI.KadisonKastler.tomitaGraphFlip_zero line 36
  3. theorem OAI.KadisonKastler.tomitaGraphFlip_one line 40
  4. theorem OAI.KadisonKastler.tomitaGraphFlip_vector line 43
  5. theorem OAI.KadisonKastler.tomitaGraphFlip_mem line 49
  6. theorem OAI.KadisonKastler.rescaledGraph_no_horizontal line 63
  7. theorem OAI.KadisonKastler.tomitaClosedLinearOperator_injective line 72

    Source documentation

    The closed Tomita operator has no kernel.

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

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