The quotient action component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PaperQuotientAction.k : Type

The k construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.k = Connes.Construction.k

@[reducible, inline]

abbrev Connes.PaperQuotientAction.D : Type

The D construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.D = Connes.Construction.PaperKernel.D

@[reducible, inline]

abbrev Connes.PaperQuotientAction.H : Type

The H construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.H = Connes.Construction.H

@[reducible, inline]

abbrev Connes.PaperQuotientAction.CharacterSpace : Type

The CharacterSpace construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.CharacterSpace = Connes.PaperDualHaar.PaperCharacterSpace

@[reducible, inline]

abbrev Connes.PaperQuotientAction.Coordinates : Type

The Coordinates construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.Coordinates = Connes.PaperFactorIsomorphism.DualCoordinates

@[reducible, inline]

noncomputable abbrev Connes.PaperQuotientAction.CoordinateL2 : AddSubgroup (PaperDualTopology.Coordinates →ₘ[PaperDualTopology.coordinatesHaar] ℂ)

The CoordinateL2 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.CoordinateL2 = MeasureTheory.Lp ℂ 2 Connes.PaperDualTopology.coordinatesHaar

@[reducible, inline]

noncomputable abbrev Connes.PaperQuotientAction.KernelL2 : AddSubgroup (PreLp fun (x : Multiplicative D) => ℂ)

The KernelL2 construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.KernelL2 = Connes.GroupL2 (Multiplicative Connes.PaperQuotientAction.D)

@[instance_reducible]

noncomputable def Connes.PaperQuotientAction.paperDDecidableEq : DecidableEq D

The paperDDecidableEq construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.paperDDecidableEq = Classical.decEq Connes.PaperQuotientAction.D

@[instance_reducible]

noncomputable def Connes.PaperQuotientAction.paperMultiplicativeDDecidableEq : DecidableEq (Multiplicative D)

The paperMultiplicativeDDecidableEq construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.paperMultiplicativeDDecidableEq = Classical.decEq (Multiplicative Connes.PaperQuotientAction.D)

noncomputable def Connes.PaperQuotientAction.paperThetaOneAddEquiv (h : H) : D ≃+ D

The paperThetaOneAddEquiv construction used in the Connes rigidity formalization.

Equations

• Connes.PaperQuotientAction.paperThetaOneAddEquiv h = (Connes.Construction.PaperKernel.paperThetaOneLinearHom h).toAddEquiv

noncomputable def Connes.PaperQuotientAction.paperThetaTwoAddEquiv (h : H) : D ≃+ D

The additive kernel action underlying the second quotient. Paper: §2.

Equations

• Connes.PaperQuotientAction.paperThetaTwoAddEquiv h = (Connes.Construction.PaperKernel.paperThetaTwoLinearHom h).toAddEquiv

noncomputable def Connes.PaperQuotientAction.paperThetaOneMulEquiv (h : H) : Multiplicative D ≃ Multiplicative D

The multiplicative reindexing form used by the group Hilbert space. Paper: §3.

Equations

• Connes.PaperQuotientAction.paperThetaOneMulEquiv h = (Connes.Construction.PaperKernel.additiveEquivToMulAut (Connes.Construction.PaperKernel.paperThetaOneLinearHom h)).toEquiv

noncomputable def Connes.PaperQuotientAction.paperThetaTwoMulEquiv (h : H) : Multiplicative D ≃ Multiplicative D

The second quotient has the analogous multiplicative reindexing. Paper: §3.

Equations

• Connes.PaperQuotientAction.paperThetaTwoMulEquiv h = (Connes.Construction.PaperKernel.additiveEquivToMulAut (Connes.Construction.PaperKernel.paperThetaTwoLinearHom h)).toEquiv

@[simp]

theorem Connes.PaperQuotientAction.paperThetaOneMulEquiv_ofAdd (h : H) (d : D) : (paperThetaOneMulEquiv h) (Multiplicative.ofAdd d) = Multiplicative.ofAdd ((Construction.PaperKernel.paperThetaOneLinearHom h) d)

@[simp]

theorem Connes.PaperQuotientAction.paperThetaTwoMulEquiv_ofAdd (h : H) (d : D) : (paperThetaTwoMulEquiv h) (Multiplicative.ofAdd d) = Multiplicative.ofAdd ((Construction.PaperKernel.paperThetaTwoLinearHom h) d)

theorem Connes.PaperQuotientAction.coordinateComplexCharacter_actionOne (h : H) (d : D) (p : Coordinates) : (PaperCrossedKernel.coordinateComplexCharacter d) ((PaperDualActions.paperCoordinateActionOne h⁻¹) p) = (PaperCrossedKernel.coordinateComplexCharacter ((Construction.PaperKernel.paperThetaOneLinearHom h) d)) p

theorem Connes.PaperQuotientAction.coordinateComplexCharacter_actionTwo (h : H) (d : D) (p : Coordinates) : (PaperCrossedKernel.coordinateComplexCharacter d) ((PaperDualActions.paperCoordinateActionTwo h⁻¹) p) = (PaperCrossedKernel.coordinateComplexCharacter ((Construction.PaperKernel.paperThetaTwoLinearHom h) d)) p

theorem Connes.PaperQuotientAction.coordinateCharacterL2_apply_ae (d : D) : ↑↑(PaperFourierCoordinates.coordinateCharacterL2 d) =ᵐ[PaperDualTopology.coordinatesHaar] ⇑(PaperCrossedKernel.coordinateComplexCharacter d)

theorem Connes.PaperQuotientAction.coordinateCharacterL2_actionOne (h : H) (d : D) : (CrossedProduct.crossedActionL2Equiv PaperCrossedHaar.paperHaarActionOne h) (PaperFourierCoordinates.coordinateCharacterL2 d) = PaperFourierCoordinates.coordinateCharacterL2 ((Construction.PaperKernel.paperThetaOneLinearHom h) d)

theorem Connes.PaperQuotientAction.coordinateCharacterL2_actionTwo (h : H) (d : D) : (CrossedProduct.crossedActionL2Equiv PaperCrossedHaar.paperHaarActionTwo h) (PaperFourierCoordinates.coordinateCharacterL2 d) = PaperFourierCoordinates.coordinateCharacterL2 ((Construction.PaperKernel.paperThetaTwoLinearHom h) d)

theorem Connes.PaperQuotientAction.paperFourierCoordinate_actionOne_comp (h : H) (ξ : ↥KernelL2) : PaperFourierCoordinates.paperFourierCoordinateUnitary ((l2Reindex (paperThetaOneMulEquiv h)) ξ) = (CrossedProduct.crossedActionL2Equiv PaperCrossedHaar.paperHaarActionOne h) (PaperFourierCoordinates.paperFourierCoordinateUnitary ξ)

theorem Connes.PaperQuotientAction.paperFourierCoordinate_actionTwo_comp (h : H) (ξ : ↥KernelL2) : PaperFourierCoordinates.paperFourierCoordinateUnitary ((l2Reindex (paperThetaTwoMulEquiv h)) ξ) = (CrossedProduct.crossedActionL2Equiv PaperCrossedHaar.paperHaarActionTwo h) (PaperFourierCoordinates.paperFourierCoordinateUnitary ξ)