MIPRE.Background.Repetition.CommutingRepetition.VN.Crossed.Product

The covariant representation #

noncomputable def CommutingRepetition.VN.Crossed.π {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y : K →L[ℂ ] K) :

L2Q K →L[ℂ ] L2Q K

π(y) = ⊕_s σ_{-s}(y).

Equations

CommutingRepetition.VN.Crossed.π M Ω y = CommutingRepetition.VN.Crossed.diag fun (s : ℚ) => CommutingRepetition.VN.Modular.σ M Ω (-↑s) y

Instances For

source

theorem CommutingRepetition.VN.Crossed.isBddFam_π {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y : K →L[ℂ ] K) :

IsBddFam fun (s : ℚ) => Modular.σ M Ω (-↑s) y

source

theorem CommutingRepetition.VN.Crossed.π_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y : K →L[ℂ ] K) (f : L2Q K) (s : ℚ) :

↑((π M Ω y) f) s = (Modular.σ M Ω (-↑s) y) (↑f s)

source

theorem CommutingRepetition.VN.Crossed.norm_π_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y : K →L[ℂ ] K) :

‖π M Ω y‖ ≤ ‖y‖

source

theorem CommutingRepetition.VN.Crossed.π_sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y : K →L[ℂ ] K) (g : ℚ) (v : K) :

(π M Ω y) ((sgl g) v) = (sgl g) ((Modular.σ M Ω (-↑g) y) v)

source

theorem CommutingRepetition.VN.Crossed.π_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y z : K →L[ℂ ] K) :

π M Ω (y + z) = π M Ω y + π M Ω z

source

theorem CommutingRepetition.VN.Crossed.π_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (c : ℂ) (y : K →L[ℂ ] K) :

π M Ω (c • y) = c • π M Ω y

source

theorem CommutingRepetition.VN.Crossed.π_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y z : K →L[ℂ ] K) :

π M Ω (y * z) = π M Ω y * π M Ω z

source

theorem CommutingRepetition.VN.Crossed.π_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y : K →L[ℂ ] K) :

π M Ω (star y) = star (π M Ω y)

source

theorem CommutingRepetition.VN.Crossed.π_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :

π M Ω 1 = 1

source

