OAI/Analysis/KadisonKastler/PointedSitesTransport.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Spatial transport of pointed matrix products

Conjugating all site operators by one Hilbert-space equivalence preserves cyclicity, separation and every finite product-state moment.

  1. theorem OAI.KadisonKastler.matrixUnit_algebra_map line 21
  2. theorem OAI.KadisonKastler.spatialTransportEquiv_vector line 34
  3. def OAI.KadisonKastler.PointedMatrixSites.transport line 47

    Source documentation

    All concrete pointed-product data survive spatial transport.

    def transport (S : PointedMatrixSites M Ω ν) (e : H ≃ₗᵢ[ℂ] K) :
    PointedMatrixSites (spatialTransportAlgebra e M) (e Ω) ν where
…

    Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.spatialTransportAlgebra