The core component of the Connes rigidity formalization.

structure Connes.CountableDiscreteGroup : Type (u + 1)

Countable discrete group carrier. Paper: §7.

• Carrier : Type u

  The Carrier component of CountableDiscreteGroup.

• group : Group self.Carrier
• countable : Countable self.Carrier

@[instance_reducible]

instance Connes.CountableDiscreteGroup.instCoeSortType : CoeSort CountableDiscreteGroup (Type u)

Coercion from the group wrapper to its carrier. Paper: §7.

Equations

• Connes.CountableDiscreteGroup.instCoeSortType = { coe := Connes.CountableDiscreteGroup.Carrier }

def Connes.IsICC (G : CountableDiscreteGroup) : Prop

ICC predicate boundary. Paper: §5.

Equations

• Connes.IsICC G = (Infinite G.Carrier ∧ ∀ (g : G.Carrier), g ≠ 1 → (conjugatesOf g).Infinite)

@[reducible, inline]

abbrev Connes.UnitaryRepresentation (G : Type u) [Group G] (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] : Type (max u v)

Unitary-representation carrier. Paper: §4.

Equations

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

def Connes.UnitaryRepresentation.IsInvariant {G : Type u} {H : Type v} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation G H) (ξ : H) : Prop

Invariant-vector predicate. Paper: §4.

Equations

• π.IsInvariant ξ = ∀ (g : G), ↑(π g) ξ = ξ

def Connes.UnitaryRepresentation.HasAlmostInvariantUnitVectors {G : Type u} {H : Type v} [Group G] [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : UnitaryRepresentation G H) : Prop

Almost-invariant-vector predicate. Paper: §4.

Equations

• π.HasAlmostInvariantUnitVectors = ∀ (K : Finset G) (ε : ℝ), 0 < ε → ∃ (ξ : H), ‖ξ‖ = 1 ∧ ∀ g ∈ K, ‖↑(π g) ξ - ξ‖ < ε

def Connes.HasKazhdanPropertyT (G : CountableDiscreteGroup) : Prop

Property-(T), universe-polymorphic in the representation carrier so concrete Type 0 groups are not restricted to Type 0 Hilbert spaces. Paper: §4.

Equations

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

def Connes.HasRelativePropertyT (G : CountableDiscreteGroup) (N : Subgroup G.Carrier) : Prop

Relative property-(T), universe-polymorphic in the representation carrier so concrete Type 0 groups are not restricted to Type 0 Hilbert spaces. Paper: §4.

Equations

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

@[reducible, inline]

noncomputable abbrev Connes.GroupL2 (G : Type u) : AddSubgroup (PreLp fun (x : G) => ℂ)

Group-indexed Hilbert carrier. Paper: §3.

Equations

• Connes.GroupL2 G = lp (fun (x : G) => ℂ) 2

theorem Connes.memℓp_reindex {α : Type u} {β : Type v} {E : Type w} [NormedAddCommGroup E] {p : ENNReal} (e : α ≃ β) (hp : 0 < p.toReal) (f : ↥(lp (fun (x : α) => E) p)) : Memℓp (fun (j : β) => ↑f (e.symm j)) p

Reindexing an ℓp family along an equivalence preserves membership in ℓp.

def Connes.l2Reindex {α : Type u} {β : Type v} (e : α ≃ β) : ↥(GroupL2 α) ≃ₗᵢ[ℂ] ↥(GroupL2 β)

Reindexing equivalence for group-indexed Hilbert spaces. Paper: §3.

Equations

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

noncomputable def Connes.leftRegularUnitary {G : Type u} [Group G] (g : G) : ↥(unitary (↥(GroupL2 G) →L[ℂ] ↥(GroupL2 G)))

Left-regular unitary boundary. Paper: §3.

Equations

• Connes.leftRegularUnitary g = Unitary.linearIsometryEquiv.symm (Connes.l2Reindex (Equiv.mulLeft g))

noncomputable def Connes.leftRegularRepresentation (G : Type u) [Group G] : G →* ↥(unitary (↥(GroupL2 G) →L[ℂ] ↥(GroupL2 G)))

Left-regular representation boundary. Paper: §3.

Equations

