The antiunitary Ĵ

theorem CommutingRepetition.VN.Crossed.summable_norm_sq_Jh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f : L2Q K) : Summable fun (h : ℚ) => ‖(Modular.Jm M Ω) ((Modular.Δit M Ω (-↑h)) (↑f (-h)))‖ ^ 2

noncomputable def CommutingRepetition.VN.Crossed.JhPre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) : L2Q K →ₗ⋆[ℂ] L2Q K

Ĵ as a conjugate-linear map: (Ĵ f)(h) = J Δ^{-ih} f(-h).

Equations

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

theorem CommutingRepetition.VN.Crossed.JhPre_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f : L2Q K) (h : ℚ) : ↑((JhPre M Ω hs hc) f) h = (Modular.Jm M Ω) ((Modular.Δit M Ω (-↑h)) (↑f (-h)))

theorem CommutingRepetition.VN.Crossed.norm_JhPre {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f : L2Q K) : ‖(JhPre M Ω hs hc) f‖ = ‖f‖

noncomputable def CommutingRepetition.VN.Crossed.Jh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) : L2Q K →L⋆[ℂ] L2Q K

The antiunitary Ĵ of the crossed product.

Equations

• CommutingRepetition.VN.Crossed.Jh M Ω hs hc = (CommutingRepetition.VN.Crossed.JhPre M Ω hs hc).mkContinuous 1 ⋯

theorem CommutingRepetition.VN.Crossed.Jh_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f : L2Q K) (h : ℚ) : ↑((Jh M Ω hs hc) f) h = (Modular.Jm M Ω) ((Modular.Δit M Ω (-↑h)) (↑f (-h)))

theorem CommutingRepetition.VN.Crossed.norm_Jh_apply {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f : L2Q K) : ‖(Jh M Ω hs hc) f‖ = ‖f‖

theorem CommutingRepetition.VN.Crossed.Jh_sgl {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (g : ℚ) (v : K) : (Jh M Ω hs hc) ((sgl g) v) = (sgl (-g)) ((Modular.Jm M Ω) ((Modular.Δit M Ω ↑g) v))

theorem CommutingRepetition.VN.Crossed.inner_Δit_Δit {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (u v : K) : inner ℂ ((Modular.Δit M Ω t) u) ((Modular.Δit M Ω t) v) = inner ℂ u v

theorem CommutingRepetition.VN.Crossed.inner_Jm_Jm' {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (u v : K) : inner ℂ ((Modular.Jm M Ω) u) ((Modular.Jm M Ω) v) = inner ℂ v u

theorem CommutingRepetition.VN.Crossed.inner_Jh_Jh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f k : L2Q K) : inner ℂ ((Jh M Ω hs hc) f) ((Jh M Ω hs hc) k) = inner ℂ k f

theorem CommutingRepetition.VN.Crossed.Jh_Jh {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f : L2Q K) : (Jh M Ω hs hc) ((Jh M Ω hs hc) f) = f

theorem CommutingRepetition.VN.Crossed.inner_Jh_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f k : L2Q K) : inner ℂ ((Jh M Ω hs hc) f) k = inner ℂ ((Jh M Ω hs hc) k) f

theorem CommutingRepetition.VN.Crossed.Jh_real_smul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (r : ℝ) (f : L2Q K) : (Jh M Ω hs hc) (r • f) = r • (Jh M Ω hs hc) f

theorem CommutingRepetition.VN.Crossed.Jh_amp_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f : L2Q K) : (Jh M Ω hs hc) ((amp (Modular.R M Ω)) f) = (amp (2 - Modular.R M Ω)) ((Jh M Ω hs hc) f)