theorem CommutingRepetition.VN.Crossed.π_zero {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :

π M Ω 0 = 0

source

theorem CommutingRepetition.VN.Crossed.shift_π_shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (g : ℚ) (y : K →L[ℂ ] K) :

shift g * π M Ω y * shift (-g) = π M Ω (Modular.σ M Ω (↑g) y)

Covariance: λ(g) π(y) λ(g)* = π(σ_g y).

source

theorem CommutingRepetition.VN.Crossed.π_shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (g : ℚ) (y : K →L[ℂ ] K) :

π M Ω y * shift g = shift g * π M Ω (Modular.σ M Ω (-↑g) y)

The crossed product #

source

def CommutingRepetition.VN.Crossed.gens {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :

Set (L2Q K →L[ℂ ] L2Q K)

The generating set π(M) ∪ λ(ℚ).

Equations

One or more equations did not get rendered due to their size.

Instances For

source

noncomputable def CommutingRepetition.VN.Crossed.crossed {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) :

VonNeumannAlgebra (L2Q K)

The crossed product ℛ = M ⋊_σ ℚ.

Equations

CommutingRepetition.VN.Crossed.crossed M Ω = CommutingRepetition.VN.wstar (CommutingRepetition.VN.Crossed.gens M Ω)

Instances For

source

theorem CommutingRepetition.VN.Crossed.π_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {y : K →L[ℂ ] K} (hy : y ∈ M) :

π M Ω y ∈ crossed M Ω

source

theorem CommutingRepetition.VN.Crossed.shift_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (g : ℚ) :

shift g ∈ crossed M Ω

source

theorem CommutingRepetition.VN.Crossed.star_mem_gens {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {T : L2Q K →L[ℂ ] L2Q K} (hT : T ∈ gens M Ω) :

star T ∈ gens M Ω

source

theorem CommutingRepetition.VN.Crossed.mem_commutant_of_commute_gens {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {z : L2Q K →L[ℂ ] L2Q K} (h : ∀ T ∈ gens M Ω, Commute T z) :

z ∈ (crossed M Ω).commutant

An operator commuting with the generators lies in the commutant of the crossed product.

The vector `Ω̂ = δ₀ ⊗ Ω` #

source

noncomputable def CommutingRepetition.VN.Crossed.Ωh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (Ω : K) :

L2Q K

Ω̂ = δ₀ ⊗ Ω.

Equations

CommutingRepetition.VN.Crossed.Ωh Ω = (CommutingRepetition.VN.Crossed.sgl 0) Ω

Instances For

source

theorem CommutingRepetition.VN.Crossed.norm_Ωh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (Ω : K) :

‖Ωh Ω‖ = ‖Ω‖

source

theorem CommutingRepetition.VN.Crossed.π_Ωh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y : K →L[ℂ ] K) :

(π M Ω y) (Ωh Ω) = (sgl 0) (y Ω)

source

theorem CommutingRepetition.VN.Crossed.shift_π_Ωh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (g : ℚ) (y : K →L[ℂ ] K) :

(shift g) ((π M Ω y) (Ωh Ω)) = (sgl g) (y Ω)

source

theorem CommutingRepetition.VN.Crossed.inner_sgl_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (v : K) (f : L2Q K) :

inner ℂ ((sgl g) v) f = inner ℂ v (↑f g)

source

theorem CommutingRepetition.VN.Crossed.inner_Ωh_shift_π {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (g : ℚ) (y : K →L[ℂ ] K) :

inner ℂ (Ωh Ω) ((shift g * π M Ω y) (Ωh Ω)) = if g = 0 then inner ℂ Ω (y Ω) else 0

The dual state: ⟪Ω̂, λ(g) π(y) Ω̂⟫ = δ_{g,0} ⟪Ω, yΩ⟫.

source

noncomputable def CommutingRepetition.VN.Crossed.comp0 {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] (X : L2Q K →L[ℂ ] L2Q K) :

K →L[ℂ ] K

The compression E(X) = ev₀ X sgl₀.

Equations

CommutingRepetition.VN.Crossed.comp0 X = CommutingRepetition.VN.Crossed.ev 0 ∘SL X ∘SL CommutingRepetition.VN.Crossed.sgl 0

Instances For

source

theorem CommutingRepetition.VN.Crossed.comp0_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (X : L2Q K →L[ℂ ] L2Q K) (v : K) :

(comp0 X) v = ↑(X ((sgl 0) v)) 0

source

theorem CommutingRepetition.VN.Crossed.comp0_π {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (y : K →L[ℂ ] K) :

comp0 (π M Ω y) = y

source

theorem CommutingRepetition.VN.Crossed.inner_Ωh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (Ω : K) (X : L2Q K →L[ℂ ] L2Q K) :

inner ℂ (Ωh Ω) (X (Ωh Ω)) = inner ℂ Ω ((comp0 X) Ω)

source

theorem CommutingRepetition.VN.Crossed.comp0_one {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] :

comp0 1 = 1

source

theorem CommutingRepetition.VN.Crossed.comp0_add {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (X Y : L2Q K →L[ℂ ] L2Q K) :

comp0 (X + Y) = comp0 X + comp0 Y

source

theorem CommutingRepetition.VN.Crossed.comp0_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (c : ℂ) (X : L2Q K →L[ℂ ] L2Q K) :

comp0 (c • X) = c • comp0 X

source

theorem CommutingRepetition.VN.Crossed.inner_sgl_right {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (w : K) (f : L2Q K) :

inner ℂ f ((sgl g) w) = inner ℂ (↑f g) w

source

theorem CommutingRepetition.VN.Crossed.comp0_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (X : L2Q K →L[ℂ ] L2Q K) :

comp0 (star X) = star (comp0 X)

source

theorem CommutingRepetition.VN.Crossed.norm_comp0_le {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (X : L2Q K →L[ℂ ] L2Q K) :

‖comp0 X‖ ≤ ‖X‖

source

theorem CommutingRepetition.VN.Crossed.comp0_nonneg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {X : L2Q K →L[ℂ ] L2Q K} (hX : 0 ≤ X) :

0 ≤ comp0 X

source

theorem CommutingRepetition.VN.Crossed.isCyclic_Ωh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hc : IsCyclic (↑M) Ω) :

IsCyclic (↑(crossed M Ω)) (Ωh Ω)

Ω̂ is cyclic for the crossed product.

The commutant: `1 ⊗ y′` and `W_g = λ(g)(1 ⊗ Δ^{-ig})` #

source

theorem CommutingRepetition.VN.Crossed.amp_commutant_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {y' : K →L[ℂ ] K} (hy' : y' ∈ M.commutant) :

amp y' ∈ (crossed M Ω).commutant

source

noncomputable def CommutingRepetition.VN.Crossed.W {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (g : ℚ) :

L2Q K →L[ℂ ] L2Q K

W_g = λ(g)(1 ⊗ Δ^{-ig}).

Equations

CommutingRepetition.VN.Crossed.W M Ω g = CommutingRepetition.VN.Crossed.shift g * CommutingRepetition.VN.Crossed.amp (CommutingRepetition.VN.Modular.Δit M Ω (-↑g))

Instances For

source

theorem CommutingRepetition.VN.Crossed.W_Ωh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (g : ℚ) :

(W M Ω g) (Ωh Ω) = (sgl g) Ω

source

theorem CommutingRepetition.VN.Crossed.W_mem_commutant {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (g : ℚ) :

W M Ω g ∈ (crossed M Ω).commutant

source

theorem CommutingRepetition.VN.Crossed.isSeparating_Ωh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) :

IsSeparating (↑(crossed M Ω)) (Ωh Ω)

Ω̂ is cyclic for the commutant of the crossed product, hence separating.

The covariant representation #

The crossed product #

The vector Ω̂ = δ₀ ⊗ Ω #

The commutant: 1 ⊗ y′ and W_g = λ(g)(1 ⊗ Δ^{-ig}) #

The vector `Ω̂ = δ₀ ⊗ Ω` #

The commutant: `1 ⊗ y′` and `W_g = λ(g)(1 ⊗ Δ^{-ig})` #