• Connes.leftRegularRepresentation G = { toFun := Connes.leftRegularUnitary, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def Connes.vonNeumannClosure {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) : VonNeumannAlgebra H

Bicommutant presentation of the von Neumann closure boundary. Paper: §3.

Equations

• Connes.vonNeumannClosure S = (let __StarSubalgebra := StarSubalgebra.centralizer ℂ S; { toStarSubalgebra := __StarSubalgebra, centralizer_centralizer' := ⋯ }).commutant

@[simp]

theorem Connes.coe_vonNeumannClosure {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (S : Set (H →L[ℂ] H)) : ↑(vonNeumannClosure S) = ↑(StarSubalgebra.centralizer ℂ ↑(StarSubalgebra.centralizer ℂ S))

The von Neumann closure has the expected bicommutant carrier.

@[simp]

theorem Connes.mem_vonNeumannClosure {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {S : Set (H →L[ℂ] H)} {x : H →L[ℂ] H} : x ∈ vonNeumannClosure S ↔ x ∈ StarSubalgebra.centralizer ℂ ↑(StarSubalgebra.centralizer ℂ S)

Membership in the von Neumann closure is membership in the star-algebraic bicommutant of the generating set.

noncomputable def Connes.groupVonNeumannAlgebra (G : CountableDiscreteGroup) : VonNeumannAlgebra ↥(GroupL2 G.Carrier)

Group von Neumann algebra boundary. Paper: §3.

Equations

• Connes.groupVonNeumannAlgebra G = Connes.vonNeumannClosure (Set.range fun (g : G.Carrier) => ↑((Connes.leftRegularRepresentation G.Carrier) g))

@[reducible, inline]

noncomputable abbrev Connes.GroupVonNeumannAlgebra (G : CountableDiscreteGroup) : StarSubalgebra ℂ (↥(GroupL2 G.Carrier) →L[ℂ] ↥(GroupL2 G.Carrier))

Group von Neumann algebra carrier. Paper: §3.

Equations

• Connes.GroupVonNeumannAlgebra G = (Connes.groupVonNeumannAlgebra G).toStarSubalgebra

noncomputable def Connes.delta (G : CountableDiscreteGroup) (g : G.Carrier) : ↥(GroupL2 G.Carrier)

Point-mass basis vector boundary. Paper: §3.

Equations

• Connes.delta G g = lp.single 2 g 1

noncomputable def Connes.canonicalTrace (G : CountableDiscreteGroup) : ↥(GroupVonNeumannAlgebra G) → ℂ

Canonical trace boundary. Paper: §3.

Equations

• Connes.canonicalTrace G x = inner ℂ (Connes.delta G 1) (↑x (Connes.delta G 1))

def Connes.IsProjectionSupremum {A : Type u} [Mul A] [Star A] [LE A] (S : Set A) (p : A) : Prop

Projection-supremum predicate boundary. Leastness is among projection upper bounds, not all ambient upper bounds as in IsLUB. Paper: §3.

Equations

• Connes.IsProjectionSupremum S p = (IsStarProjection p ∧ (∀ q ∈ S, IsStarProjection q ∧ q ≤ p) ∧ ∀ (r : A), IsStarProjection r → (∀ q ∈ S, q ≤ r) → p ≤ r)

theorem Connes.IsProjectionSupremum.intro {A : Type u} [Mul A] [Star A] [LE A] {S : Set A} {p : A} (hp : IsStarProjection p) (hupper : ∀ q ∈ S, IsStarProjection q ∧ q ≤ p) (hleast : ∀ (r : A), IsStarProjection r → (∀ q ∈ S, q ≤ r) → p ≤ r) : IsProjectionSupremum S p

Construct a projection supremum from its projection, upper-bound, and leastness clauses.

theorem Connes.IsProjectionSupremum.isStarProjection {A : Type u} [Mul A] [Star A] [LE A] {S : Set A} {p : A} (h : IsProjectionSupremum S p) : IsStarProjection p

The supremum candidate is a projection.

theorem Connes.IsProjectionSupremum.upper {A : Type u} [Mul A] [Star A] [LE A] {S : Set A} {p q : A} (h : IsProjectionSupremum S p) (hq : q ∈ S) : IsStarProjection q ∧ q ≤ p

Every member is a projection below the supremum candidate.

theorem Connes.IsProjectionSupremum.least {A : Type u} [Mul A] [Star A] [LE A] {S : Set A} {p r : A} (h : IsProjectionSupremum S p) (hr : IsStarProjection r) (hupper : ∀ q ∈ S, q ≤ r) : p ≤ r

The supremum candidate lies below every projection upper bound.

theorem Connes.IsProjectionSupremum.unique {A : Type u} [Mul A] [Star A] [LE A] [Std.Antisymm fun (a b : A) => a ≤ b] {S : Set A} {p q : A} (hp : IsProjectionSupremum S p) (hq : IsProjectionSupremum S q) : p = q

Projection suprema are unique.

def Connes.IsNormalStarAlgEquiv {A : Type u} {B : Type v} [Add A] [Mul A] [SMul ℂ A] [Star A] [LE A] [Add B] [Mul B] [SMul ℂ B] [Star B] [LE B] (e : A ≃⋆ₐ[ℂ] B) : Prop

Preservation of projection suprema by a star-algebra equivalence and its inverse, relative to the supplied order relations. Paper: §3.

Equations

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

theorem Connes.IsNormalStarAlgEquiv.intro {A : Type u} {B : Type v} [Add A] [Mul A] [SMul ℂ A] [Star A] [LE A] [Add B] [Mul B] [SMul ℂ B] [Star B] [LE B] {e : A ≃⋆ₐ[ℂ] B} (hmap : ∀ (S : Set A) (p : A), IsProjectionSupremum S p → IsProjectionSupremum (⇑e '' S) (e p)) (hsymm_map : ∀ (S : Set B) (p : B), IsProjectionSupremum S p → IsProjectionSupremum (⇑e.symm '' S) (e.symm p)) : IsNormalStarAlgEquiv e

Construct normality from projection-supremum transport in both directions.

theorem Connes.IsNormalStarAlgEquiv.map {A : Type u} {B : Type v} [Add A] [Mul A] [SMul ℂ A] [Star A] [LE A] [Add B] [Mul B] [SMul ℂ B] [Star B] [LE B] {e : A ≃⋆ₐ[ℂ] B} (h : IsNormalStarAlgEquiv e) {S : Set A} {p : A} (hp : IsProjectionSupremum S p) : IsProjectionSupremum (⇑e '' S) (e p)

A normal star-algebra equivalence preserves projection suprema.

theorem Connes.IsNormalStarAlgEquiv.symm_map {A : Type u} {B : Type v} [Add A] [Mul A] [SMul ℂ A] [Star A] [LE A] [Add B] [Mul B] [SMul ℂ B] [Star B] [LE B] {e : A ≃⋆ₐ[ℂ] B} (h : IsNormalStarAlgEquiv e) {S : Set B} {p : B} (hp : IsProjectionSupremum S p) : IsProjectionSupremum (⇑e.symm '' S) (e.symm p)

The inverse of a normal star-algebra equivalence preserves projection suprema.

theorem Connes.IsNormalStarAlgEquiv.refl {A : Type u} [Add A] [Mul A] [SMul ℂ A] [Star A] [LE A] : IsNormalStarAlgEquiv (StarAlgEquiv.refl ℂ A)

The identity star-algebra equivalence is normal.

theorem Connes.IsNormalStarAlgEquiv.symm {A : Type u} {B : Type v} [Add A] [Mul A] [SMul ℂ A] [Star A] [LE A] [Add B] [Mul B] [SMul ℂ B] [Star B] [LE B] {e : A ≃⋆ₐ[ℂ] B} (h : IsNormalStarAlgEquiv e) : IsNormalStarAlgEquiv e.symm

The inverse of a normal star-algebra equivalence is normal.

theorem Connes.IsNormalStarAlgEquiv.trans {A : Type u} {B : Type v} [Add A] [Mul A] [SMul ℂ A] [Star A] [LE A] [Add B] [Mul B] [SMul ℂ B] [Star B] [LE B] {C : Type u_1} [Add C] [Mul C] [SMul ℂ C] [Star C] [LE C] {e : A ≃⋆ₐ[ℂ] B} {f : B ≃⋆ₐ[ℂ] C} (he : IsNormalStarAlgEquiv e) (hf : IsNormalStarAlgEquiv f) : IsNormalStarAlgEquiv (e.trans f)

A composite of normal star-algebra equivalences is normal.

structure Connes.TracialGroupFactorEquiv (G : CountableDiscreteGroup) (H : CountableDiscreteGroup) : Type (max u v)

Trace-preserving factor-equivalence witness. Paper: §3.

• toStarAlgEquiv : ↥(GroupVonNeumannAlgebra G) ≃⋆ₐ[ℂ] ↥(GroupVonNeumannAlgebra H)

  The toStarAlgEquiv component of TracialGroupFactorEquiv.

• normal : IsNormalStarAlgEquiv self.toStarAlgEquiv
• trace_preserving (x : ↥(GroupVonNeumannAlgebra G)) : canonicalTrace H (self.toStarAlgEquiv x) = canonicalTrace G x

def Connes.TracialGroupFactorsIsomorphic (G : CountableDiscreteGroup) (H : CountableDiscreteGroup) : Prop

Trace-preserving factor-isomorphism predicate. Paper: §3.

Equations

• Connes.TracialGroupFactorsIsomorphic G H = Nonempty (Connes.TracialGroupFactorEquiv G H)