The property t transfer component of the Connes rigidity formalization.

noncomputable def Connes.CountableDiscreteGroup.quotient (G : CountableDiscreteGroup) (N : Subgroup G.Carrier) (hN : N.Normal) : CountableDiscreteGroup

The quotient construction used in the Connes rigidity formalization.

Equations

• G.quotient N hN = { Carrier := G.Carrier ⧸ N, group := inferInstance, countable := ⋯ }

structure Connes.PropertyTTransfer.FiniteExtensionData (L G Q : CountableDiscreteGroup) : Type u

The finite extension in Zhou Proposition 4.8, before applying Lemma 4.7.

• subgroup : Subgroup G.Carrier

  The subgroup component of FiniteExtensionData.

• normal : self.subgroup.Normal
• finiteIndex : self.subgroup.FiniteIndex
• subgroupEquiv : L.Carrier ≃* (OpenAIPort.CountableDiscreteGroup.subgroup G self.subgroup).Carrier

  The subgroupEquiv component of FiniteExtensionData.

• quotientEquiv : (G.quotient self.subgroup ⋯).Carrier ≃* Q.Carrier

  The quotientEquiv component of FiniteExtensionData.

theorem Connes.PropertyTTransfer.relativePropertyT_of_subgroupEquiv (L G : CountableDiscreteGroup) (N : Subgroup G.Carrier) (e : L.Carrier ≃* (OpenAIPort.CountableDiscreteGroup.subgroup G N).Carrier) (hL : HasKazhdanPropertyT L) : HasRelativePropertyT G N

theorem Connes.PropertyTTransfer.normalFixedQuotient_hasAlmostInvariantUnitVectors (G : CountableDiscreteGroup) (N : Subgroup G.Carrier) [N.Normal] (hrelative : HasRelativePropertyT G N) {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (π : UnitaryRepresentation G.Carrier K) (hπ : π.HasAlmostInvariantUnitVectors) : (normalFixedQuotientRepresentation N π).HasAlmostInvariantUnitVectors

theorem Connes.PropertyTTransfer.hasKazhdanPropertyT_of_relative_and_quotient (G : CountableDiscreteGroup) (N : Subgroup G.Carrier) (hN : N.Normal) (hrelative : HasRelativePropertyT G N) (hquotient : HasKazhdanPropertyT (G.quotient N hN)) : HasKazhdanPropertyT G

theorem Connes.PropertyTTransfer.hasKazhdanPropertyT_of_finiteExtension {L G Q : CountableDiscreteGroup} (data : FiniteExtensionData L G Q) (hL : HasKazhdanPropertyT L) (hQ : HasKazhdanPropertyT Q) : HasKazhdanPropertyT G