The factor witness component of the Connes rigidity formalization.

structure Connes.FactorWitness.SpatialWitness (G : CountableDiscreteGroup) (H : CountableDiscreteGroup) : Type (max u_1 u_2)

Spatial witness data for a factor equivalence. Paper: §3.

• unitary : ↥(GroupL2 G.Carrier) ≃ₗᵢ[ℂ] ↥(GroupL2 H.Carrier)

  The unitary component of SpatialWitness.

• maps_group_factor (T : ↥(GroupL2 G.Carrier) →L[ℂ] ↥(GroupL2 G.Carrier)) : T ∈ groupVonNeumannAlgebra G ↔ self.unitary.conjStarAlgEquiv T ∈ groupVonNeumannAlgebra H
• maps_vacuum : self.unitary (delta G 1) = delta H 1

noncomputable def Connes.FactorWitness.SpatialWitness.toStarAlgEquiv {G : CountableDiscreteGroup} {H : CountableDiscreteGroup} (w : SpatialWitness G H) : ↥(GroupVonNeumannAlgebra G) ≃⋆ₐ[ℂ] ↥(GroupVonNeumannAlgebra H)

Turn a spatial witness into its conjugation star-algebra equivalence. Paper: §3.

Equations

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

theorem Connes.FactorWitness.SpatialWitness.trace_preserving {G : CountableDiscreteGroup} {H : CountableDiscreteGroup} (w : SpatialWitness G H) (x : ↥(GroupVonNeumannAlgebra G)) : canonicalTrace H (w.toStarAlgEquiv x) = canonicalTrace G x

The spatial witness preserves the canonical vacuum trace. Paper: §3.

noncomputable def Connes.FactorWitness.SpatialWitness.toTracialGroupFactorEquiv {G : CountableDiscreteGroup} {H : CountableDiscreteGroup} (w : SpatialWitness G H) : TracialGroupFactorEquiv G H

Package the spatial witness as a trace-preserving factor equivalence. Paper: §3.

Equations

• w.toTracialGroupFactorEquiv = { toStarAlgEquiv := w.toStarAlgEquiv, normal := ⋯, trace_preserving := ⋯ }

theorem Connes.FactorWitness.tracialEquiv_of_spatialWitness {G : CountableDiscreteGroup} {H : CountableDiscreteGroup} (w : SpatialWitness G H) : TracialGroupFactorsIsomorphic G H

Spatial-to-tracial transfer. Paper: §3.