theorem CommutingRepetition.VN.Crossed.Jh_amp_Tm {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (f : L2Q K) : (Jh M Ω hs hc) ((amp (Modular.Tm M Ω)) f) = (amp (Modular.Tm M Ω)) ((Jh M Ω hs hc) f)

theorem CommutingRepetition.VN.Crossed.amp_R_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : IsSelfAdjoint (amp (Modular.R M Ω))

theorem CommutingRepetition.VN.Crossed.amp_Tm_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : IsSelfAdjoint (amp (Modular.Tm M Ω))

theorem CommutingRepetition.VN.Crossed.amp_two_sub_R_isSelfAdjoint {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : IsSelfAdjoint (amp (2 - Modular.R M Ω))

The bounded identity on generators

theorem CommutingRepetition.VN.Crossed.Th_Jh_gen {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (g : ℚ) {y : K →L[ℂ] K} (hy : y ∈ M) : (amp (Modular.Tm M Ω)) ((Jh M Ω hs hc) ((shift g * π M Ω y) (Ωh Ω))) = (amp (2 - Modular.R M Ω)) ((star (shift g * π M Ω y)) (Ωh Ω))

RvD Lemma 4.5 for (ℛ, Ω̂) on a generator a = λ(g) π(y): T̂ Ĵ (a Ω̂) = (2 − R̂)(a* Ω̂).

The *-algebra spanned by the generators

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

The set {λ(g) π(y) : g ∈ ℚ, y ∈ M}.

Equations

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

theorem CommutingRepetition.VN.Crossed.genSet_mul {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a b : L2Q K →L[ℂ] L2Q K} (ha : a ∈ genSet M Ω) (hb : b ∈ genSet M Ω) : a * b ∈ genSet M Ω

theorem CommutingRepetition.VN.Crossed.genSet_star {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : L2Q K →L[ℂ] L2Q K} (ha : a ∈ genSet M Ω) : star a ∈ genSet M Ω

theorem CommutingRepetition.VN.Crossed.one_mem_genSet {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) : 1 ∈ genSet M Ω

noncomputable def CommutingRepetition.VN.Crossed.spanAlg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) : StarSubalgebra ℂ (L2Q K →L[ℂ] L2Q K)

The *-subalgebra spanned by the generators λ(g) π(y).

Equations

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

theorem CommutingRepetition.VN.Crossed.mem_spanAlg_iff {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : L2Q K →L[ℂ] L2Q K} : a ∈ spanAlg M Ω hs hc ↔ a ∈ Submodule.span ℂ (genSet M Ω)

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

The bounded identity on ℛ

theorem CommutingRepetition.VN.Crossed.Th_Jh_spanAlg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : L2Q K →L[ℂ] L2Q K} (ha : a ∈ spanAlg M Ω hs hc) : (amp (Modular.Tm M Ω)) ((Jh M Ω hs hc) (a (Ωh Ω))) = (amp (2 - Modular.R M Ω)) ((star a) (Ωh Ω))

The identity T̂ Ĵ (aΩ̂) = (2 − R̂)(a*Ω̂) for a in the spanned *-algebra.

theorem CommutingRepetition.VN.Crossed.Th_Jh_mem {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {a : L2Q K →L[ℂ] L2Q K} (ha : a ∈ crossed M Ω) : (amp (Modular.Tm M Ω)) ((Jh M Ω hs hc) (a (Ωh Ω))) = (amp (2 - Modular.R M Ω)) ((star a) (Ωh Ω))

RvD Lemma 4.5 for (ℛ, Ω̂): T̂ Ĵ (aΩ̂) = (2 − R̂)(a*Ω̂) for all a ∈ ℛ.

Identification of the modular data

theorem CommutingRepetition.VN.Crossed.fiber_orth {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {u v : K} (h : ∀ y ∈ M, inner ℂ u (y Ω) + inner ℂ Ω (y v) = 0) : (Modular.R M Ω) u + (Modular.Tm M Ω) ((Modular.Jm M Ω) v) = 0

The one-fiber lemma: if ⟪u, yΩ⟫ + ⟪Ω, y v⟫ = 0 for all y ∈ M then R u + T J v = 0.

theorem CommutingRepetition.VN.Crossed.inner_add_inner_eq_zero_of_mem_orthogonal {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) {ζ : K} (hζ : ζ ∈ (↑(Modular.Kre M Ω))ᗮ) {b : K →L[ℂ] K} (hb : b ∈ M) : inner ℂ ζ (b Ω) + inner ℂ Ω (b ζ) = 0

The pairing identity characterising 𝒦ᗮ: ⟪ζ, bΩ⟫ + ⟪Ω, bζ⟫ = 0 for all b ∈ M.

theorem CommutingRepetition.VN.Crossed.hker_crossed {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {ζ : L2Q K} (hζ : ζ ∈ (↑(Modular.Kre (crossed M Ω) (Ωh Ω)))ᗮ) : (amp (Modular.R M Ω)) ζ + (amp (Modular.Tm M Ω)) ((Jh M Ω hs hc) ζ) = 0

hker for (ℛ, Ω̂): on 𝒦(ℛ, Ω̂)ᗮ, R̂ ζ + T̂ Ĵ ζ = 0, fiberwise from fiber_orth.

theorem CommutingRepetition.VN.Crossed.hfix_crossed {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) {ζ : L2Q K} (hζ : ζ ∈ Modular.Kre (crossed M Ω) (Ωh Ω)) : (amp (Modular.R M Ω)) ζ + (amp (Modular.Tm M Ω)) ((Jh M Ω hs hc) ζ) = 2 • ζ

hfix for (ℛ, Ω̂): on 𝒦(ℛ, Ω̂), R̂ ζ + T̂ Ĵ ζ = 2ζ, from the bounded identity.

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

(M4), the operator R̂: R(ℛ, Ω̂) = 1 ⊗ R.

theorem CommutingRepetition.VN.Crossed.Am_crossed {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (ζ : L2Q K) : (Modular.Am (crossed M Ω) (Ωh Ω)) ζ = (amp (Modular.Tm M Ω)) ((Jh M Ω hs hc) ζ)

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

(M4), T̂: T(ℛ, Ω̂) = 1 ⊗ T.

theorem CommutingRepetition.VN.Crossed.Jm_crossed {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (ζ : L2Q K) : (Modular.Jm (crossed M Ω) (Ωh Ω)) ζ = (Jh M Ω hs hc) ζ

(M4), Ĵ: the antiunitary of (ℛ, Ω̂) is Ĵ.

theorem CommutingRepetition.VN.Crossed.Δit_crossed {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) : Modular.Δit (crossed M Ω) (Ωh Ω) t = amp (Modular.Δit M Ω t)

(M4), the modular group: Δ̂^{it} = 1 ⊗ Δ^{it}.

The dual action

theorem CommutingRepetition.VN.Crossed.σ_crossed {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) (x : L2Q K →L[ℂ] L2Q K) : Modular.σ (crossed M Ω) (Ωh Ω) t x = amp (Modular.Δit M Ω t) * x * amp (Modular.Δit M Ω (-t))

theorem CommutingRepetition.VN.Crossed.amp_mul_diag {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (y : K →L[ℂ] K) : amp y * diag x = diag fun (s : ℚ) => y * x s

theorem CommutingRepetition.VN.Crossed.diag_mul_amp {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {x : ℚ → K →L[ℂ] K} (hx : IsBddFam x) (y : K →L[ℂ] K) : diag x * amp y = diag fun (s : ℚ) => x s * y

theorem CommutingRepetition.VN.Crossed.σ_crossed_π {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) (y : K →L[ℂ] K) : Modular.σ (crossed M Ω) (Ωh Ω) t (π M Ω y) = π M Ω (Modular.σ M Ω t y)

σ̂_t(π(y)) = π(σ_t y).

theorem CommutingRepetition.VN.Crossed.σ_crossed_shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) (g : ℚ) : Modular.σ (crossed M Ω) (Ωh Ω) t (shift g) = shift g

σ̂_t(λ(g)) = λ(g).

theorem CommutingRepetition.VN.Crossed.Δit_crossed_commute_shift {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (t : ℝ) (g : ℚ) : Commute (Modular.Δit (crossed M Ω) (Ωh Ω) t) (shift g)

theorem CommutingRepetition.VN.Crossed.shift_commute_R {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (g : ℚ) : Commute (shift g) (Modular.R (crossed M Ω) (Ωh Ω))

theorem CommutingRepetition.VN.Crossed.inner_amp_Δit_conj {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (t : ℝ) (a : L2Q K →L[ℂ] L2Q K) (u v : L2Q K) : inner ℂ u ((amp (Modular.Δit M Ω t) * a * amp (Modular.Δit M Ω (-t))) v) = inner ℂ ((amp (Modular.Δit M Ω (-t))) u) (a ((amp (Modular.Δit M Ω (-t))) v))

theorem CommutingRepetition.VN.Crossed.inner_shift_conj {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (g : ℚ) (a : L2Q K →L[ℂ] L2Q K) (u v : L2Q K) : inner ℂ u ((shift g * a * shift (-g)) v) = inner ℂ ((shift (-g)) u) (a ((shift (-g)) v))

theorem CommutingRepetition.VN.Crossed.σ_crossed_rat_spanAlg {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (s : ℚ) {a : L2Q K →L[ℂ] L2Q K} (ha : a ∈ spanAlg M Ω hs hc) : Modular.σ (crossed M Ω) (Ωh Ω) (↑s) a = shift s * a * shift (-s)

On the spanned *-algebra, σ̂_s = Ad λ(s) for s ∈ ℚ.

theorem CommutingRepetition.VN.Crossed.σ_crossed_rat {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (M : VonNeumannAlgebra K) (Ω : K) (hs : IsSeparating (↑M) Ω) (hc : IsCyclic (↑M) Ω) (s : ℚ) {x : L2Q K →L[ℂ] L2Q K} (hx : x ∈ crossed M Ω) : Modular.σ (crossed M Ω) (Ωh Ω) (↑s) x = shift s * x * shift (-s)

The dual action is inner on the rationals: σ̂_s(x) = λ(s) x λ(s)* for s ∈ ℚ, x ∈ ℛ.