The semidirect fubini component of the Connes rigidity formalization.

def Connes.SemidirectFubini.l2CurryFiber {ι : Type u} {κ : Type v} (ξ : ↥(GroupL2 (ι × κ))) (i : ι) : ↥(GroupL2 κ)

Restrict a square-summable family on a product to one fibre.

Equations

• Connes.SemidirectFubini.l2CurryFiber ξ i = ⟨fun (k : κ) => ↑ξ (i, k), ⋯⟩

def Connes.SemidirectFubini.l2Curry (ι : Type u) (κ : Type v) : ↥(GroupL2 (ι × κ)) ≃ₗᵢ[ℂ] ↥(lp (fun (x : ι) => ↥(GroupL2 κ)) 2)

The l2Curry construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.SemidirectFubini.l2Curry_apply {ι : Type u} {κ : Type v} (ξ : ↥(GroupL2 (ι × κ))) (i : ι) (k : κ) : ↑(↑((l2Curry ι κ) ξ) i) k = ↑ξ (i, k)

@[simp]

theorem Connes.SemidirectFubini.l2Curry_symm_apply {ι : Type u} {κ : Type v} (ξ : ↥(lp (fun (x : ι) => ↥(GroupL2 κ)) 2)) (i : ι) (k : κ) : ↑((l2Curry ι κ).symm ξ) (i, k) = ↑(↑ξ i) k

def Connes.SemidirectFubini.semidirectFubiniCoordinates {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) : A ⋊[φ] K ≃ K × A

The semidirect product is identified with quotient-indexed kernel fibres. Paper: §3.

Equations

• Connes.SemidirectFubini.semidirectFubiniCoordinates φ = SemidirectProduct.equivProd.trans (Equiv.prodComm A K)

@[simp]

theorem Connes.SemidirectFubini.semidirectFubiniCoordinates_apply {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (g : A ⋊[φ] K) : (semidirectFubiniCoordinates φ) g = (g.right, g.left)

noncomputable def Connes.SemidirectFubini.semidirectFubini {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) : ↥(GroupL2 (A ⋊[φ] K)) ≃ₗᵢ[ℂ] ↥(lp (fun (x : K) => ↥(GroupL2 A)) 2)

The semidirect-product ℓ² carrier in fibre coordinates. Ported from the public OpenAI construction, then kept local to Zhou's §3 model.

Equations

• Connes.SemidirectFubini.semidirectFubini φ = (Connes.l2Reindex (Connes.SemidirectFubini.semidirectFubiniCoordinates φ)).trans (Connes.SemidirectFubini.l2Curry K A)

@[simp]

theorem Connes.SemidirectFubini.semidirectFubini_apply {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (ξ : ↥(GroupL2 (A ⋊[φ] K))) (k : K) (a : A) : ↑(↑((semidirectFubini φ) ξ) k) a = ↑ξ ⟨a, k⟩

@[simp]

theorem Connes.SemidirectFubini.semidirectFubini_symm_apply {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (ξ : ↥(lp (fun (x : K) => ↥(GroupL2 A)) 2)) (a : A) (k : K) : ↑((semidirectFubini φ).symm ξ) ⟨a, k⟩ = ↑(↑ξ k) a

theorem Connes.SemidirectFubini.semidirectFubini_leftRegular_apply {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (g : A ⋊[φ] K) (ξ : ↥(GroupL2 (A ⋊[φ] K))) (k : K) (a : A) : ↑(↑((semidirectFubini φ) (↑(leftRegularUnitary g) ξ)) k) a = ↑(↑((semidirectFubini φ) ξ) (g.right⁻¹ * k)) ((φ g.right⁻¹) (g.left⁻¹ * a))

theorem Connes.SemidirectFubini.semidirectFubini_leftRegular_inl_apply {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (b : A) (ξ : ↥(GroupL2 (A ⋊[φ] K))) (k : K) (a : A) : ↑(↑((semidirectFubini φ) (↑(leftRegularUnitary (SemidirectProduct.inl b)) ξ)) k) a = ↑(↑((semidirectFubini φ) ξ) k) (b⁻¹ * a)

theorem Connes.SemidirectFubini.semidirectFubini_leftRegular_inr_apply {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (h : K) (ξ : ↥(GroupL2 (A ⋊[φ] K))) (k : K) (a : A) : ↑(↑((semidirectFubini φ) (↑(leftRegularUnitary (SemidirectProduct.inr h)) ξ)) k) a = ↑(↑((semidirectFubini φ) ξ) (h⁻¹ * k)) ((φ h⁻¹) a)

theorem Connes.SemidirectFubini.semidirectFubini_conj_leftRegular_apply {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (g : A ⋊[φ] K) (ξ : ↥(lp (fun (x : K) => ↥(GroupL2 A)) 2)) (k : K) (a : A) : ↑(↑(((semidirectFubini φ).conjStarAlgEquiv ↑(leftRegularUnitary g)) ξ) k) a = ↑(↑ξ (g.right⁻¹ * k)) ((φ g.right⁻¹) (g.left⁻¹ * a))

theorem Connes.SemidirectFubini.semidirectFubini_leftRegular_inl {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (b : A) (ξ : ↥(lp (fun (x : K) => ↥(GroupL2 A)) 2)) (k : K) (a : A) : ↑(↑(((semidirectFubini φ).conjStarAlgEquiv ↑(leftRegularUnitary (SemidirectProduct.inl b))) ξ) k) a = ↑(↑ξ k) (b⁻¹ * a)

theorem Connes.SemidirectFubini.semidirectFubini_leftRegular_inr {A : Type u} {K : Type v} [Group A] [Group K] (φ : K →* MulAut A) (h : K) (ξ : ↥(lp (fun (x : K) => ↥(GroupL2 A)) 2)) (k : K) (a : A) : ↑(↑(((semidirectFubini φ).conjStarAlgEquiv ↑(leftRegularUnitary (SemidirectProduct.inr h))) ξ) k) a = ↑(↑ξ (h⁻¹ * k)) ((φ h⁻¹) a)