PointedMatrixSum.lean`

13 declarations, 0 contain sorry, 0 declared as axioms

Tensor products of pointed matrix-site systems

The two site families act in the two tensor legs. Finite words split into their two subwords, and their vector moments multiply. Cyclicity follows from the dense tensor-product orbit; separation follows by the same argument for the commutants. No modular or infinite-product input is used.

def OAI.KadisonKastler.sumLeftList line 26
def OAI.KadisonKastler.sumRightList line 29
theorem OAI.KadisonKastler.sumLeftList_nodup line 32
theorem OAI.KadisonKastler.sumRightList_nodup line 38
theorem OAI.KadisonKastler.sumList_scalar_prod line 44
theorem OAI.KadisonKastler.sumList_operator_prod line 57

theorem OAI.KadisonKastler.separating_spatialProduct_vector_of_separating line 81

Source documentation

Separation in each tensor leg implies separation of the product vector, without requiring supplied modular conjugations.

theorem separating_spatialProduct_vector_of_separating
    (M : VonNeumannAlgebra H) (N : VonNeumannAlgebra K) (Ω : H) (ξ : K)
    (hM : Function.Injective (algebraVectorMap M Ω))
    (hN : Function.Injective (algebraVectorMap N ξ)) :
    Function.Injective (algebraVectorMap (spatialProductAlgebra M N) (tensorVector ξ Ω)) := by
…

Mentions: OAI.KadisonKastler.algebraVectorMap, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.tensorVector

def OAI.KadisonKastler.PointedMatrixSites.sumSite line 120

Source documentation

The actual site family on the two tensor legs.

def sumSite (S : PointedMatrixSites M Ω ν) (T : PointedMatrixSites N ξ η) :
    I ⊕ J → MatrixUnitSystem (Fin 2) (SpatialHilbert H K →L[ℂ] SpatialHilbert H K) :=
…

Mentions: OAI.KadisonKastler.PointedMatrixSites

theorem OAI.KadisonKastler.PointedMatrixSites.site_mem line 125
theorem OAI.KadisonKastler.PointedMatrixSites.sumSite_generates line 131
theorem OAI.KadisonKastler.PointedMatrixSites.sumSite_moments line 176
def OAI.KadisonKastler.PointedMatrixSites.sum line 207
Source documentation
Tensoring two pointed systems constructs their sum-indexed system.
```
def sum (S : PointedMatrixSites M Ω ν) (T : PointedMatrixSites N ξ η) :
    PointedMatrixSites (spatialProductAlgebra M N) (tensorVector ξ Ω) (Sum.elim ν η) where
…
```
Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.tensorVector

theorem OAI.KadisonKastler.pointedMatrixSites_sum line 244

Source documentation

The sum clause of the pointed-product input is an actual construction.

theorem pointedMatrixSites_sum {I J : Type*} {M : VonNeumannAlgebra H} {N : VonNeumannAlgebra K}
    {Ω : H} {ξ : K} {ν : I → ℝ} {η : J → ℝ}
    (S : PointedMatrixSites M Ω ν) (T : PointedMatrixSites N ξ η) :
    Nonempty (PointedMatrixSites (spatialProductAlgebra M N) (tensorVector ξ Ω) (Sum.elim ν η)) :=
…

Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.spatialProductAlgebra, OAI.KadisonKastler.tensorVector