The finite property t component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.PropertyTTransfer.UnitaryRep (G : Type u_1) (H : Type u_2) [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Type (max u_1 u_2)

The UnitaryRep construction used in the Connes rigidity formalization.

Equations

• Connes.PropertyTTransfer.UnitaryRep G H = (G →* ↥(unitary (H →L[ℂ] H)))

noncomputable def Connes.PropertyTTransfer.unitaryToModuleRepresentation {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRep G H) : Representation ℂ G H

The linear representation underlying a unitary representation. Paper: §4.

Equations

• Connes.PropertyTTransfer.unitaryToModuleRepresentation π = { toFun := fun (g : G) => ↑↑(π g), map_one' := ⋯, map_mul' := ⋯ }

theorem Connes.PropertyTTransfer.averageMap_apply {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Fintype G] (π : UnitaryRep G H) (ξ : H) : (unitaryToModuleRepresentation π).averageMap ξ = (↑(Fintype.card G))⁻¹ • ∑ g : G, ↑(π g) ξ

theorem Connes.PropertyTTransfer.averageMap_sub_apply {G : Type u_1} {H : Type u_2} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [Fintype G] (π : UnitaryRep G H) (ξ : H) : (unitaryToModuleRepresentation π).averageMap ξ - ξ = (↑(Fintype.card G))⁻¹ • ∑ g : G, (↑(π g) ξ - ξ)

theorem Connes.PropertyTTransfer.hasKazhdanPropertyT_of_fintype (G : CountableDiscreteGroup) [Finite G.Carrier] : HasKazhdanPropertyT G