The crossed product transport component of the Connes rigidity formalization.
noncomputable def
Connes.CrossedProduct.crossedHaarHilbertEquiv
{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)
:
The crossedHaarHilbertEquiv construction used in the Connes rigidity formalization.
Equations
Instances For
@[simp]
theorem
Connes.CrossedProduct.crossedHaarHilbertEquiv_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)
(ξ : ↥(crossedHilbert X))
(k : K)
:
theorem
Connes.CrossedProduct.crossedBaseHaarEquiv_const_one
{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)
:
have x := ⋯;
have x_1 := ⋯;
(crossedBaseHaarEquiv e) ((MeasureTheory.Lp.const 2 X.measure) 1) = (MeasureTheory.Lp.const 2 Y.measure) 1
theorem
Connes.CrossedProduct.crossedHaarHilbertEquiv_vacuum
{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)
:
theorem
Connes.CrossedProduct.crossedBaseHaarEquiv_multiplier_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 X))
(ξ : ↥(crossedBaseHilbert X))
:
(crossedBaseHaarEquiv e) ((crossedBaseMultiplier X f) ξ) = (crossedBaseMultiplier Y ((MeasureTheory.Lp.compMeasurePreserving ⇑e.toMeasurableEquiv.symm ⋯) f))
((crossedBaseHaarEquiv e) ξ)
theorem
Connes.CrossedProduct.crossedBaseHaarEquiv_action
{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)
(k : K)
(ξ : ↥(crossedBaseHilbert X))
:
(crossedBaseHaarEquiv e) ((crossedActionL2Equiv X k) ξ) = (crossedActionL2Equiv Y k) ((crossedBaseHaarEquiv e) ξ)
theorem
Connes.CrossedProduct.crossedHaarHilbertEquiv_group_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)
(k : K)
(ξ : ↥(crossedHilbert X))
:
(crossedHaarHilbertEquiv e) ((crossedGroupUnitary X k) ξ) = (crossedGroupUnitary Y k) ((crossedHaarHilbertEquiv e) ξ)
theorem
Connes.CrossedProduct.crossedHaarHilbertEquiv_group_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)
(k : K)
:
(crossedHaarHilbertEquiv e).conjStarAlgEquiv ↑↑(crossedGroupUnitary X k) = ↑↑(crossedGroupUnitary Y k)