OAI/Analysis/KadisonKastler/SpatialAssociatorTransport.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Tensoring Hilbert-space identifications

An isometric equivalence in either Hilbert tensor leg lifts to the completed tensor product. Conjugation by this equivalence transports both the bounded tensor operators and their generated spatial algebras.

  1. def OAI.KadisonKastler.spatialTensorEquiv line 27

    Source documentation

    The completed tensor product of two Hilbert-space identifications.

    def spatialTensorEquiv (f : H ≃ₗᵢ[ℂ] H') (g : K ≃ₗᵢ[ℂ] K') :
    SpatialHilbert H K ≃ₗᵢ[ℂ] SpatialHilbert H' K' :=
…
  2. theorem OAI.KadisonKastler.spatialTensorEquiv_coe line 39
  3. theorem OAI.KadisonKastler.spatialTensorEquiv_tmul line 46
  4. theorem OAI.KadisonKastler.spatialTensorEquiv_symm_tmul line 53
  5. theorem OAI.KadisonKastler.spatialTensorEquiv_conjugate_tensor line 64

    Source documentation

    Tensor-product operators transform componentwise.

    theorem spatialTensorEquiv_conjugate_tensor
    (f : H ≃ₗᵢ[ℂ] H') (g : K ≃ₗᵢ[ℂ] K') (a : H →L[ℂ] H) (b : K →L[ℂ] K) :
    (spatialTensorEquiv f g).conjStarAlgEquiv (spatialTensorOp a b) =
      spatialTensorOp (f.conjStarAlgEquiv a) (g.conjStarAlgEquiv b) := by
…

    Mentions: OAI.KadisonKastler.spatialTensorEquiv

  6. theorem OAI.KadisonKastler.spatialTransport_generated line 75

    Source documentation

    Transport commutes with taking the generated concrete von Neumann algebra.

    theorem spatialTransport_generated
    (f : H ≃ₗᵢ[ℂ] H') (S : StarSubalgebra ℂ (H →L[ℂ] H)) :
    spatialTransportAlgebra f (generatedVonNeumannAlgebra S) =
      generatedVonNeumannAlgebra (S.map f.conjStarAlgEquiv.toStarAlgHom) := by
…

    Mentions: OAI.KadisonKastler.spatialTransportAlgebra, OAI.KadisonKastler.generatedVonNeumannAlgebra

  7. theorem OAI.KadisonKastler.spatialTensorEquiv_spatialProduct line 89

    Source documentation

    Tensoring Hilbert-space identifications transports both spatial factors.

    theorem spatialTensorEquiv_spatialProduct
    (f : H ≃ₗᵢ[ℂ] H') (g : K ≃ₗᵢ[ℂ] K')
    (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K) :
    spatialTransportAlgebra (spatialTensorEquiv f g) (spatialProductAlgebra M D) =
      spatialProductAlgebra (spatialTransportAlgebra f M) (spatialTransportAlgebra g D) := by
…

    Mentions: OAI.KadisonKastler.spatialTransportAlgebra, OAI.KadisonKastler.spatialTensorEquiv, OAI.KadisonKastler.spatialProductAlgebra

  8. theorem OAI.KadisonKastler.spatialTensorEquiv_right_spatialProduct line 124

    Source documentation

    Changing only the second tensor leg preserves the first algebra.

    theorem spatialTensorEquiv_right_spatialProduct
    (g : K ≃ₗᵢ[ℂ] K') (M : VonNeumannAlgebra H) (D : VonNeumannAlgebra K) :
    spatialTransportAlgebra (spatialTensorEquiv (LinearIsometryEquiv.refl ℂ H) g)
      (spatialProductAlgebra M D) =
        spatialProductAlgebra M (spatialTransportAlgebra g D) := by
…

    Mentions: OAI.KadisonKastler.spatialTransportAlgebra, OAI.KadisonKastler.spatialTensorEquiv, OAI.KadisonKastler.spatialProductAlgebra