PointedCyclicEquivalence.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Unitary reindexing of pointed matrix products

Matching finite-site moments identify the dense spans of all word vectors. The resulting Hilbert isometry intertwines every site and therefore the concrete von Neumann algebras they generate.

def OAI.KadisonKastler.PointedMatrixSites.siteGenerator line 26
theorem OAI.KadisonKastler.PointedMatrixSites.generates_siteGenerator line 29
theorem OAI.KadisonKastler.PointedMatrixSites.wordSpan_dense line 44
Source documentation
All finite word vectors have dense linear span.
```
theorem wordSpan_dense (S : PointedMatrixSites M Ω ν) :
    DenseRange (Finsupp.linearCombination ℂ S.wordVector) := by
…
```
Mentions: OAI.KadisonKastler.PointedMatrixSites
theorem OAI.KadisonKastler.PointedMatrixSites.reindex_symm line 54
theorem OAI.KadisonKastler.PointedMatrixSites.reindexed_wordSpan_dense line 60
def OAI.KadisonKastler.PointedMatrixSites.reindexEquivalence line 77
Source documentation
The actual Hilbert-space equivalence determined by all finite words.
```
def reindexEquivalence (S : PointedMatrixSites M Ω ν) (T : PointedMatrixSites N ξ η)
    (e : I ≃ J) (hweight : ∀ i, η (e i) = ν i) : H ≃ₗᵢ[ℂ] K :=
…
```
Mentions: OAI.KadisonKastler.PointedMatrixSites
theorem OAI.KadisonKastler.PointedMatrixSites.reindexEquivalence_word line 84
theorem OAI.KadisonKastler.PointedMatrixSites.reindexEquivalence_vector line 91
theorem OAI.KadisonKastler.PointedMatrixSites.reindexEquivalence_intertwines line 97
theorem OAI.KadisonKastler.PointedMatrixSites.reindexEquivalence_conjugate_site line 122
theorem OAI.KadisonKastler.PointedMatrixSites.reindexEquivalence_algebra line 132
Source documentation
The finite-word Hilbert equivalence transports the generated algebras.
```
theorem reindexEquivalence_algebra (S : PointedMatrixSites M Ω ν)
    (T : PointedMatrixSites N ξ η) (e : I ≃ J) (hweight : ∀ i, η (e i) = ν i) :
    spatialTransportAlgebra (S.reindexEquivalence T e hweight) M = N := by
…
```
Mentions: OAI.KadisonKastler.PointedMatrixSites, OAI.KadisonKastler.spatialTransportAlgebra

theorem OAI.KadisonKastler.PointedMatrixSites.exists_reindex_unitary line 159

Source documentation

The complete reindex clause of the published pointed-product input.

theorem exists_reindex_unitary (S : PointedMatrixSites M Ω ν)
    (T : PointedMatrixSites N ξ η) (e : I ≃ J) (hweight : ∀ i, η (e i) = ν i) :
    ∃ U : H ≃ₗᵢ[ℂ] K, U Ω = ξ ∧ ∀ x : H →L[ℂ] H, x ∈ M ↔ U.conjStarAlgEquiv x ∈ N := by
…

Mentions: OAI.KadisonKastler.PointedMatrixSites