The semidirect generator transport component of the Connes rigidity formalization.

def Connes.SemidirectGeneratorTransport.generatorSet {A : Type u_1} {K : Type u_2} [Group A] [Group K] (φ : K →* MulAut A) : Set (↥(GroupL2 (A ⋊[φ] K)) →L[ℂ] ↥(GroupL2 (A ⋊[φ] K)))

The generatorSet construction used in the Connes rigidity formalization.

Equations

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

structure Connes.SemidirectGeneratorTransport.Data {A : Type u_1} {K : Type u_2} [Group A] [Group K] {φ₁ φ₂ : K →* MulAut A} (U : ↥(GroupL2 (A ⋊[φ₁] K)) ≃ₗᵢ[ℂ] ↥(GroupL2 (A ⋊[φ₂] K))) : Prop

The two generator families are the only analytic data needed for factor transport. Paper: §3.

• kernel_generator (a : A) : U.conjStarAlgEquiv ↑((leftRegularRepresentation (A ⋊[φ₁] K)) (SemidirectProduct.inl a)) = ↑((leftRegularRepresentation (A ⋊[φ₂] K)) (SemidirectProduct.inl a))
• quotient_generator (k : K) : U.conjStarAlgEquiv ↑((leftRegularRepresentation (A ⋊[φ₁] K)) (SemidirectProduct.inr k)) = ↑((leftRegularRepresentation (A ⋊[φ₂] K)) (SemidirectProduct.inr k))

theorem Connes.SemidirectGeneratorTransport.generatorSet_image_eq {A : Type u_1} {K : Type u_2} [Group A] [Group K] {φ₁ φ₂ : K →* MulAut A} {U : ↥(GroupL2 (A ⋊[φ₁] K)) ≃ₗᵢ[ℂ] ↥(GroupL2 (A ⋊[φ₂] K))} (data : Data U) : ⇑U.conjStarAlgEquiv '' generatorSet φ₁ = generatorSet φ₂

theorem Connes.SemidirectGeneratorTransport.mem_regularClosure_iff {A : Type u_1} {K : Type u_2} [Group A] [Group K] {φ₁ φ₂ : K →* MulAut A} {U : ↥(GroupL2 (A ⋊[φ₁] K)) ≃ₗᵢ[ℂ] ↥(GroupL2 (A ⋊[φ₂] K))} (data : Data U) (T : ↥(GroupL2 (A ⋊[φ₁] K)) →L[ℂ] ↥(GroupL2 (A ⋊[φ₁] K))) : T ∈ vonNeumannClosure (Set.range fun (g : A ⋊[φ₁] K) => ↑((leftRegularRepresentation (A ⋊[φ₁] K)) g)) ↔ U.conjStarAlgEquiv T ∈ vonNeumannClosure (Set.range fun (g : A ⋊[φ₂] K) => ↑((leftRegularRepresentation (A ⋊[φ₂] K)) g))