The spectral property t component of the Connes rigidity formalization.

@[instance_reducible]

noncomputable instance Connes.PaperSpectralPropertyT.paperRawCharacterMeasurableSpace : MeasurableSpace (DiscreteCharacterSpace Construction.PaperKernel.D)

Borel structure on the raw compact character carrier used by §4. Paper: §4.

Equations

• Connes.PaperSpectralPropertyT.paperRawCharacterMeasurableSpace = borel (Connes.DiscreteCharacterSpace Connes.Construction.PaperKernel.D)

instance Connes.PaperSpectralPropertyT.paperRawCharacterBorelSpace : BorelSpace (DiscreteCharacterSpace Construction.PaperKernel.D)

The raw compact character carrier is a Borel space. Paper: §4.

instance Connes.PaperSpectralPropertyT.paperRawCharacterMeasurableSingletonClass : MeasurableSingletonClass (DiscreteCharacterSpace Construction.PaperKernel.D)

Singletons are measurable in the paper's compact character space. Paper: §4.

@[reducible, inline]

noncomputable abbrev Connes.PaperSpectralPropertyT.lambdaOneExtension : SplitAbelianExtension Construction.PaperKernel.D PaperPropertyT.lambdaOne SpecialLinear.sl3Group

The first actual split extension used by the spectral argument. Paper: §4.

Equations

• Connes.PaperSpectralPropertyT.lambdaOneExtension = Connes.PaperSplitExtensions.lambdaExtension Connes.Construction.PaperKernel.paperThetaOneHom

@[reducible, inline]

noncomputable abbrev Connes.PaperSpectralPropertyT.lambdaTwoExtension : SplitAbelianExtension Construction.PaperKernel.D PaperPropertyT.lambdaTwo SpecialLinear.sl3Group

The second actual split extension used by the spectral argument. Paper: §4.

Equations

• Connes.PaperSpectralPropertyT.lambdaTwoExtension = Connes.PaperSplitExtensions.lambdaExtension Connes.Construction.PaperKernel.paperThetaTwoHom

structure Connes.PaperSpectralPropertyT.SpectralData (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) : Type

Spectral data for the intermediate group associated to an action. Paper: §4.

• J : Finset Construction.PaperKernel.D

  The J component of SpectralData.

• c : ℝ

  The c component of SpectralData.

• c_pos : 0 < self.c
• detection : HasFiniteSpectralDetection (PaperSplitExtensions.lambdaExtension action) self.J self.c

theorem Connes.PaperSpectralPropertyT.lambda_propertyT_of_spectralData (input : PaperPropertyT.EJZKInput) (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) (data : SpectralData action) : HasKazhdanPropertyT (PaperPropertyT.lambdaOf action)

The intermediate group of an action is property-(T) from spectral data. Paper: §4.

theorem Connes.PaperSpectralPropertyT.gamma_propertyT_of_spectralData (input : PaperPropertyT.EJZKInput) (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) (data : SpectralData action) : HasKazhdanPropertyT (Construction.PaperKernel.paperGammaOf action)

The full semidirect group of an action is property-(T) from spectral data. Paper: §4.

theorem Connes.PaperSpectralPropertyT.completion_of_spectralData (input : PaperPropertyT.EJZKInput) (dataOne : SpectralData Construction.PaperKernel.paperThetaOneHom) (dataTwo : SpectralData Construction.PaperKernel.paperThetaTwoHom) : HasKazhdanPropertyT Construction.PaperKernel.paperGammaOne ∧ HasKazhdanPropertyT Construction.PaperKernel.paperGammaTwo

Both concrete Zhou groups have property-(T) from the two spectral inputs. Paper: §4.