Concrete group construction and ICC certificates

@[instance_reducible]

noncomputable def ConnesRigidity.integerDualMeasurableSpace : MeasurableSpace (DiscreteCharacterSpace (Fin 2 → ℤ))

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

Equations

• ConnesRigidity.integerDualMeasurableSpace = borel (ConnesRigidity.DiscreteCharacterSpace (Fin 2 → ℤ))

theorem ConnesRigidity.integerDualBorelSpace : BorelSpace (DiscreteCharacterSpace (Fin 2 → ℤ))

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

@[instance_reducible]

noncomputable def ConnesRigidity.integerAtomDualMeasurable : MeasurableSpace (DiscreteCharacterSpace (Fin 2 → ℤ))

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

Equations

• ConnesRigidity.integerAtomDualMeasurable = borel (ConnesRigidity.DiscreteCharacterSpace (Fin 2 → ℤ))

theorem ConnesRigidity.integerAtomDualBorel : BorelSpace (DiscreteCharacterSpace (Fin 2 → ℤ))

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

theorem ConnesRigidity.universalLatticePropertyT_of_suslinRelative (hSuslinRelative : SuslinRelativeElementaryGeneration) : ErshovJaikinUniversalLatticePropertyT

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

theorem ConnesRigidity.suslinRelativeElementaryGeneration : SuslinRelativeElementaryGeneration

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

theorem ConnesRigidity.conj_mem_vonNeumannClosure_image_iff {H : Type u_1} {K : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (e : H ≃ₗᵢ[ℂ] K) (S : Set (H →L[ℂ] H)) (T : H →L[ℂ] H) : e.conjStarAlgEquiv T ∈ vonNeumannClosure (⇑e.conjStarAlgEquiv '' S) ↔ T ∈ vonNeumannClosure S

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

theorem ConnesRigidity.starAlgEquiv_isNormal {A : Type u} {B : Type v} [Semiring A] [StarRing A] [Algebra ℂ A] [Semiring B] [StarRing B] [Algebra ℂ B] (e : A ≃⋆ₐ[ℂ] B) : IsNormalStarAlgEquiv e

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

theorem ConnesRigidity.crossedHaarHilbertEquiv_mem_algebra_iff {Γ : Type u_1} [Group Γ] {Ω : Type u_2} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type u_3} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction Γ Ω} {Y : HaarProbabilityAction Γ Ξ} (e : EquivariantHaarEquiv X Y) (T : ↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X)) : T ∈ (crossedProductModel X).algebra ↔ (crossedHaarHilbertEquiv e).conjStarAlgEquiv T ∈ (crossedProductModel Y).algebra

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

theorem ConnesRigidity.DetectionGap.primitive_detecting_seventh {α : Type u_1} [DecidableEq α] (ambient primitive detecting : Finset α) (k : ℕ) (hprimitive_subset : primitive ⊆ ambient) (hdetecting_subset : detecting ⊆ ambient) (hambient : ambient.card = 8 * k) (hprimitive : primitive.card = 7 * k + 1) (hquarter : ambient.card ≤ 4 * detecting.card) : primitive.card ≤ 7 * (detecting ∩ primitive).card

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

theorem ConnesRigidity.DetectionGap.cube_card_eq_eight_mul_scale (N : ℕ) (hN : 0 < N) : 2 ^ (4 * N) = 8 * 2 ^ (4 * N - 3)

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

@[instance_reducible]

def ConnesRigidity.sourceDiscreteTopology : TopologicalSpace D

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

Equations

• ConnesRigidity.sourceDiscreteTopology = ⊥

theorem ConnesRigidity.sourceDiscrete : DiscreteTopology D

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

noncomputable def ConnesRigidity.binaryRootEquiv : F ≃ ↥(rootsOfUnity 2 Circle)

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

Equations

• ConnesRigidity.binaryRootEquiv = Equiv.ofBijective (⇑(ZMod.rootsOfUnityAddChar 2)) ConnesRigidity.binaryRootEquiv._proof_2

