Factor equivalence and infinite Connes-rigidity family

@[instance_reducible]

noncomputable def ConnesRigidity.gammaDualMeasurable (n : ℕ) : MeasurableSpace (DiscreteCharacterSpace (E n))

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.gammaDualMeasurable n = borel (ConnesRigidity.DiscreteCharacterSpace (ConnesRigidity.E n))

theorem ConnesRigidity.gammaDualBorel (n : ℕ) : BorelSpace (DiscreteCharacterSpace (E n))

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.gammaKernelDecidableEq (n : ℕ) : DecidableEq (E n)

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.gammaKernelDecidableEq n = Classical.decEq (ConnesRigidity.E n)

@[instance_reducible]

noncomputable def ConnesRigidity.gammaCircleMeasurable : MeasurableSpace Circle

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.gammaCircleMeasurable = borel Circle

theorem ConnesRigidity.gammaCircleBorel : BorelSpace Circle

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.dualProductMeasurable : MeasurableSpace (X × Y)

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.dualProductMeasurable = borel (ConnesRigidity.X × ConnesRigidity.Y)

theorem ConnesRigidity.dualProductBorel : BorelSpace (X × Y)

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.gammaDetectionDualMeasurable (n : ℕ) : MeasurableSpace (DiscreteCharacterSpace (E n))

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.gammaDetectionDualMeasurable n = borel (ConnesRigidity.DiscreteCharacterSpace (ConnesRigidity.E n))

theorem ConnesRigidity.gammaDetectionDualBorel (n : ℕ) : BorelSpace (DiscreteCharacterSpace (E n))

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.gammaDetectionPairMeasurable : MeasurableSpace (X × Y)

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.gammaDetectionPairMeasurable = borel (ConnesRigidity.X × ConnesRigidity.Y)

theorem ConnesRigidity.gammaDetectionPairBorel : BorelSpace (X × Y)

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.gammaDetectionKernelDecidableEq (n : ℕ) : DecidableEq (E n)

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.gammaDetectionKernelDecidableEq n = Classical.decEq (ConnesRigidity.E n)

@[instance_reducible]

def ConnesRigidity.spectralGapDiscreteTopology : TopologicalSpace D

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.spectralGapDiscreteTopology = ⊥

theorem ConnesRigidity.spectralGapDiscrete : DiscreteTopology D

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.spectralGapDualMeasurable : MeasurableSpace (DiscreteCharacterSpace D)

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.spectralGapDualMeasurable = borel (ConnesRigidity.DiscreteCharacterSpace ConnesRigidity.D)

theorem ConnesRigidity.spectralGapDualBorel : BorelSpace (DiscreteCharacterSpace D)

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.spectralGapPairMeasurable : MeasurableSpace (X × Y)

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.spectralGapPairMeasurable = borel (ConnesRigidity.X × ConnesRigidity.Y)

theorem ConnesRigidity.spectralGapPairBorel : BorelSpace (X × Y)

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

def ConnesRigidity.lambdaDiscreteTopology : TopologicalSpace D

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.lambdaDiscreteTopology = ⊥

theorem ConnesRigidity.lambdaDiscrete : DiscreteTopology D

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.lambdaDecidableEq : DecidableEq D

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.lambdaDecidableEq = Classical.decEq ConnesRigidity.D

@[instance_reducible]

noncomputable def ConnesRigidity.lambdaDualMeasurable : MeasurableSpace (DiscreteCharacterSpace D)

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.lambdaDualMeasurable = borel (ConnesRigidity.DiscreteCharacterSpace ConnesRigidity.D)

theorem ConnesRigidity.lambdaDualBorel : BorelSpace (DiscreteCharacterSpace D)

Cross-module support for the infinite Connes-rigidity construction.

@[instance_reducible]

noncomputable def ConnesRigidity.lambdaCircleMeasurable : MeasurableSpace Circle

Cross-module support for the infinite Connes-rigidity construction.

Equations

• ConnesRigidity.lambdaCircleMeasurable = borel Circle

theorem ConnesRigidity.lambdaCircleBorel : BorelSpace Circle

Cross-module support for the infinite Connes-rigidity construction.

theorem ConnesRigidity.exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors : ∃ (Λ : CountableDiscreteGroup) (Γ : ℕ → CountableDiscreteGroup), Group.FG Λ.Carrier ∧ (∀ (n : ℕ), Group.FG (Γ n).Carrier) ∧ IsICC Λ ∧ (∀ (n : ℕ), IsICC (Γ n)) ∧ HasKazhdanPropertyT Λ ∧ (∀ (n : ℕ), HasKazhdanPropertyT (Γ n)) ∧ (∀ (n : ℕ), TracialGroupFactorsIsomorphic (Γ n) Λ) ∧ (∀ (m n : ℕ), TracialGroupFactorsIsomorphic (Γ m) (Γ n)) ∧ (∀ ⦃m n : ℕ⦄, m ≠ n → ¬GroupsIsomorphic (Γ m) (Γ n)) ∧ ∀ (n : ℕ), ¬GroupsIsomorphic Λ (Γ n)

There are infinitely many pairwise nonisomorphic finitely generated ICC property-(T) groups whose tracial group factors are all isomorphic.

@[reducible, inline]

abbrev ConnesRigidity.infiniteConnesRigidity : ∃ (Λ : CountableDiscreteGroup) (Γ : ℕ → CountableDiscreteGroup), Group.FG Λ.Carrier ∧ (∀ (n : ℕ), Group.FG (Γ n).Carrier) ∧ IsICC Λ ∧ (∀ (n : ℕ), IsICC (Γ n)) ∧ HasKazhdanPropertyT Λ ∧ (∀ (n : ℕ), HasKazhdanPropertyT (Γ n)) ∧ (∀ (n : ℕ), TracialGroupFactorsIsomorphic (Γ n) Λ) ∧ (∀ (m n : ℕ), TracialGroupFactorsIsomorphic (Γ m) (Γ n)) ∧ (∀ ⦃m n : ℕ⦄, m ≠ n → ¬GroupsIsomorphic (Γ m) (Γ n)) ∧ ∀ (n : ℕ), ¬GroupsIsomorphic Λ (Γ n)

A short registry alias for the infinite Connes-rigidity counterexample theorem.

Equations

• ConnesRigidity.infiniteConnesRigidity = ConnesRigidity.exists_infinite_pairwise_nonisomorphic_propertyT_icc_groups_with_isomorphic_factors