Property-(T) transfer for Zhou §4 on the concrete tensor-kernel groups.

noncomputable def Connes.PaperPropertyT.elementaryGroup : CountableDiscreteGroup

The elementary subgroup appearing in the cited EJZK theorem. Paper: §4.

Equations

• Connes.PaperPropertyT.elementaryGroup = { Carrier := ↥Connes.SpecialLinear.elementarySubgroup, group := inferInstance, countable := Connes.PaperPropertyT.elementaryGroup._proof_1 }

noncomputable def Connes.PaperPropertyT.elementaryEquivSL3 : ↥SpecialLinear.elementarySubgroup ≃* SpecialLinear.SL3

Zhou Proposition 4.1(a) identifies the elementary group with SL₃(R). Paper: §4.

Equations

• Connes.PaperPropertyT.elementaryEquivSL3 = (MulEquiv.subgroupCongr Connes.SpecialLinear.elementarySubgroup_eq_top).trans Subgroup.topEquiv

structure Connes.PaperPropertyT.EJZKInput : Prop

The external EJZK property-(T) input used by Zhou §4. Paper: §4, Proposition 4.1(b).

• propertyT : HasKazhdanPropertyT elementaryGroup

theorem Connes.PaperPropertyT.sl3_propertyT_from_EJZK (input : EJZKInput) : HasKazhdanPropertyT SpecialLinear.sl3Group

Transport the cited elementary-group theorem across Zhou Proposition 4.1(a). Paper: §4.

def Connes.PaperPropertyT.sl3ToActingGroup : SpecialLinear.SL3 →* Construction.H

Inclusion of the SL₃ factor into the actual acting group. Paper: §4.

Equations

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

@[simp]

theorem Connes.PaperPropertyT.sl3ToActingGroup_apply (g : SpecialLinear.SL3) : sl3ToActingGroup g = (g, 1)

Pointwise form of the standard inclusion of the SL₃ factor. Paper: §4.

noncomputable def Connes.PaperPropertyT.finiteSymplecticGroup : CountableDiscreteGroup

The finite quotient in Zhou Proposition 4.8. Paper: §4.

Equations

• Connes.PaperPropertyT.finiteSymplecticGroup = { Carrier := ↥Connes.Construction.PaperKernel.Q, group := inferInstance, countable := Connes.PaperPropertyT.finiteSymplecticGroup._proof_1 }

@[reducible, inline]

abbrev Connes.PaperPropertyT.lambdaCarrier (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) : Type

Carrier of the SL₃ intermediate group associated to an action. Paper: §4.

Equations

• Connes.PaperPropertyT.lambdaCarrier action = (Multiplicative Connes.Construction.PaperKernel.D ⋊[action.comp Connes.PaperPropertyT.sl3ToActingGroup] Connes.SpecialLinear.SL3)

@[reducible, inline]

noncomputable abbrev Connes.PaperPropertyT.lambdaOf (action : Construction.H →* MulAut (Multiplicative Construction.PaperKernel.D)) : CountableDiscreteGroup

Countable wrapper for the SL₃ intermediate group of an action. Paper: §4.

Equations

• Connes.PaperPropertyT.lambdaOf action = { Carrier := Connes.PaperPropertyT.lambdaCarrier action, group := SemidirectProduct.instGroup, countable := ⋯ }

@[reducible, inline]

noncomputable abbrev Connes.PaperPropertyT.lambdaOne : CountableDiscreteGroup

Zhou's first concrete SL₃ intermediate group. Paper: §4.

Equations

• Connes.PaperPropertyT.lambdaOne = Connes.PaperPropertyT.lambdaOf Connes.Construction.PaperKernel.paperThetaOneHom

@[reducible, inline]

noncomputable abbrev Connes.PaperPropertyT.lambdaTwo : CountableDiscreteGroup

Zhou's second concrete SL₃ intermediate group. Paper: §4.

Equations

• Connes.PaperPropertyT.lambdaTwo = Connes.PaperPropertyT.lambdaOf Connes.Construction.PaperKernel.paperThetaTwoHom

theorem Connes.PaperPropertyT.finiteSymplecticGroup_propertyT : HasKazhdanPropertyT finiteSymplecticGroup