noncomputable def ConnesRigidity.circleBit (z : Circle) (hz : z ^ 2 = 1) : F

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

Equations

• ConnesRigidity.circleBit z hz = ConnesRigidity.binaryRootEquiv.symm (rootsOfUnity.mkOfPowEq z hz)

theorem ConnesRigidity.dualCharacter_square (χ : DiscreteCharacterSpace D) (d : D) : χ (Multiplicative.ofAdd d) ^ 2 = 1

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

noncomputable def ConnesRigidity.characterBit (χ : DiscreteCharacterSpace D) (d : D) : F

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

Equations

• ConnesRigidity.characterBit χ d = ConnesRigidity.circleBit (χ (Multiplicative.ofAdd d)) ⋯

theorem ConnesRigidity.characterBit_spec (χ : DiscreteCharacterSpace D) (d : D) : ZMod.toCircle (characterBit χ d) = χ (Multiplicative.ofAdd d)

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

theorem ConnesRigidity.characterBit_add (χ : DiscreteCharacterSpace D) (d₁ d₂ : D) : characterBit χ (d₁ + d₂) = characterBit χ d₁ + characterBit χ d₂

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

noncomputable def ConnesRigidity.characterBitLinear (χ : DiscreteCharacterSpace D) : D →ₗ[F] F

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

Equations

