Crossed-product factor transport

This module first transports the full measurable crossed-product generator family across an equivariant Haar equivalence. It then treats the continuous coefficient closure used in Zhou's §3: a norm-dense coefficient family has the same von Neumann closure as all continuous coefficients, and an equivariant measure-preserving homeomorphism transports that closure. The homeomorphism is not required to preserve the addition on either compact group.

theorem Connes.CrossedProduct.crossedHaarHilbertEquiv_multiplier_conj {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) (f : ↥(crossedCoefficient X)) : (crossedHaarHilbertEquiv e).conjStarAlgEquiv (crossedMultiplier X f) = crossedMultiplier Y ((MeasureTheory.Lp.compMeasurePreserving ⇑e.toMeasurableEquiv.symm ⋯) f)

theorem Connes.CrossedProduct.crossedCoefficient_pullback_symm_apply {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) (f : ↥(crossedCoefficient Y)) : (MeasureTheory.Lp.compMeasurePreserving ⇑e.toMeasurableEquiv.symm ⋯) ((MeasureTheory.Lp.compMeasurePreserving ⇑e.toMeasurableEquiv ⋯) f) = f

theorem Connes.CrossedProduct.crossedGeneratorSet_image {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) : ⇑(crossedHaarHilbertEquiv e).conjStarAlgEquiv '' crossedGeneratorSet X = crossedGeneratorSet Y

theorem Connes.CrossedProduct.crossedHaarHilbertEquiv_mem_algebra_iff {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) (T : ↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X)) : T ∈ (crossedProductModel X).algebra ↔ (crossedHaarHilbertEquiv e).conjStarAlgEquiv T ∈ (crossedProductModel Y).algebra

structure Connes.CrossedProduct.EquivariantHaarHomeomorph {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] (X : HaarProbabilityAction K Ω) (Y : HaarProbabilityAction K Ξ) : Type (max v w)

An equivariant measure-preserving homeomorphism between Haar actions. Unlike a compact-group equivalence, the homeomorphism need not preserve addition; this is the boundary needed by Zhou's quadratic fiber shear.

• toHomeomorph : Ω ≃ₜ Ξ

  The toHomeomorph component of EquivariantHaarHomeomorph.

• measure_preserving : MeasureTheory.MeasurePreserving (⇑self.toHomeomorph) X.measure Y.measure
• equivariant (k : K) (z : Ω) : self.toHomeomorph ((X.action k) z) = (Y.action k) (self.toHomeomorph z)

def Connes.CrossedProduct.EquivariantHaarHomeomorph.toEquivariantHaarEquiv {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] [BorelSpace Ω] [BorelSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarHomeomorph X Y) : EquivariantHaarEquiv X Y

Forget the topology of an equivariant Haar homeomorphism, retaining its measurable, measure-preserving, equivariant action equivalence.

Equations

• e.toEquivariantHaarEquiv = { toMeasurableEquiv := e.toHomeomorph.toMeasurableEquiv, measure_preserving := ⋯, equivariant := ⋯ }

theorem Connes.CrossedProduct.haarProbabilitySource {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : MeasureTheory.IsProbabilityMeasure X.measure

theorem Connes.CrossedProduct.haarProbabilityTarget {K : Type u} [Group K] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] (Y : HaarProbabilityAction K Ξ) : MeasureTheory.IsProbabilityMeasure Y.measure

noncomputable def Connes.CrossedProduct.crossedFiberwiseOperatorContinuousLinearMap {K : Type u} {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] : (E →L[ℂ] E) →L[ℂ] ↥(lp (fun (x : K) => E) 2) →L[ℂ] ↥(lp (fun (x : K) => E) 2)

Apply a bounded operator to each fibre of a square-summable family.

Equations

• Connes.CrossedProduct.crossedFiberwiseOperatorContinuousLinearMap = { toFun := Connes.CrossedProduct.crossedFiberwiseOperator, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

noncomputable def Connes.CrossedProduct.continuousCrossedMultiplier {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [CompactSpace Ω] [BorelSpace Ω] (X : HaarProbabilityAction K Ω) : C(Ω, ℂ) →L[ℂ] ↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X)

Continuous coefficients act as a continuous family of fiberwise multipliers on the regular crossed-product Hilbert space.

Equations

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

@[simp]

theorem Connes.CrossedProduct.continuousCrossedMultiplier_apply {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [CompactSpace Ω] [BorelSpace Ω] (X : HaarProbabilityAction K Ω) (q : C(Ω, ℂ)) : (continuousCrossedMultiplier X) q = crossedMultiplier X ((ContinuousMap.toLp ⊤ X.measure ℂ) q)

Evaluating the continuous-coefficient multiplier agrees with the crossed-product multiplier of the corresponding L∞ coefficient.

def Connes.CrossedProduct.continuousCrossedGeneratorSet {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [CompactSpace Ω] [BorelSpace Ω] (X : HaarProbabilityAction K Ω) : Set (↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X))

The regular crossed-product generators with all continuous coefficient multipliers and all action unitaries.

Equations

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

def Connes.CrossedProduct.crossedGeneratorSetOfContinuousCoefficients {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [CompactSpace Ω] [BorelSpace Ω] (X : HaarProbabilityAction K Ω) {I : Type u_1} (v : I → C(Ω, ℂ)) : Set (↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X))

The regular crossed-product generators cut down to a specified family of continuous coefficients, together with all action unitaries.

Equations

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

theorem Connes.CrossedProduct.vonNeumannClosure_crossedGeneratorSetOfContinuousCoefficients_eq {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [CompactSpace Ω] [BorelSpace Ω] (X : HaarProbabilityAction K Ω) {I : Type u_1} (v : I → C(Ω, ℂ)) (hv : (Submodule.span ℂ (Set.range v)).topologicalClosure = ⊤) : vonNeumannClosure (crossedGeneratorSetOfContinuousCoefficients X v) = vonNeumannClosure (continuousCrossedGeneratorSet X)

If a family of continuous coefficients has norm-dense linear span, then its multipliers and the action unitaries generate the same von Neumann closure as all continuous-coefficient multipliers and the action unitaries.

theorem Connes.CrossedProduct.continuousCrossedClosure_mem_iff {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] [CompactSpace Ω] [BorelSpace Ω] [CompactSpace Ξ] [BorelSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarHomeomorph X Y) (T : ↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X)) : T ∈ vonNeumannClosure (continuousCrossedGeneratorSet X) ↔ (crossedHaarHilbertEquiv e.toEquivariantHaarEquiv).conjStarAlgEquiv T ∈ vonNeumannClosure (continuousCrossedGeneratorSet Y)

An equivariant measure-preserving homeomorphism transports membership in the von Neumann closure generated by continuous multipliers and action unitaries. No compatibility with the compact-group additions is required.