RescaledGraphAction.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The common unitary action on rescaled graphs

Left and right multiplication by common unitaries acts on graph vectors through one unitary of the fixed two-coordinate Hilbert space. Thus each closed graph reduces this unitary whenever the right action belongs to the relevant commutant and has the prescribed value on the common vector.

def OAI.KadisonKastler.graphDiagonalUnitary line 22
Source documentation
Two unitary coordinate actions form an actual Hilbert-space unitary.
```
def graphDiagonalUnitary (u v : unitary (H →L[ℂ] H)) :
    unitary (TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) :=
…
```
Mentions: OAI.KadisonKastler.TomitaGraphHilbert
theorem OAI.KadisonKastler.graphDiagonalUnitary_apply_zero line 27
theorem OAI.KadisonKastler.graphDiagonalUnitary_apply_one line 35

def OAI.KadisonKastler.rescaledGraphAction line 44

Source documentation

The common graph action implementing x ↦ r*x*s.

def rescaledGraphAction (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (r s : unitary (H →L[ℂ] H)) :
    unitary (TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) :=
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert

theorem OAI.KadisonKastler.right_operator_on_algebra_vector line 50

theorem OAI.KadisonKastler.rescaledGraphAction_vector line 61

Source documentation

Exact action on graph vectors, before any closure argument.

theorem rescaledGraphAction_vector
    (P : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J)
    (Ω : H) (c : ℝ) (r s : unitary (H →L[ℂ] H))
    (hsright : conjugationOperator J (star (s : H →L[ℂ] H)) ∈ P.commutant)
    (hrright : conjugationOperator J (r : H →L[ℂ] H) ∈ P.commutant)
    (hsΩ : conjugationOperator J (star (s : H →L[ℂ] H)) Ω = (s : H →L[ℂ] H) Ω)
    (hrΩ : conjugationOperator J (r : H →L[ℂ] H) Ω = star (r : H →L[ℂ] H) Ω)
    (x : Algebra P) :
    (rescaledGraphAction J hJ r s :
      TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H)
      (rescaledGraphVector J Ω c x.val) =
        rescaledGraphVector J Ω c ((r : H →L[ℂ] H) * x.val * (s : H →L[ℂ] H)) := by
…

Mentions: OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rescaledGraphAction, OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.rescaledGraphVector

theorem OAI.KadisonKastler.rescaledGraphSubspace_invariant_of_vectors line 104

Source documentation

A bounded operator preserving defining graph vectors preserves the closed graph subspace.

theorem rescaledGraphSubspace_invariant_of_vectors
    (P : VonNeumannAlgebra H) (J : H ≃ₗᵢ⋆[ℂ] H) (Ω : H) (c : ℝ)
    (T : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H)
    (hT : ∀ x : Algebra P, ∃ y : Algebra P,
      T (rescaledGraphVector J Ω c x.val) = rescaledGraphVector J Ω c y.val)
    {ξ : TomitaGraphHilbert H} (hξ : ξ ∈ rescaledGraphSubspace P J Ω c) :
    T ξ ∈ rescaledGraphSubspace P J Ω c := by
…

Mentions: OAI.KadisonKastler.TomitaGraphHilbert, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.rescaledGraphVector, OAI.KadisonKastler.rescaledGraphSubspace

theorem OAI.KadisonKastler.rescaledGraphProjection_commutes line 122

Source documentation

The common right-action identities make the graph reduce the unitary implementing simultaneous left and right multiplication.

theorem rescaledGraphProjection_commutes
    (P : VonNeumannAlgebra H) (R : StarSubalgebra ℂ (H →L[ℂ] H))
    (hRP : R ≤ P.toStarSubalgebra)
    (J : H ≃ₗᵢ⋆[ℂ] H) (hJ : Function.Involutive J) (Ω : H) (c : ℝ)
    (hcomm : ∀ a ∈ R, conjugationOperator J (star a) ∈ P.commutant)
    (hvector : ∀ a ∈ R, conjugationOperator J (star a) Ω = a Ω)
    (r s : unitary (H →L[ℂ] H))
    (hr : (r : H →L[ℂ] H) ∈ R) (hs : (s : H →L[ℂ] H) ∈ R) :
    rescaledGraphProjection P J Ω c *
        (rescaledGraphAction J hJ r s : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) =
      (rescaledGraphAction J hJ r s : TomitaGraphHilbert H →L[ℂ] TomitaGraphHilbert H) *
        rescaledGraphProjection P J Ω c := by
…

Mentions: OAI.KadisonKastler.conjugationOperator, OAI.KadisonKastler.rescaledGraphProjection, OAI.KadisonKastler.rescaledGraphAction, OAI.KadisonKastler.TomitaGraphHilbert