Dual automorphisms of Zhou's compact kernel

This file packages the dual of a discrete automorphism of the concrete kernel and proves continuity and Haar preservation. It is the common §3 input for the crossed-action conjugacy and the §4 spectral detector.

@[reducible, inline]

abbrev Connes.PaperDualAutomorphism.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualAutomorphism.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperDualAutomorphism.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperDualAutomorphism.CharacterSpace = Connes.PaperDualTopology.CharacterSpace

noncomputable def Connes.PaperDualAutomorphism.continuousMulAut (e : AddAut D) : Multiplicative D →ₜ* Multiplicative D

The continuousMulAut construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.PaperDualAutomorphism.continuousMulAut_apply (e : AddAut D) (x : Multiplicative D) : (continuousMulAut e) x = Multiplicative.ofAdd (e (Multiplicative.toAdd x))

noncomputable def Connes.PaperDualAutomorphism.dualCharacterEquiv (e : AddAut D) : CharacterSpace ≃+ CharacterSpace

The dual automorphism is precomposition by the inverse kernel automorphism.

Equations

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

@[simp]

theorem Connes.PaperDualAutomorphism.dualCharacterEquiv_apply (e : AddAut D) (χ : CharacterSpace) (x : D) : (Additive.toMul ((dualCharacterEquiv e) χ)) (Multiplicative.ofAdd x) = (Additive.toMul χ) (Multiplicative.ofAdd ((AddEquiv.symm e) x))

theorem Connes.PaperDualAutomorphism.dualCharacterEquiv_continuous (e : AddAut D) : Continuous ⇑(dualCharacterEquiv e)