The finite index component of the Connes rigidity formalization.

def Connes.OpenAIPort.CountableDiscreteGroup.subgroup (G : CountableDiscreteGroup) (S : Subgroup G.Carrier) : CountableDiscreteGroup

Countable discrete subgroup wrapper. Paper: §4.

Equations

• Connes.OpenAIPort.CountableDiscreteGroup.subgroup G S = { Carrier := ↥S, group := inferInstance, countable := ⋯ }

noncomputable def Connes.OpenAIPort.FiniteIndex.correction {G : Type u} [Group G] (S : Subgroup G) (g : G) (q : G ⧸ S) : ↥S

Correction element for the finite-index induced representation. Paper: §4.

Equations

• Connes.OpenAIPort.FiniteIndex.correction S g q = ⟨(Quotient.out (g • q))⁻¹ * g * Quotient.out q, ⋯⟩

@[simp]

theorem Connes.OpenAIPort.FiniteIndex.correction_coe {G : Type u} [Group G] (S : Subgroup G) (g : G) (q : G ⧸ S) : ↑(correction S g q) = (Quotient.out (g • q))⁻¹ * g * Quotient.out q

Pointwise formula for the correction element. Paper: §4.

theorem Connes.OpenAIPort.FiniteIndex.correction_mul {G : Type u} [Group G] (S : Subgroup G) (g h : G) (q : G ⧸ S) : correction S (g * h) q = correction S g (h • q) * correction S h q

Multiplicativity of the correction cocycle. Paper: §4.

@[simp]

theorem Connes.OpenAIPort.FiniteIndex.correction_one {G : Type u} [Group G] (S : Subgroup G) (q : G ⧸ S) : correction S 1 q = 1

Unit value of the correction cocycle. Paper: §4.

theorem Connes.OpenAIPort.FiniteIndex.subgroup_smul_baseCoset {G : Type u} [Group G] (S : Subgroup G) (s : ↥S) : ↑s • ↑1 = ↑1

The subgroup fixes the base coset. Paper: §4.

theorem Connes.OpenAIPort.FiniteIndex.quotientOut_baseCoset_mem {G : Type u} [Group G] (S : Subgroup G) : Quotient.out ↑1 ∈ S

The chosen representative of the base coset lies in the subgroup. Paper: §4.

@[instance_reducible]

noncomputable def Connes.OpenAIPort.FiniteIndex.finiteIndexQuotientFintype {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] : Fintype (G ⧸ S)

The finiteIndexQuotientFintype construction used in the Connes rigidity formalization.

Equations

• Connes.OpenAIPort.FiniteIndex.finiteIndexQuotientFintype S = Subgroup.fintypeQuotientOfFiniteIndex

@[reducible, inline]

abbrev Connes.OpenAIPort.FiniteIndex.InducedSpace {G : Type u} [Group G] (S : Subgroup G) {H : Type v} : Type (max u v)

Hilbert space induced from a finite-index subgroup. Paper: §4.

Equations

• Connes.OpenAIPort.FiniteIndex.InducedSpace S = PiLp 2 fun (x : G ⧸ S) => H

noncomputable def Connes.OpenAIPort.FiniteIndex.inducedLinearIsometryEquiv {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) (g : G) : InducedSpace S ≃ₗᵢ[ℂ] InducedSpace S

Linear-isometric action on the induced Hilbert space. Paper: §4.

Equations

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

@[simp]

theorem Connes.OpenAIPort.FiniteIndex.inducedLinearIsometryEquiv_apply {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) (g : G) (ξ : InducedSpace S) (q : G ⧸ S) : ((inducedLinearIsometryEquiv S π g) ξ).ofLp q = ↑(π (correction S g (g⁻¹ • q))) (ξ.ofLp (g⁻¹ • q))

Pointwise formula for the induced linear isometry. Paper: §4.

noncomputable def Connes.OpenAIPort.FiniteIndex.inducedUnitary {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) (g : G) : ↥(unitary (InducedSpace S →L[ℂ] InducedSpace S))

Unitary wrapper for the induced linear isometry. Paper: §4.

Equations

• Connes.OpenAIPort.FiniteIndex.inducedUnitary S π g = Unitary.linearIsometryEquiv.symm (Connes.OpenAIPort.FiniteIndex.inducedLinearIsometryEquiv S π g)

@[simp]

theorem Connes.OpenAIPort.FiniteIndex.inducedUnitary_apply {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) (g : G) (ξ : InducedSpace S) (q : G ⧸ S) : (↑(inducedUnitary S π g) ξ).ofLp q = ↑(π (correction S g (g⁻¹ • q))) (ξ.ofLp (g⁻¹ • q))

Pointwise formula for the induced unitary. Paper: §4.

noncomputable def Connes.OpenAIPort.FiniteIndex.inducedRepresentation {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) : UnitaryRepresentation G (InducedSpace S)

Induced unitary representation of the ambient group. Paper: §4.

Equations

• Connes.OpenAIPort.FiniteIndex.inducedRepresentation S π = { toFun := Connes.OpenAIPort.FiniteIndex.inducedUnitary S π, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Connes.OpenAIPort.FiniteIndex.inducedRepresentation_apply {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) (g : G) (ξ : InducedSpace S) (q : G ⧸ S) : (↑((inducedRepresentation S π) g) ξ).ofLp q = ↑(π (correction S g (g⁻¹ • q))) (ξ.ofLp (g⁻¹ • q))

Pointwise formula for the induced representation. Paper: §4.

theorem Connes.OpenAIPort.FiniteIndex.inducedSpace_norm_le_sum_norm_apply {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] (ξ : InducedSpace S) : ‖ξ‖ ≤ ∑ q : G ⧸ S, ‖ξ.ofLp q‖

Sum-of-coordinate norm bound for the induced space. Paper: §4.

theorem Connes.OpenAIPort.FiniteIndex.inducedRepresentation_hasAlmostInvariantUnitVectors {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) (hπ : π.HasAlmostInvariantUnitVectors) : (inducedRepresentation S π).HasAlmostInvariantUnitVectors

Almost-invariant vectors lift through finite-index induction. Paper: §4.

theorem Connes.OpenAIPort.FiniteIndex.inducedInvariant_baseCoset_ne_zero {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) (η : InducedSpace S) (hη : η ≠ 0) (hinv : (inducedRepresentation S π).IsInvariant η) : η.ofLp ↑1 ≠ 0

A nonzero invariant induced vector is nonzero at the base coset. Paper: §4.

theorem Connes.OpenAIPort.FiniteIndex.correction_conjugate_at_baseCoset {G : Type u} [Group G] (S : Subgroup G) (s : ↥S) : have r := ⟨Quotient.out ↑1, ⋯⟩; correction S ↑(r * s * r⁻¹) ↑1 = s

Correction conjugacy at the base coset. Paper: §4.

theorem Connes.OpenAIPort.FiniteIndex.inducedInvariant_baseCoset_isInvariant {G : Type u} [Group G] (S : Subgroup G) [S.FiniteIndex] {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation (↥S) H) (η : InducedSpace S) (hinv : (inducedRepresentation S π).IsInvariant η) : π.IsInvariant (η.ofLp ↑1)

Invariant induced vectors restrict to invariant subgroup vectors. Paper: §4.

theorem Connes.OpenAIPort.hasKazhdanPropertyT_subgroup_of_finiteIndex (G : CountableDiscreteGroup) (S : Subgroup G.Carrier) [S.FiniteIndex] (hG : HasKazhdanPropertyT G) : HasKazhdanPropertyT (CountableDiscreteGroup.subgroup G S)

Property-(T) descends to a finite-index subgroup. Paper: §4.