• ConnesRigidity.characterBitLinear χ = { toFun := ConnesRigidity.characterBit χ, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ConnesRigidity.dualToPair (χ : DiscreteCharacterSpace D) : X × Y

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

Equations

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

@[simp]

theorem ConnesRigidity.dualToPair_linear_apply (χ : DiscreteCharacterSpace D) (v : V) : (dualToPair χ).1 v = characterBit χ (v, 0)

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

@[simp]

theorem ConnesRigidity.dualToPair_quadratic_apply (χ : DiscreteCharacterSpace D) (b : ↥B) : (dualToPair χ).2 b = characterBit χ (0, b)

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

noncomputable def ConnesRigidity.pairToDual (z : X × Y) : DiscreteCharacterSpace D

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

Equations

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

theorem ConnesRigidity.pairToDual_linear_ne_one_iff (z : X × Y) (v : V) : (pairToDual z) (Multiplicative.ofAdd (v, 0)) ≠ 1 ↔ z.1 v ≠ 0

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

theorem ConnesRigidity.pairToDual_quadratic_ne_one_iff (z : X × Y) (b : ↥B) : (pairToDual z) (Multiplicative.ofAdd (0, b)) ≠ 1 ↔ z.2 b ≠ 0

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

@[simp]

theorem ConnesRigidity.dualToPair_pairToDual (z : X × Y) : dualToPair (pairToDual z) = z

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

@[simp]

theorem ConnesRigidity.pairToDual_dualToPair (χ : DiscreteCharacterSpace D) : pairToDual (dualToPair χ) = χ

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

noncomputable def ConnesRigidity.pairDualEquiv : X × Y ≃ DiscreteCharacterSpace D

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

Equations

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

theorem ConnesRigidity.pairToDual_continuous : Continuous pairToDual

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

noncomputable def ConnesRigidity.pairDualHomeomorph : X × Y ≃ₜ DiscreteCharacterSpace D

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

Equations

• ConnesRigidity.pairDualHomeomorph = ConnesRigidity.pairToDual_continuous.homeoOfEquivCompactToT2

noncomputable def ConnesRigidity.dualPairAction (k : ↥K) (z : X × Y) : X × Y

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

Equations

• ConnesRigidity.dualPairAction k z = (z.1 ∘ₗ ↑(ConnesRigidity.kLinear k⁻¹), z.2 ∘ₗ ↑(ConnesRigidity.kDividedSquareLinear k⁻¹))

noncomputable def ConnesRigidity.moduleAddAction : actingGroup.Carrier →* Multiplicative (AddAut D)

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

Equations

• ConnesRigidity.moduleAddAction = (MulAutMultiplicative ConnesRigidity.D).toMonoidHom.comp ConnesRigidity.kDAction

theorem ConnesRigidity.pairDualHomeomorph_equivariant (k : ↥K) (z : X × Y) : pairDualHomeomorph (dualPairAction k z) = dualCharacterAction moduleAddAction k (pairDualHomeomorph z)

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

theorem ConnesRigidity.pi₂_surjective : Function.Surjective ⇑pi₂

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

noncomputable def ConnesRigidity.dualCarryPullback (n : ℕ) : E 0 →+ E n

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

Equations

• ConnesRigidity.dualCarryPullback n = MonoidHom.toAdditive (PontryaginDual.map (ConnesRigidity.carryPullbackContinuous n)).toMonoidHom

theorem ConnesRigidity.dualCarryPullback_range_index (n : ℕ) : (dualCarryPullback n).range.index = 2 ^ (4 * n)

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

noncomputable def ConnesRigidity.gammaEmbedding (n : ℕ) : Gamma 0 →* Gamma n

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

Equations

• ConnesRigidity.gammaEmbedding n = SemidirectProduct.map (AddMonoidHom.toMultiplicative (ConnesRigidity.dualCarryPullback n)) (MonoidHom.id ↥ConnesRigidity.K) ⋯

theorem ConnesRigidity.gammaEmbedding_injective (n : ℕ) : Function.Injective ⇑(gammaEmbedding n)

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

theorem ConnesRigidity.gammaEmbedding_range_index (n : ℕ) : (gammaEmbedding n).range.index = 2 ^ (4 * n)

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

noncomputable def ConnesRigidity.gammaExactIndexEmbedding (n : ℕ) : ExactIndexEmbedding (gammaGroup 0) (gammaGroup n) (2 ^ (4 * n))

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

Equations

• ConnesRigidity.gammaExactIndexEmbedding n = { hom := ConnesRigidity.gammaEmbedding n, injective := ⋯, index_eq := ⋯ }

theorem ConnesRigidity.carryFourier_conjugates_normal_generator (n : ℕ) (η : E n) : (carryFourierEquiv n).conjStarAlgEquiv ↑(leftRegularUnitary (Multiplicative.ofAdd η)) = crossedBaseMultiplier (paperCarryHaarAction n) (carryCharacterCoefficient n η)

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

theorem ConnesRigidity.splitFourier_conjugates_normal_generator (d : D) : splitFourierEquiv.conjStarAlgEquiv ↑(leftRegularUnitary (Multiplicative.ofAdd d)) = crossedBaseMultiplier paperSplitHaarAction (splitCharacterCoefficient d)

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

theorem ConnesRigidity.k_dividedSquare_orbit_infinite (b : ↥B) (hb : b ≠ 0) : (Set.range fun (k : ↥K) => (kDividedSquareLinear k) b).Infinite

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

theorem ConnesRigidity.k_D_orbit_infinite (x : D) (hx : x ≠ 0) : (Set.range fun (k : ↥K) => (kDLinear k) x).Infinite

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

def ConnesRigidity.semidirectCountableGroup (A H : CountableDiscreteGroup) (action : H.Carrier →* MulAut A.Carrier) : CountableDiscreteGroup

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

Equations

• ConnesRigidity.semidirectCountableGroup A H action = { Carrier := A.Carrier ⋊[action] H.Carrier, group := inferInstance, countable := ⋯ }

theorem ConnesRigidity.semidirect_isICC (A H : CountableDiscreteGroup) (action : H.Carrier →* MulAut A.Carrier) (hH : IsICC H) (horbit : ∀ (a : A.Carrier), a ≠ 1 → (Set.range fun (h : H.Carrier) => (action h) a).Infinite) : IsICC (semidirectCountableGroup A H action)

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

theorem ConnesRigidity.sigma_equivariant_raw (n : ℕ) (k : ↥K) (η : E n) : (sigma n) (Multiplicative.toAdd (((kEAction n) k) (Multiplicative.ofAdd η))) = (kDividedSquareLinear k) ((sigma n) η)

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

theorem ConnesRigidity.gamma_isICC (n : ℕ) : IsICC (gammaGroup n)

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