Carry groups, duality, and crossed products

theorem ConnesRigidity.suslinElementaryGeneration_iff_relative : SuslinElementaryGeneration ↔ SuslinRelativeElementaryGeneration

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

theorem ConnesRigidity.suslinRelativeElementaryGeneration_of_maximal_local_elementary (hlocal : ∀ g ∈ suslinAugmentationKernel, ∀ (m : Ideal ℤ) [inst : m.IsMaximal], (Matrix.SpecialLinearGroup.map (Polynomial.mapRingHom (algebraMap ℤ (Localization.AtPrime m)))) g ∈ localGlobalElementarySubgroup (Polynomial (Localization.AtPrime m))) : SuslinRelativeElementaryGeneration

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

@[reducible, inline]

abbrev ConnesRigidity.cornulierLast : Index

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

Equations

• ConnesRigidity.cornulierLast = 3

noncomputable def ConnesRigidity.cornulierRoot (i j : Index) (h : i ≠ j) (a : IntegralPolynomial) : integralElementaryGroup.Carrier

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

Equations

• ConnesRigidity.cornulierRoot i j h a = ⟨Matrix.SpecialLinearGroup.transvection h a, ⋯⟩

noncomputable def ConnesRigidity.cornulierK₁ : Subgroup integralElementaryGroup.Carrier

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

Equations

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

noncomputable def ConnesRigidity.cornulierK₂ : Subgroup integralElementaryGroup.Carrier

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

Equations

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

theorem ConnesRigidity.cornulierRoot_mem_K₁ (i : Index) (h : i ≠ cornulierLast) (a : IntegralPolynomial) : cornulierRoot i cornulierLast h a ∈ cornulierK₁

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

theorem ConnesRigidity.cornulierRoot_mem_K₂ (j : Index) (h : cornulierLast ≠ j) (a : IntegralPolynomial) : cornulierRoot cornulierLast j h a ∈ cornulierK₂

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

theorem ConnesRigidity.cornulierK₁_sup_cornulierK₂_eq_top : cornulierK₁ ⊔ cornulierK₂ = ⊤

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

def ConnesRigidity.cornulierBlockSubgroup : Subgroup IntegralSpecialLinearGroup

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

Equations

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

noncomputable def ConnesRigidity.cornulierH : Subgroup integralElementaryGroup.Carrier

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

Equations

• ConnesRigidity.cornulierH = Subgroup.comap ConnesRigidity.integralElementarySubgroup.subtype ConnesRigidity.cornulierBlockSubgroup

def ConnesRigidity.CornulierBoundedFactorization : Prop

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

Equations

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

theorem ConnesRigidity.cornulierH_le_normalizer_K₁ : cornulierH ≤ Subgroup.normalizer ↑cornulierK₁

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

theorem ConnesRigidity.cornulierH_le_normalizer_K₂ : cornulierH ≤ Subgroup.normalizer ↑cornulierK₂

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

theorem ConnesRigidity.suslin_atPrime_polynomial_elementary (p : Ideal ℤ) [p.IsMaximal] (g : Matrix.SpecialLinearGroup (Fin 4) (Polynomial (Localization.AtPrime p))) : g ∈ localGlobalElementarySubgroup (Polynomial (Localization.AtPrime p))

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

theorem ConnesRigidity.K_no_nontrivial_torsion (g : ↥K) : IsOfFinOrder g → g = 1

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

theorem ConnesRigidity.actingGroup_isICC : IsICC actingGroup

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

@[reducible, inline]

abbrev ConnesRigidity.X : Type

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

Equations

• ConnesRigidity.X = (ConnesRigidity.V →ₗ[ConnesRigidity.F] ConnesRigidity.F)

@[reducible, inline]

abbrev ConnesRigidity.Y : Type

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

Equations

• ConnesRigidity.Y = (↥ConnesRigidity.B →ₗ[ConnesRigidity.F] ConnesRigidity.F)

noncomputable def ConnesRigidity.tensorFunctional (ℓ ℓ' : X) : T →ₗ[F] F

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

Equations

• ConnesRigidity.tensorFunctional ℓ ℓ' = TensorProduct.lift ((LinearMap.mul ConnesRigidity.F ConnesRigidity.F).compl₁₂ ℓ ℓ')

noncomputable def ConnesRigidity.carry (ℓ ℓ' : X) : Y

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

Equations

• ConnesRigidity.carry ℓ ℓ' = ConnesRigidity.tensorFunctional ℓ ℓ' ∘ₗ ConnesRigidity.B.subtype

noncomputable def ConnesRigidity.shiftVector (n : ℕ) : V →ₗ[F] V

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

Equations

• ConnesRigidity.shiftVector n = ↑ConnesRigidity.F ((LinearMap.lsmul ConnesRigidity.R ConnesRigidity.V) (Polynomial.X ^ n))

noncomputable def ConnesRigidity.shift (n : ℕ) : X →ₗ[F] X

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

Equations

• ConnesRigidity.shift n = { toFun := fun (ℓ : ConnesRigidity.X) => ℓ ∘ₗ ConnesRigidity.shiftVector n, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ConnesRigidity.shiftedCarry (n : ℕ) (ℓ ℓ' : X) : Y

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

Equations

• ConnesRigidity.shiftedCarry n ℓ ℓ' = ConnesRigidity.carry ((ConnesRigidity.shift n) ℓ) ((ConnesRigidity.shift n) ℓ')

structure ConnesRigidity.CarryGroup (_n : ℕ) : Type

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

• linear : X

  The linear coordinate.

• quadratic : Y

  The quadratic coordinate.

theorem ConnesRigidity.CarryGroup.ext {n : ℕ} {x y : CarryGroup n} (hlinear : x.linear = y.linear) (hquadratic : x.quadratic = y.quadratic) : x = y

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

theorem ConnesRigidity.CarryGroup.ext_iff {n : ℕ} {x y : CarryGroup n} : x = y ↔ x.linear = y.linear ∧ x.quadratic = y.quadratic

@[instance_reducible]

noncomputable instance ConnesRigidity.CarryGroup.instZero {n : ℕ} : Zero (CarryGroup n)

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

Equations

• ConnesRigidity.CarryGroup.instZero = { zero := { linear := 0, quadratic := 0 } }

@[instance_reducible]

noncomputable instance ConnesRigidity.CarryGroup.instAdd {n : ℕ} : Add (CarryGroup n)

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

Equations

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

@[instance_reducible]

noncomputable instance ConnesRigidity.CarryGroup.instNeg {n : ℕ} : Neg (CarryGroup n)

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

Equations

• ConnesRigidity.CarryGroup.instNeg = { neg := fun (x : ConnesRigidity.CarryGroup n) => { linear := x.linear, quadratic := x.quadratic + ConnesRigidity.shiftedCarry n x.linear x.linear } }

theorem ConnesRigidity.CarryGroup.add_assoc' {n : ℕ} (x y z : CarryGroup n) : x + y + z = x + (y + z)

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

theorem ConnesRigidity.CarryGroup.zero_add' {n : ℕ} (x : CarryGroup n) : 0 + x = x

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

theorem ConnesRigidity.CarryGroup.neg_add_cancel' {n : ℕ} (x : CarryGroup n) : -x + x = 0

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

@[instance_reducible]

noncomputable instance ConnesRigidity.CarryGroup.instAddGroup {n : ℕ} : AddGroup (CarryGroup n)

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

Equations

• ConnesRigidity.CarryGroup.instAddGroup = AddGroup.ofLeftAxioms ⋯ ⋯ ⋯

@[instance_reducible]

noncomputable instance ConnesRigidity.CarryGroup.instAddCommGroup {n : ℕ} : AddCommGroup (CarryGroup n)

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

Equations

• ConnesRigidity.CarryGroup.instAddCommGroup = { toAddGroup := ConnesRigidity.CarryGroup.instAddGroup, add_comm := ⋯ }

@[reducible]

def ConnesRigidity.pointwiseDualTopology (M : Type u_1) [AddCommGroup M] [Module F M] : TopologicalSpace (M →ₗ[F] F)

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

Equations

• ConnesRigidity.pointwiseDualTopology M = TopologicalSpace.induced (fun (ℓ : M →ₗ[ConnesRigidity.F] ConnesRigidity.F) (m : M) => ℓ m) inferInstance

@[instance_reducible]

noncomputable instance ConnesRigidity.instXTopologicalSpace : TopologicalSpace X

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

Equations

• ConnesRigidity.instXTopologicalSpace = ConnesRigidity.pointwiseDualTopology ConnesRigidity.V

@[instance_reducible]

noncomputable instance ConnesRigidity.instYTopologicalSpace : TopologicalSpace Y

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

Equations

• ConnesRigidity.instYTopologicalSpace = ConnesRigidity.pointwiseDualTopology ↥ConnesRigidity.B

instance ConnesRigidity.instXCompactSpace : CompactSpace X

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

instance ConnesRigidity.instYCompactSpace : CompactSpace Y

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

instance ConnesRigidity.instXT2Space : T2Space X

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

instance ConnesRigidity.instYT2Space : T2Space Y

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

instance ConnesRigidity.instXSecondCountableTopology : SecondCountableTopology X

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

instance ConnesRigidity.instYSecondCountableTopology : SecondCountableTopology Y

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

theorem ConnesRigidity.continuous_X_eval (v : V) : Continuous fun (ℓ : X) => ℓ v

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

theorem ConnesRigidity.continuous_Y_eval (w : ↥B) : Continuous fun (q : Y) => q w

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

theorem ConnesRigidity.continuous_X_precomp (f : V →ₗ[F] V) : Continuous fun (ℓ : X) => ℓ ∘ₗ f

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

theorem ConnesRigidity.continuous_Y_precomp (f : ↥B →ₗ[F] ↥B) : Continuous fun (q : Y) => q ∘ₗ f

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

instance ConnesRigidity.instXTopologicalAddGroup : IsTopologicalAddGroup X

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

instance ConnesRigidity.instYTopologicalAddGroup : IsTopologicalAddGroup Y

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

def ConnesRigidity.carryCoordinates (n : ℕ) (z : CarryGroup n) : X × Y

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

Equations

• ConnesRigidity.carryCoordinates n z = (z.linear, z.quadratic)

@[instance_reducible]

noncomputable instance ConnesRigidity.instCarryGroupTopologicalSpace (n : ℕ) : TopologicalSpace (CarryGroup n)

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

Equations

• ConnesRigidity.instCarryGroupTopologicalSpace n = TopologicalSpace.induced (ConnesRigidity.carryCoordinates n) inferInstance

def ConnesRigidity.carryHomeomorph (n : ℕ) : CarryGroup n ≃ₜ X × Y

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

Equations

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

theorem ConnesRigidity.continuous_linear_eval (n : ℕ) (v : V) : Continuous fun (z : CarryGroup n) => z.linear v

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

instance ConnesRigidity.instCarryGroupCompactSpace (n : ℕ) : CompactSpace (CarryGroup n)

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

instance ConnesRigidity.instCarryGroupT2Space (n : ℕ) : T2Space (CarryGroup n)

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

instance ConnesRigidity.instCarryGroupSecondCountableTopology (n : ℕ) : SecondCountableTopology (CarryGroup n)

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

noncomputable def ConnesRigidity.binaryRootsEquiv : Multiplicative F ≃* ↥(rootsOfUnity 2 Circle)

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

Equations

• ConnesRigidity.binaryRootsEquiv = MulEquiv.ofBijective (AddChar.toMonoidHomEquiv (ZMod.rootsOfUnityAddChar 2)) ConnesRigidity.binaryRootsEquiv._proof_2

noncomputable def ConnesRigidity.characterIntoRoots (M : Type u_1) [AddCommGroup M] [Module F M] [TopologicalSpace M] (χ : PontryaginDual (Multiplicative M)) : Multiplicative M →* ↥(rootsOfUnity 2 Circle)

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

Equations

• ConnesRigidity.characterIntoRoots M χ = { toFun := fun (x : Multiplicative M) => ⟨toUnits (χ x), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

noncomputable def ConnesRigidity.characterAdd (M : Type u_1) [AddCommGroup M] [Module F M] [TopologicalSpace M] (χ : PontryaginDual (Multiplicative M)) : M →+ F

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

Equations

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

noncomputable def ConnesRigidity.characterLinear (M : Type u_1) [AddCommGroup M] [Module F M] [TopologicalSpace M] (χ : PontryaginDual (Multiplicative M)) : M →ₗ[F] F

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

Equations

• ConnesRigidity.characterLinear M χ = AddMonoidHom.toZModLinearMap 2 (ConnesRigidity.characterAdd M χ)

@[simp]

theorem ConnesRigidity.characterLinear_circle (M : Type u_1) [AddCommGroup M] [Module F M] [TopologicalSpace M] (χ : PontryaginDual (Multiplicative M)) (x : M) : ZMod.toCircle ((characterLinear M χ) x) = χ (Multiplicative.ofAdd x)

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

theorem ConnesRigidity.continuous_characterLinear (M : Type u_1) [AddCommGroup M] [Module F M] [TopologicalSpace M] (χ : PontryaginDual (Multiplicative M)) : Continuous ⇑(characterLinear M χ)

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

theorem ConnesRigidity.continuous_binaryDual_eq_evaluation (M : Type u_1) [AddCommGroup M] [Module F M] (φ : (M →ₗ[F] F) →ₗ[F] F) (hφ : Continuous ⇑φ) : ∃ (m : M), ∀ (ℓ : M →ₗ[F] F), φ ℓ = ℓ m

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

@[instance_reducible]

def ConnesRigidity.instPointwiseBinaryDualTopology (M : Type u_1) [AddCommGroup M] [Module F M] : TopologicalSpace (M →ₗ[F] F)

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

Equations

• ConnesRigidity.instPointwiseBinaryDualTopology M = ConnesRigidity.pointwiseDualTopology M

noncomputable def ConnesRigidity.pointwiseEvaluationCharacter (M : Type u_1) [AddCommGroup M] [Module F M] (m : M) : PontryaginDual (Multiplicative (M →ₗ[F] F))

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

Equations

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

noncomputable def ConnesRigidity.pointwiseEvaluationHom (M : Type u_1) [AddCommGroup M] [Module F M] : M →+ Additive (PontryaginDual (Multiplicative (M →ₗ[F] F)))

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

Equations

• ConnesRigidity.pointwiseEvaluationHom M = { toFun := fun (m : M) => Additive.ofMul (ConnesRigidity.pointwiseEvaluationCharacter M m), map_zero' := ⋯, map_add' := ⋯ }

noncomputable def ConnesRigidity.pointwisePontryaginDualEquiv (M : Type u_1) [AddCommGroup M] [Module F M] : Additive (PontryaginDual (Multiplicative (M →ₗ[F] F))) ≃+ M

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

Equations

• ConnesRigidity.pointwisePontryaginDualEquiv M = (AddEquiv.ofBijective (ConnesRigidity.pointwiseEvaluationHom M) ⋯).symm

@[reducible, inline]

abbrev ConnesRigidity.FiniteCarry.Bit : Type

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

Equations

• ConnesRigidity.FiniteCarry.Bit = ZMod 2

def ConnesRigidity.FiniteCarry.carry (x x' : Bit) : Bit

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

Equations

• ConnesRigidity.FiniteCarry.carry x x' = x * x'

def ConnesRigidity.FiniteCarry.liftBit (x : Bit) : ZMod 4

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

Equations

• ConnesRigidity.FiniteCarry.liftBit x = ↑(ZMod.val x)

structure ConnesRigidity.FiniteCarry.Carry : Type

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

• low : Bit

  The low carry bit.

• high : Bit

  The high carry bit.

theorem ConnesRigidity.FiniteCarry.Carry.ext_iff {x y : Carry} : x = y ↔ x.low = y.low ∧ x.high = y.high

theorem ConnesRigidity.FiniteCarry.Carry.ext {x y : Carry} (low : x.low = y.low) (high : x.high = y.high) : x = y

def ConnesRigidity.FiniteCarry.instDecidableEqCarry.decEq (x✝ x✝¹ : Carry) : Decidable (x✝ = x✝¹)

Equations

• ConnesRigidity.FiniteCarry.instDecidableEqCarry.decEq { low := a, high := a_1 } { low := b, high := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance ConnesRigidity.FiniteCarry.instDecidableEqCarry : DecidableEq Carry

Equations

• ConnesRigidity.FiniteCarry.instDecidableEqCarry = ConnesRigidity.FiniteCarry.instDecidableEqCarry.decEq

@[instance_reducible]

instance ConnesRigidity.FiniteCarry.instFintypeCarry : Fintype Carry

Equations

• ConnesRigidity.FiniteCarry.instFintypeCarry = Fintype.ofEquiv ((_ : ConnesRigidity.FiniteCarry.Bit) × ConnesRigidity.FiniteCarry.Bit) ConnesRigidity.FiniteCarry.Carry.proxyTypeEquiv

@[instance_reducible]

instance ConnesRigidity.FiniteCarry.Carry.instAdd : Add Carry

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

Equations

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

@[instance_reducible]

instance ConnesRigidity.FiniteCarry.Carry.instZero : Zero Carry

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

Equations

• ConnesRigidity.FiniteCarry.Carry.instZero = { zero := { low := 0, high := 0 } }

@[instance_reducible]

instance ConnesRigidity.FiniteCarry.Carry.instNeg : Neg Carry

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

Equations

• ConnesRigidity.FiniteCarry.Carry.instNeg = { neg := fun (p : ConnesRigidity.FiniteCarry.Carry) => { low := p.low, high := p.high + p.low } }

@[instance_reducible]

instance ConnesRigidity.FiniteCarry.Carry.instAddCommGroup : AddCommGroup Carry

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

Equations

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

def ConnesRigidity.FiniteCarry.Carry.code (p : Carry) : ZMod 4

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

Equations

• p.code = ConnesRigidity.FiniteCarry.liftBit p.low + 2 * ConnesRigidity.FiniteCarry.liftBit p.high

def ConnesRigidity.FiniteCarry.Carry.decode (z : ZMod 4) : Carry

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

Equations

• ConnesRigidity.FiniteCarry.Carry.decode z = { low := ↑(z.val % 2), high := ↑(z.val / 2) }

def ConnesRigidity.FiniteCarry.Carry.codeEquiv : Carry ≃+ ZMod 4

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

Equations

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

theorem ConnesRigidity.FiniteCarry.Carry.exponent_four (p : Carry) : 4 • p = 0

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

@[simp]

theorem ConnesRigidity.FiniteCarry.Carry.card : Fintype.card Carry = 4

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

noncomputable def ConnesRigidity.CarryGroup.pointEvaluation (n : ℕ) (v : V) : CarryGroup n →+ FiniteCarry.Carry

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

Equations

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

noncomputable def ConnesRigidity.CarryGroup.evalFour (n : ℕ) (v : V) : CarryGroup n →+ ZMod 4

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

Equations

• ConnesRigidity.CarryGroup.evalFour n v = ConnesRigidity.FiniteCarry.Carry.codeEquiv.toAddMonoidHom.comp (ConnesRigidity.CarryGroup.pointEvaluation n v)

@[simp]

theorem ConnesRigidity.CarryGroup.evalFour_apply (n : ℕ) (v : V) (x : CarryGroup n) : (evalFour n v) x = FiniteCarry.liftBit (((shift n) x.linear) v) + 2 * FiniteCarry.liftBit (x.quadratic (diagonal v))

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

instance ConnesRigidity.instCarryGroupContinuousAdd (n : ℕ) : ContinuousAdd (CarryGroup n)

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

instance ConnesRigidity.instCarryGroupContinuousNeg (n : ℕ) : ContinuousNeg (CarryGroup n)

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

instance ConnesRigidity.instCarryGroupTopologicalAddGroup (n : ℕ) : IsTopologicalAddGroup (CarryGroup n)

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

@[reducible, inline]

abbrev ConnesRigidity.E (n : ℕ) : Type

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

Equations

• ConnesRigidity.E n = Additive (PontryaginDual (Multiplicative (ConnesRigidity.CarryGroup n)))

noncomputable def ConnesRigidity.fourthRootAddCharacter : AddChar (ZMod 4) Circle

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

Equations

• ConnesRigidity.fourthRootAddCharacter = ZMod.toCircle

noncomputable def ConnesRigidity.fourthRootMonoidCharacter : Multiplicative (ZMod 4) →* Circle

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

Equations

• ConnesRigidity.fourthRootMonoidCharacter = AddChar.toMonoidHomEquiv ConnesRigidity.fourthRootAddCharacter

noncomputable def ConnesRigidity.fourthRootCharacter : PontryaginDual (Multiplicative (ZMod 4))

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

Equations

• ConnesRigidity.fourthRootCharacter = { toMonoidHom := ConnesRigidity.fourthRootMonoidCharacter, continuous_toFun := ConnesRigidity.fourthRootCharacter._proof_1 }

theorem ConnesRigidity.E_four_nsmul (n : ℕ) (η : E n) : 4 • η = 0

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

theorem ConnesRigidity.continuous_evalFour (n : ℕ) (v : V) : Continuous ⇑(CarryGroup.evalFour n v)

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

noncomputable def ConnesRigidity.evalFourContinuous (n : ℕ) (v : V) : Multiplicative (CarryGroup n) →ₜ* Multiplicative (ZMod 4)

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

Equations

• ConnesRigidity.evalFourContinuous n v = { toMonoidHom := AddMonoidHom.toMultiplicative (ConnesRigidity.CarryGroup.evalFour n v), continuous_toFun := ⋯ }

noncomputable def ConnesRigidity.fourthRootCharacter.comp {A : Type u_1} [AddMonoid A] [TopologicalSpace A] (f : Multiplicative A →ₜ* Multiplicative (ZMod 4)) : PontryaginDual (Multiplicative A)

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

Equations

• ConnesRigidity.fourthRootCharacter.comp f = (PontryaginDual.map f) ConnesRigidity.fourthRootCharacter

@[simp]

theorem ConnesRigidity.fourthRootCharacter.comp_apply {A : Type u_1} [AddMonoid A] [TopologicalSpace A] (f : Multiplicative A →ₜ* Multiplicative (ZMod 4)) (a : Multiplicative A) : (comp f) a = fourthRootCharacter (f a)

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

noncomputable def ConnesRigidity.epsilon (n : ℕ) (v : V) : E n

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

Equations

• ConnesRigidity.epsilon n v = Additive.ofMul (ConnesRigidity.fourthRootCharacter.comp (ConnesRigidity.evalFourContinuous n v))

@[simp]

theorem ConnesRigidity.epsilon_apply (n : ℕ) (v : V) (z : CarryGroup n) : (Additive.toMul (epsilon n v)) (Multiplicative.ofAdd z) = ZMod.toCircle ((CarryGroup.evalFour n v) z)

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

theorem ConnesRigidity.epsilon_two_nsmul_ne_zero (n : ℕ) : 2 • epsilon n e ≠ 0

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

noncomputable def ConnesRigidity.dualAut (A : Type u_1) [CommGroup A] [TopologicalSpace A] (e : A ≃ₜ* A) : MulAut (PontryaginDual A)

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

Equations

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

def ConnesRigidity.continuousAutOfAction (A : Type u_1) [CommGroup A] [TopologicalSpace A] (K : Type u_2) [Group K] (ρ : K →* MulAut A) (hcont : ∀ (k : K), Continuous ⇑(ρ k)) (k : K) : A ≃ₜ* A

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

Equations

• ConnesRigidity.continuousAutOfAction A K ρ hcont k = { toMulEquiv := ρ k, continuous_toFun := ⋯, continuous_invFun := ⋯ }

noncomputable def ConnesRigidity.dualAction (A : Type u_1) [CommGroup A] [TopologicalSpace A] (K : Type u_2) [Group K] (ρ : K →* MulAut A) (hcont : ∀ (k : K), Continuous ⇑(ρ k)) : K →* MulAut (PontryaginDual A)

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

Equations

• ConnesRigidity.dualAction A K ρ hcont = { toFun := fun (k : K) => ConnesRigidity.dualAut A (ConnesRigidity.continuousAutOfAction A K ρ hcont k), map_one' := ⋯, map_mul' := ⋯ }

instance ConnesRigidity.instECountable (n : ℕ) : Countable (E n)

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

theorem ConnesRigidity.shiftVector_injective (n : ℕ) : Function.Injective ⇑(shiftVector n)

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

theorem ConnesRigidity.shiftVector_range (n : ℕ) : (shiftVector n).range = shiftedSubmodule n

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

noncomputable def ConnesRigidity.shiftKernel (n : ℕ) : Submodule F X

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

Equations

• ConnesRigidity.shiftKernel n = (ConnesRigidity.shift n).ker

theorem ConnesRigidity.shiftKernel_eq_dualAnnihilator (n : ℕ) : shiftKernel n = (shiftedSubmodule n).dualAnnihilator

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

noncomputable def ConnesRigidity.shiftKernelEquivDualQuotient (n : ℕ) : ↥(shiftKernel n) ≃ₗ[F] Module.Dual F (ShiftedQuotient n)

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

Equations

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

noncomputable def ConnesRigidity.shiftedQuotientBasis (n : ℕ) : Module.Basis (Fin 4 × Fin n) F (ShiftedQuotient n)

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

Equations

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

noncomputable def ConnesRigidity.shiftKernelEquivQuotient (n : ℕ) : ↥(shiftKernel n) ≃ₗ[F] ShiftedQuotient n

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

Equations

• ConnesRigidity.shiftKernelEquivQuotient n = (ConnesRigidity.shiftKernelEquivDualQuotient n).trans (ConnesRigidity.shiftedQuotientBasis n).toDualEquiv.symm

theorem ConnesRigidity.shiftKernel_card (n : ℕ) : Nat.card ↥(shiftKernel n) = 2 ^ (4 * n)

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

noncomputable def ConnesRigidity.carryKernelInclusion (n : ℕ) : Y →+ CarryGroup n

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

Equations

• ConnesRigidity.carryKernelInclusion n = { toFun := fun (q : ConnesRigidity.Y) => { linear := 0, quadratic := q }, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def ConnesRigidity.carryPullback (n : ℕ) : CarryGroup n →+ CarryGroup 0

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

Equations

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

theorem ConnesRigidity.continuous_carryPullback (n : ℕ) : Continuous ⇑(carryPullback n)

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

noncomputable def ConnesRigidity.shiftKernelInclusion (n : ℕ) : ↥(shiftKernel n) →+ CarryGroup n

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

Equations

• ConnesRigidity.shiftKernelInclusion n = { toFun := fun (ℓ : ↥(ConnesRigidity.shiftKernel n)) => { linear := ↑ℓ, quadratic := 0 }, map_zero' := ⋯, map_add' := ⋯ }

theorem ConnesRigidity.continuous_shiftKernelInclusion (n : ℕ) : Continuous ⇑(shiftKernelInclusion n)

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

noncomputable def ConnesRigidity.shiftVectorLeftInverse (n : ℕ) : V →ₗ[F] V

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

Equations

• ConnesRigidity.shiftVectorLeftInverse n = (ConnesRigidity.shiftVector n).leftInverse

noncomputable def ConnesRigidity.shiftSection (n : ℕ) : X →ₗ[F] X

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

Equations

• ConnesRigidity.shiftSection n = { toFun := fun (ℓ : ConnesRigidity.X) => ℓ ∘ₗ ConnesRigidity.shiftVectorLeftInverse n, map_add' := ⋯, map_smul' := ⋯ }

noncomputable def ConnesRigidity.carryPullbackSection (n : ℕ) : CarryGroup 0 →+ CarryGroup n

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

Equations

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

theorem ConnesRigidity.continuous_carryPullbackSection (n : ℕ) : Continuous ⇑(carryPullbackSection n)

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

@[simp]

theorem ConnesRigidity.carryPullback_carryPullbackSection (n : ℕ) (z : CarryGroup 0) : (carryPullback n) ((carryPullbackSection n) z) = z

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

noncomputable def ConnesRigidity.carryPullbackContinuous (n : ℕ) : Multiplicative (CarryGroup n) →ₜ* Multiplicative (CarryGroup 0)

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

Equations

• ConnesRigidity.carryPullbackContinuous n = { toMonoidHom := AddMonoidHom.toMultiplicative (ConnesRigidity.carryPullback n), continuous_toFun := ⋯ }

noncomputable def ConnesRigidity.carryPullbackSectionContinuous (n : ℕ) : Multiplicative (CarryGroup 0) →ₜ* Multiplicative (CarryGroup n)

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

Equations

• ConnesRigidity.carryPullbackSectionContinuous n = { toMonoidHom := AddMonoidHom.toMultiplicative (ConnesRigidity.carryPullbackSection n), continuous_toFun := ⋯ }

noncomputable def ConnesRigidity.kernelProjection (n : ℕ) : CarryGroup n →+ ↥(shiftKernel n)

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

Equations

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

theorem ConnesRigidity.continuous_kernelProjection (n : ℕ) : Continuous ⇑(kernelProjection n)

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

noncomputable def ConnesRigidity.kernelProjectionContinuous (n : ℕ) : Multiplicative (CarryGroup n) →ₜ* Multiplicative ↥(shiftKernel n)

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

Equations

• ConnesRigidity.kernelProjectionContinuous n = { toMonoidHom := AddMonoidHom.toMultiplicative (ConnesRigidity.kernelProjection n), continuous_toFun := ⋯ }

noncomputable def ConnesRigidity.shiftKernelInclusionContinuous (n : ℕ) : Multiplicative ↥(shiftKernel n) →ₜ* Multiplicative (CarryGroup n)

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

Equations

• ConnesRigidity.shiftKernelInclusionContinuous n = { toMonoidHom := AddMonoidHom.toMultiplicative (ConnesRigidity.shiftKernelInclusion n), continuous_toFun := ⋯ }

@[simp]

theorem ConnesRigidity.kernelProjection_shiftKernelInclusion (n : ℕ) (ℓ : ↥(shiftKernel n)) : (kernelProjection n) ((shiftKernelInclusion n) ℓ) = ℓ

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

noncomputable def ConnesRigidity.carryGroupSplitEquiv (n : ℕ) : CarryGroup n ≃+ CarryGroup 0 × ↥(shiftKernel n)

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

Equations

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

noncomputable def ConnesRigidity.auxiliaryBasis : Module.Basis (↑(Module.Basis.ofVectorSpaceIndex F V)) F V

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

Equations

• ConnesRigidity.auxiliaryBasis = Module.Basis.ofVectorSpace ConnesRigidity.F ConnesRigidity.V

noncomputable def ConnesRigidity.coordinateProduct : V →ₗ[F] V →ₗ[F] V

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

Equations

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

noncomputable def ConnesRigidity.tensorDiagonal : T →ₗ[F] V

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

Equations

• ConnesRigidity.tensorDiagonal = TensorProduct.lift ConnesRigidity.coordinateProduct

noncomputable def ConnesRigidity.d : ↥B →ₗ[F] V

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

Equations

• ConnesRigidity.d = ConnesRigidity.tensorDiagonal ∘ₗ ConnesRigidity.B.subtype

theorem ConnesRigidity.d_surjective : Function.Surjective ⇑d

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

theorem ConnesRigidity.linearMap_ext_on_diagonal {W : Type u_1} [AddCommGroup W] [Module F W] {f g : ↥B →ₗ[F] W} (h : ∀ (v : V), f (diagonal v) = g (diagonal v)) : f = g

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

noncomputable def ConnesRigidity.binaryRootCharacter : PontryaginDual (Multiplicative F)

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

Equations

• ConnesRigidity.binaryRootCharacter = { toMonoidHom := AddChar.toMonoidHomEquiv ZMod.toCircle, continuous_toFun := ConnesRigidity.binaryRootCharacter._proof_1 }

noncomputable def ConnesRigidity.carryLinearEvaluation (n : ℕ) (v : V) : CarryGroup n →+ F

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

Equations

• ConnesRigidity.carryLinearEvaluation n v = { toFun := fun (z : ConnesRigidity.CarryGroup n) => z.linear v, map_zero' := ⋯, map_add' := ⋯ }

noncomputable def ConnesRigidity.carryLinearEvaluationContinuous (n : ℕ) (v : V) : Multiplicative (CarryGroup n) →ₜ* Multiplicative F

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

Equations

• ConnesRigidity.carryLinearEvaluationContinuous n v = { toMonoidHom := AddMonoidHom.toMultiplicative (ConnesRigidity.carryLinearEvaluation n v), continuous_toFun := ⋯ }

noncomputable def ConnesRigidity.iotaCharacter (n : ℕ) (v : V) : E n

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

Equations

• ConnesRigidity.iotaCharacter n v = Additive.ofMul ((PontryaginDual.map (ConnesRigidity.carryLinearEvaluationContinuous n v)) ConnesRigidity.binaryRootCharacter)

noncomputable def ConnesRigidity.iota (n : ℕ) : V →+ E n

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

Equations

• ConnesRigidity.iota n = { toFun := ConnesRigidity.iotaCharacter n, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem ConnesRigidity.iota_apply (n : ℕ) (v : V) (z : CarryGroup n) : (Additive.toMul ((iota n) v)) (Multiplicative.ofAdd z) = ZMod.toCircle (z.linear v)

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

theorem ConnesRigidity.iota_injective (n : ℕ) : Function.Injective ⇑(iota n)

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

noncomputable def ConnesRigidity.quadraticInclusionContinuous (n : ℕ) : Multiplicative Y →ₜ* Multiplicative (CarryGroup n)

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

Equations

• ConnesRigidity.quadraticInclusionContinuous n = { toMonoidHom := AddMonoidHom.toMultiplicative (ConnesRigidity.carryKernelInclusion n), continuous_toFun := ⋯ }

noncomputable def ConnesRigidity.quadraticRestriction (n : ℕ) : E n →+ Additive (PontryaginDual (Multiplicative Y))

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

Equations

• ConnesRigidity.quadraticRestriction n = MonoidHom.toAdditive (PontryaginDual.map (ConnesRigidity.quadraticInclusionContinuous n)).toMonoidHom

noncomputable def ConnesRigidity.sigma (n : ℕ) : E n →+ ↥B

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

Equations

• ConnesRigidity.sigma n = (ConnesRigidity.pointwisePontryaginDualEquiv ↥ConnesRigidity.B).toAddMonoidHom.comp (ConnesRigidity.quadraticRestriction n)

theorem ConnesRigidity.sigma_characterization (n : ℕ) (η : E n) (q : Y) : ZMod.toCircle (q ((sigma n) η)) = (Additive.toMul η) (Multiplicative.ofAdd { linear := 0, quadratic := q })

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

theorem ConnesRigidity.sigma_surjective (n : ℕ) : Function.Surjective ⇑(sigma n)

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

theorem ConnesRigidity.sigma_ker (n : ℕ) : (sigma n).ker = (iota n).range

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

theorem ConnesRigidity.two_nsmul_eta (n : ℕ) (η : E n) : 2 • η = (iota n) ((shiftVector n) (d ((sigma n) η)))

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

@[instance_reducible]

noncomputable instance ConnesRigidity.instXMeasurableSpace : MeasurableSpace X

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

Equations

• ConnesRigidity.instXMeasurableSpace = borel ConnesRigidity.X

instance ConnesRigidity.instXBorelSpace : BorelSpace X

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

@[instance_reducible]

noncomputable instance ConnesRigidity.instYMeasurableSpace : MeasurableSpace Y

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

Equations

• ConnesRigidity.instYMeasurableSpace = borel ConnesRigidity.Y

instance ConnesRigidity.instYBorelSpace : BorelSpace Y

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

@[instance_reducible]

noncomputable instance ConnesRigidity.instCarryGroupMeasurableSpace (n : ℕ) : MeasurableSpace (CarryGroup n)

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

Equations

• ConnesRigidity.instCarryGroupMeasurableSpace n = borel (ConnesRigidity.CarryGroup n)

instance ConnesRigidity.instCarryGroupBorelSpace (n : ℕ) : BorelSpace (CarryGroup n)

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

noncomputable def ConnesRigidity.normalizedAddHaar (A : Type u) [AddGroup A] [TopologicalSpace A] [CompactSpace A] [IsTopologicalAddGroup A] [MeasurableSpace A] [BorelSpace A] : MeasureTheory.Measure A

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

Equations

• ConnesRigidity.normalizedAddHaar A = MeasureTheory.Measure.addHaarMeasure { carrier := Set.univ, isCompact' := ⋯, interior_nonempty' := ⋯ }

instance ConnesRigidity.normalizedAddHaar_isProbabilityMeasure (A : Type u) [AddGroup A] [TopologicalSpace A] [CompactSpace A] [IsTopologicalAddGroup A] [MeasurableSpace A] [BorelSpace A] : MeasureTheory.IsProbabilityMeasure (normalizedAddHaar A)

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

instance ConnesRigidity.normalizedAddHaar_isAddHaarMeasure (A : Type u) [AddGroup A] [TopologicalSpace A] [CompactSpace A] [IsTopologicalAddGroup A] [MeasurableSpace A] [BorelSpace A] : (normalizedAddHaar A).IsAddHaarMeasure

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

noncomputable def ConnesRigidity.productHaar : MeasureTheory.Measure (X × Y)

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

Equations

• ConnesRigidity.productHaar = (ConnesRigidity.normalizedAddHaar ConnesRigidity.X).prod (ConnesRigidity.normalizedAddHaar ConnesRigidity.Y)

instance ConnesRigidity.productHaar_isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure productHaar

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

instance ConnesRigidity.productHaar_isAddLeftInvariant : productHaar.IsAddLeftInvariant

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

instance ConnesRigidity.productHaar_isAddHaarMeasure : productHaar.IsAddHaarMeasure

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

noncomputable def ConnesRigidity.carryHaar (n : ℕ) : MeasureTheory.Measure (CarryGroup n)

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

Equations

• ConnesRigidity.carryHaar n = MeasureTheory.Measure.map (⇑(ConnesRigidity.carryHomeomorph n).symm) ConnesRigidity.productHaar

instance ConnesRigidity.carryHaar_isProbabilityMeasure (n : ℕ) : MeasureTheory.IsProbabilityMeasure (carryHaar n)

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

instance ConnesRigidity.carryHaar_isAddLeftInvariant (n : ℕ) : (carryHaar n).IsAddLeftInvariant

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

instance ConnesRigidity.carryHaar_isAddHaarMeasure (n : ℕ) : (carryHaar n).IsAddHaarMeasure

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

noncomputable def ConnesRigidity.carryCoordinatesMeasurableEquiv (n : ℕ) : CarryGroup n ≃ᵐ X × Y

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

Equations

• ConnesRigidity.carryCoordinatesMeasurableEquiv n = (ConnesRigidity.carryHomeomorph n).toMeasurableEquiv

theorem ConnesRigidity.carryCoordinates_measurePreserving (n : ℕ) : MeasureTheory.MeasurePreserving (⇑(carryCoordinatesMeasurableEquiv n)) (carryHaar n) productHaar

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

noncomputable def ConnesRigidity.carryComplexCharacter (n : ℕ) (η : E n) : C(CarryGroup n, ℂ)

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

Equations

• ConnesRigidity.carryComplexCharacter n η = { toFun := fun (z : ConnesRigidity.CarryGroup n) => ↑((Additive.toMul η) (Multiplicative.ofAdd z)), continuous_toFun := ⋯ }

theorem ConnesRigidity.carryComplexCharacter_span_closure_eq_top (n : ℕ) : (Submodule.span ℂ (Set.range (carryComplexCharacter n))).topologicalClosure = ⊤

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

noncomputable def ConnesRigidity.carryCharacterL2 (n : ℕ) (η : E n) : ↥(MeasureTheory.Lp ℂ 2 (carryHaar n))

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

Equations

• ConnesRigidity.carryCharacterL2 n η = (ContinuousMap.toLp 2 (ConnesRigidity.carryHaar n) ℂ) (ConnesRigidity.carryComplexCharacter n η)

theorem ConnesRigidity.carryCharacterL2_span_closure_eq_top (n : ℕ) : (Submodule.span ℂ (Set.range (carryCharacterL2 n))).topologicalClosure = ⊤

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

theorem ConnesRigidity.integral_character_mul_conj {G : Type u_1} [AddCommGroup G] [TopologicalSpace G] [IsTopologicalAddGroup G] [MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G) [μ.IsAddLeftInvariant] [MeasureTheory.IsProbabilityMeasure μ] (χ ψ : PontryaginDual (Multiplicative G)) : ∫ (x : G), ↑(ψ (Multiplicative.ofAdd x)) * (starRingEnd ℂ) ↑(χ (Multiplicative.ofAdd x)) ∂μ = if χ = ψ then 1 else 0

Distinct characters are orthogonal for any invariant probability measure.

theorem ConnesRigidity.carryCharacterL2_orthonormal (n : ℕ) : Orthonormal ℂ (carryCharacterL2 n)

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

noncomputable def ConnesRigidity.carryFourierBasis (n : ℕ) : HilbertBasis (E n) ℂ ↥(MeasureTheory.Lp ℂ 2 (carryHaar n))

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

Equations

• ConnesRigidity.carryFourierBasis n = HilbertBasis.mk ⋯ ⋯

noncomputable def ConnesRigidity.carryFourierTransform (n : ℕ) : ↥(lp (fun (x : E n) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 (carryHaar n))

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

Equations

• ConnesRigidity.carryFourierTransform n = (ConnesRigidity.carryFourierBasis n).repr.symm

@[reducible, inline]

noncomputable abbrev ConnesRigidity.carryFourierEquiv (n : ℕ) : ↥(lp (fun (x : E n) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 (carryHaar n))

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

Equations

• ConnesRigidity.carryFourierEquiv n = ConnesRigidity.carryFourierTransform n

theorem ConnesRigidity.carryFourierEquiv_single (n : ℕ) [DecidableEq (E n)] (η : E n) : (carryFourierEquiv n) (lp.single 2 η 1) = carryCharacterL2 n η

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

noncomputable def ConnesRigidity.carryBidualEvaluation (n : ℕ) (z : CarryGroup n) : PontryaginDual (Multiplicative (E n))

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

Equations

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

theorem ConnesRigidity.continuous_carryBidualEvaluation (n : ℕ) : Continuous (carryBidualEvaluation n)

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

theorem ConnesRigidity.carryBidualEvaluation_injective (n : ℕ) : Function.Injective (carryBidualEvaluation n)

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

@[instance_reducible]

def ConnesRigidity.CarryBidualInternal.vectorDiscreteTopology : TopologicalSpace V

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

Equations

• ConnesRigidity.CarryBidualInternal.vectorDiscreteTopology = ⊥

theorem ConnesRigidity.CarryBidualInternal.vectorDiscrete : DiscreteTopology V

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

@[instance_reducible]

def ConnesRigidity.CarryBidualInternal.dividedSquareDiscreteTopology : TopologicalSpace ↥B

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

Equations

• ConnesRigidity.CarryBidualInternal.dividedSquareDiscreteTopology = ⊥

theorem ConnesRigidity.CarryBidualInternal.dividedSquareDiscrete : DiscreteTopology ↥B

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

theorem ConnesRigidity.carryBidualEvaluation_surjective (n : ℕ) : Function.Surjective (carryBidualEvaluation n)

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

noncomputable def ConnesRigidity.carryBidualEquiv (n : ℕ) : CarryGroup n ≃ PontryaginDual (Multiplicative (E n))

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

Equations

• ConnesRigidity.carryBidualEquiv n = Equiv.ofBijective (ConnesRigidity.carryBidualEvaluation n) ⋯

noncomputable def ConnesRigidity.carryBidualHomeomorph (n : ℕ) : CarryGroup n ≃ₜ PontryaginDual (Multiplicative (E n))

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

Equations

• ConnesRigidity.carryBidualHomeomorph n = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem ConnesRigidity.carryBidualHomeomorph_apply (n : ℕ) (z : CarryGroup n) (η : E n) : ((carryBidualHomeomorph n) z) (Multiplicative.ofAdd η) = (Additive.toMul η) (Multiplicative.ofAdd z)

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

noncomputable def ConnesRigidity.splitBinaryEvaluation (d : D) : X × Y →+ F

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

Equations

• ConnesRigidity.splitBinaryEvaluation d = { toFun := fun (z : ConnesRigidity.X × ConnesRigidity.Y) => z.1 d.1 + z.2 d.2, map_zero' := ⋯, map_add' := ⋯ }

theorem ConnesRigidity.continuous_splitBinaryEvaluation (d : D) : Continuous ⇑(splitBinaryEvaluation d)

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

noncomputable def ConnesRigidity.splitPontryaginCharacter (d : D) : PontryaginDual (Multiplicative (X × Y))

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

Equations

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

noncomputable def ConnesRigidity.splitComplexCharacter (d : D) : C(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.splitComplexCharacter_zero : splitComplexCharacter 0 = 1

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

theorem ConnesRigidity.splitComplexCharacter_span_closure_eq_top : (Submodule.span ℂ (Set.range splitComplexCharacter)).topologicalClosure = ⊤

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

noncomputable def ConnesRigidity.splitCharacterL2 (d : D) : ↥(MeasureTheory.Lp ℂ 2 productHaar)

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

Equations

• ConnesRigidity.splitCharacterL2 d = (ContinuousMap.toLp 2 ConnesRigidity.productHaar ℂ) (ConnesRigidity.splitComplexCharacter d)

theorem ConnesRigidity.splitCharacterL2_span_closure_eq_top : (Submodule.span ℂ (Set.range splitCharacterL2)).topologicalClosure = ⊤

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

theorem ConnesRigidity.splitCharacterL2_orthonormal : Orthonormal ℂ splitCharacterL2

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

noncomputable def ConnesRigidity.splitFourierBasis : HilbertBasis D ℂ ↥(MeasureTheory.Lp ℂ 2 productHaar)

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

Equations

• ConnesRigidity.splitFourierBasis = HilbertBasis.mk ConnesRigidity.splitCharacterL2_orthonormal ConnesRigidity.splitFourierBasis._proof_4

noncomputable def ConnesRigidity.splitFourierTransform : ↥(lp (fun (x : D) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 productHaar)

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

Equations

• ConnesRigidity.splitFourierTransform = ConnesRigidity.splitFourierBasis.repr.symm

@[reducible, inline]

noncomputable abbrev ConnesRigidity.splitFourierEquiv : ↥(lp (fun (x : D) => ℂ) 2) ≃ₗᵢ[ℂ] ↥(MeasureTheory.Lp ℂ 2 productHaar)

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

Equations

• ConnesRigidity.splitFourierEquiv = ConnesRigidity.splitFourierTransform

theorem ConnesRigidity.splitFourierEquiv_single [DecidableEq D] (d : D) : splitFourierEquiv (lp.single 2 d 1) = splitCharacterL2 d

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

theorem ConnesRigidity.groupFactorsIsomorphic_symm {G : CountableDiscreteGroup} {H : CountableDiscreteGroup} (h : TracialGroupFactorsIsomorphic G H) : TracialGroupFactorsIsomorphic H G

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

theorem ConnesRigidity.groupFactorsIsomorphic_trans {G : CountableDiscreteGroup} {H : CountableDiscreteGroup} {J : CountableDiscreteGroup} (hGH : TracialGroupFactorsIsomorphic G H) (hHJ : TracialGroupFactorsIsomorphic H J) : TracialGroupFactorsIsomorphic G J

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

structure ConnesRigidity.HaarProbabilityAction (K : Type u) (Ω : Type v) [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] : Type (max u v)

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

• measure : MeasureTheory.Measure Ω

  The invariant probability measure.

• haar : self.measure.IsAddHaarMeasure
• probability : MeasureTheory.IsProbabilityMeasure self.measure
• action : K →* Equiv.Perm Ω

  The group action on the measured group.

• action_add (k : K) (z z' : Ω) : (self.action k) (z + z') = (self.action k) z + (self.action k) z'
• action_preserves_measure (k : K) : MeasureTheory.MeasurePreserving (⇑(self.action k)) self.measure self.measure

structure ConnesRigidity.EquivariantHaarEquiv {K : Type u} {Ω : Type v} {Ξ : Type w} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] (X : HaarProbabilityAction K Ω) (Y : HaarProbabilityAction K Ξ) : Type (max v w)

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

• toMeasurableEquiv : Ω ≃ᵐ Ξ

  The underlying measurable equivalence.

• measure_preserving : MeasureTheory.MeasurePreserving (⇑self.toMeasurableEquiv) X.measure Y.measure
• equivariant (k : K) (z : Ω) : self.toMeasurableEquiv ((X.action k) z) = (Y.action k) (self.toMeasurableEquiv z)

def ConnesRigidity.EquivariantHaarEquiv.refl {K : Type u} {Ω : Type v} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : EquivariantHaarEquiv X X

The identity equivariant equivalence.

Equations

• ConnesRigidity.EquivariantHaarEquiv.refl X = { toMeasurableEquiv := MeasurableEquiv.refl Ω, measure_preserving := ⋯, equivariant := ⋯ }

def ConnesRigidity.EquivariantHaarEquiv.symm {K : Type u} {Ω : Type v} {Ξ : Type w} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) : EquivariantHaarEquiv Y X

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

Equations

• e.symm = { toMeasurableEquiv := e.toMeasurableEquiv.symm, measure_preserving := ⋯, equivariant := ⋯ }

def ConnesRigidity.EquivariantHaarEquiv.trans {K : Type u} {Ω : Type v} {Ξ : Type w} {Ζ : Type x} [Group K] [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] [AddCommGroup Ζ] [TopologicalSpace Ζ] [MeasurableSpace Ζ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} {Z : HaarProbabilityAction K Ζ} (e : EquivariantHaarEquiv X Y) (f : EquivariantHaarEquiv Y Z) : EquivariantHaarEquiv X Z

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

Equations

• e.trans f = { toMeasurableEquiv := e.toMeasurableEquiv.trans f.toMeasurableEquiv, measure_preserving := ⋯, equivariant := ⋯ }

structure ConnesRigidity.CrossedProductModel (ℋ : Type v) [NormedAddCommGroup ℋ] [InnerProductSpace ℂ ℋ] [CompleteSpace ℋ] : Type v

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

• algebra : VonNeumannAlgebra ℋ

  The modeled von Neumann algebra.

• trace : ↥self.algebra.toStarSubalgebra → ℂ

  The trace on the modeled algebra.

instance ConnesRigidity.instCountableSubtypeTMemSubmoduleFB : Countable ↥B

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

instance ConnesRigidity.instCountableD : Countable D

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

instance ConnesRigidity.instCountableMultiplicativeD : Countable (Multiplicative D)

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

noncomputable def ConnesRigidity.kLinear : ↥K →* V ≃ₗ[F] V

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

Equations

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

noncomputable def ConnesRigidity.kTensorLinear : ↥K →* T ≃ₗ[F] T

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

Equations

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

theorem ConnesRigidity.kTensorLinear_map_B (k : ↥K) : Submodule.map (↑(kTensorLinear k)) B = B

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

noncomputable def ConnesRigidity.kDividedSquareLinear : ↥K →* ↥B ≃ₗ[F] ↥B

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.kDividedSquareLinear_val (k : ↥K) (b : ↥B) : ↑((kDividedSquareLinear k) b) = (kTensorLinear k) ↑b

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

@[simp]

theorem ConnesRigidity.kDividedSquareLinear_diagonal (k : ↥K) (v : V) : (kDividedSquareLinear k) (diagonal v) = diagonal ((kLinear k) v)

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

noncomputable def ConnesRigidity.kDLinear : ↥K →* D ≃ₗ[F] D

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

Equations

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

noncomputable def ConnesRigidity.kDAction : ↥K →* MulAut (Multiplicative D)

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

Equations

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

@[reducible, inline]

abbrev ConnesRigidity.Lambda : Type

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

Equations

• ConnesRigidity.Lambda = (Multiplicative ConnesRigidity.D ⋊[ConnesRigidity.kDAction] ↥ConnesRigidity.K)

instance ConnesRigidity.instCountableLambda : Countable Lambda

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

noncomputable def ConnesRigidity.lambdaGroup : CountableDiscreteGroup

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

Equations

• ConnesRigidity.lambdaGroup = { Carrier := ConnesRigidity.Lambda, group := inferInstance, countable := ConnesRigidity.lambdaGroup._proof_1 }

@[reducible, inline]

noncomputable abbrev ConnesRigidity.lambdaInl : Multiplicative D →* Lambda

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

Equations

• ConnesRigidity.lambdaInl = SemidirectProduct.inl

@[reducible, inline]

noncomputable abbrev ConnesRigidity.lambdaInr : ↥K →* Lambda

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

Equations

• ConnesRigidity.lambdaInr = SemidirectProduct.inr

@[reducible, inline]

noncomputable abbrev ConnesRigidity.lambdaProjection : Lambda →* ↥K

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

Equations

• ConnesRigidity.lambdaProjection = SemidirectProduct.rightHom

theorem ConnesRigidity.lambda_conjugation (k : ↥K) (d : Multiplicative D) : lambdaInl ((kDAction k) d) = lambdaInr k * lambdaInl d * (lambdaInr k)⁻¹

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

structure ConnesRigidity.GroupCardinalInvariant : Type (u + 1)

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

• carrier : CountableDiscreteGroup → Type u

  The type assigned to each group.

• mapMulEquiv {G H : CountableDiscreteGroup} : G.Carrier ≃* H.Carrier → self.carrier G ≃ self.carrier H

  Transport of the invariant along a group equivalence.

noncomputable def ConnesRigidity.GroupCardinalInvariant.value (I : GroupCardinalInvariant) (G : CountableDiscreteGroup) : ℕ

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

Equations

• I.value G = Nat.card (I.carrier G)

theorem ConnesRigidity.GroupCardinalInvariant.value_mulEquiv (I : GroupCardinalInvariant) {G H : CountableDiscreteGroup} (e : G.Carrier ≃* H.Carrier) : I.value G = I.value H

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

structure ConnesRigidity.ExactIndexEmbedding (G H : CountableDiscreteGroup) (index : ℕ) : Type u

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

• hom : G.Carrier →* H.Carrier

  The underlying group homomorphism.

• injective : Function.Injective ⇑self.hom
• index_eq : self.hom.range.index = index

def ConnesRigidity.AbstractlyCommensurable (G H : CountableDiscreteGroup) : Prop

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

Equations

• ConnesRigidity.AbstractlyCommensurable G H = ∃ (S : Subgroup G.Carrier) (T : Subgroup H.Carrier), S.FiniteIndex ∧ T.FiniteIndex ∧ Nonempty (↥S ≃* ↥T)

theorem ConnesRigidity.not_groupsIsomorphic_of_orderFour {G H : CountableDiscreteGroup} (hG : ∃ (g : G.Carrier), orderOf g = 4) (hH : ∀ (h : H.Carrier), orderOf h ≠ 4) : ¬GroupsIsomorphic G H

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

structure ConnesRigidity.PaperFamilyInput : Type (u + 1)

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

• Lambda : CountableDiscreteGroup

  The distinguished group in the family.

• Gamma : ℕ → CountableDiscreteGroup

  The indexed groups in the family.

• invariant : GroupCardinalInvariant

  The cardinal invariant separating the indexed groups.

• invariant_card (n : ℕ) : self.invariant.value (self.Gamma n) = 2 ^ (4 * n)
• lambda_no_order_four (g : self.Lambda.Carrier) : orderOf g ≠ 4
• gamma_order_four (n : ℕ) : ∃ (g : (self.Gamma n).Carrier), orderOf g = 4
• lambda_fg : Group.FG self.Lambda.Carrier
• gamma_fg (n : ℕ) : Group.FG (self.Gamma n).Carrier
• lambda_icc : IsICC self.Lambda
• gamma_icc (n : ℕ) : IsICC (self.Gamma n)
• lambda_propertyT : HasKazhdanPropertyT self.Lambda
• gamma_propertyT (n : ℕ) : HasKazhdanPropertyT (self.Gamma n)
• factors_isomorphic (n : ℕ) : TracialGroupFactorsIsomorphic (self.Gamma n) self.Lambda
• embeddings (n : ℕ) : ExactIndexEmbedding (self.Gamma 0) (self.Gamma n) (2 ^ (4 * n))

  Exact-index embeddings from the first group into every indexed group.

theorem ConnesRigidity.PaperFamilyInput.gamma_not_isomorphic (F : PaperFamilyInput) {m n : ℕ} (hmn : m ≠ n) : ¬GroupsIsomorphic (F.Gamma m) (F.Gamma n)

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

theorem ConnesRigidity.PaperFamilyInput.gamma_not_isomorphic_lambda (F : PaperFamilyInput) (n : ℕ) : ¬GroupsIsomorphic (F.Gamma n) F.Lambda

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

theorem ConnesRigidity.PaperFamilyInput.lambda_not_isomorphic_gamma (F : PaperFamilyInput) (n : ℕ) : ¬GroupsIsomorphic F.Lambda (F.Gamma n)

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

theorem ConnesRigidity.PaperFamilyInput.gamma_commensurable (F : PaperFamilyInput) (m n : ℕ) : AbstractlyCommensurable (F.Gamma m) (F.Gamma n)

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

structure ConnesRigidity.InfinitePropertyTFiber : Type (u + 1)

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

• Lambda : CountableDiscreteGroup

  The distinguished group in the fiber.

• Gamma : ℕ → CountableDiscreteGroup

  The infinite sequence of groups in the fiber.

• lambda_fg : Group.FG self.Lambda.Carrier
• gamma_fg (n : ℕ) : Group.FG (self.Gamma n).Carrier
• lambda_icc : IsICC self.Lambda
• gamma_icc (n : ℕ) : IsICC (self.Gamma n)
• lambda_propertyT : HasKazhdanPropertyT self.Lambda
• gamma_propertyT (n : ℕ) : HasKazhdanPropertyT (self.Gamma n)
• factors_isomorphic (n : ℕ) : TracialGroupFactorsIsomorphic (self.Gamma n) self.Lambda
• gamma_pairwise_nonisomorphic {m n : ℕ} : m ≠ n → ¬GroupsIsomorphic (self.Gamma m) (self.Gamma n)
• lambda_not_isomorphic (n : ℕ) : ¬GroupsIsomorphic self.Lambda (self.Gamma n)
• exactIndexEmbeddings (n : ℕ) : ExactIndexEmbedding (self.Gamma 0) (self.Gamma n) (2 ^ (4 * n))

  Exact-index embeddings from the first group into every indexed group.

• commensurable (m n : ℕ) : AbstractlyCommensurable (self.Gamma m) (self.Gamma n)

def ConnesRigidity.PaperFamilyInput.toInfinitePropertyTFiber (F : PaperFamilyInput) : InfinitePropertyTFiber

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

Equations

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

noncomputable def ConnesRigidity.kXLinear : ↥K →* X ≃ₗ[F] X

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

Equations

• ConnesRigidity.kXLinear = { toFun := fun (k : ↥ConnesRigidity.K) => (ConnesRigidity.kLinear k⁻¹).dualMap, map_one' := ConnesRigidity.kXLinear._proof_1, map_mul' := ⋯ }

@[simp]

theorem ConnesRigidity.kXLinear_apply (k : ↥K) (ℓ : X) (v : V) : ((kXLinear k) ℓ) v = ℓ ((kLinear k⁻¹) v)

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

noncomputable def ConnesRigidity.kYLinear : ↥K →* Y ≃ₗ[F] Y

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

Equations

• ConnesRigidity.kYLinear = { toFun := fun (k : ↥ConnesRigidity.K) => (ConnesRigidity.kDividedSquareLinear k⁻¹).dualMap, map_one' := ConnesRigidity.kYLinear._proof_1, map_mul' := ⋯ }

@[simp]

theorem ConnesRigidity.kYLinear_apply (k : ↥K) (q : Y) (b : ↥B) : ((kYLinear k) q) b = q ((kDividedSquareLinear k⁻¹) b)

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

theorem ConnesRigidity.kXLinear_shift (k : ↥K) (n : ℕ) (ℓ : X) : (shift n) ((kXLinear k) ℓ) = (kXLinear k) ((shift n) ℓ)

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

noncomputable def ConnesRigidity.kCarryAddAut (n : ℕ) (k : ↥K) : AddAut (CarryGroup n)

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

Equations

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

noncomputable def ConnesRigidity.kCarryAction (n : ℕ) : ↥K →* MulAut (Multiplicative (CarryGroup n))

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

Equations

• ConnesRigidity.kCarryAction n = { toFun := fun (k : ↥ConnesRigidity.K) => AddEquiv.toMultiplicative (ConnesRigidity.kCarryAddAut n k), map_one' := ⋯, map_mul' := ⋯ }

theorem ConnesRigidity.continuous_kCarryAction (n : ℕ) (k : ↥K) : Continuous ⇑((kCarryAction n) k)

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

noncomputable def ConnesRigidity.kEAction (n : ℕ) : ↥K →* MulAut (Multiplicative (E n))

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

Equations

• ConnesRigidity.kEAction n = id (ConnesRigidity.dualAction (Multiplicative (ConnesRigidity.CarryGroup n)) (↥ConnesRigidity.K) (ConnesRigidity.kCarryAction n) ⋯)

@[simp]

theorem ConnesRigidity.kEAction_apply (n : ℕ) (k : ↥K) (η : Multiplicative (E n)) (z : Multiplicative (CarryGroup n)) : (Additive.toMul (Multiplicative.toAdd (((kEAction n) k) η))) z = (Additive.toMul (Multiplicative.toAdd η)) (((kCarryAction n) k)⁻¹ z)

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

instance ConnesRigidity.instMultiplicativeECountable (n : ℕ) : Countable (Multiplicative (E n))

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

@[reducible, inline]

abbrev ConnesRigidity.Gamma (n : ℕ) : Type

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

Equations

• ConnesRigidity.Gamma n = (Multiplicative (ConnesRigidity.E n) ⋊[ConnesRigidity.kEAction n] ↥ConnesRigidity.K)

instance ConnesRigidity.instGammaCountable (n : ℕ) : Countable (Gamma n)

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

noncomputable def ConnesRigidity.gammaGroup (n : ℕ) : CountableDiscreteGroup

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

Equations

• ConnesRigidity.gammaGroup n = { Carrier := ConnesRigidity.Gamma n, group := inferInstance, countable := ⋯ }

theorem ConnesRigidity.gamma_has_order_four (n : ℕ) : ∃ (g : (gammaGroup n).Carrier), orderOf g = 4

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

noncomputable def ConnesRigidity.paperSplitAddAut (k : ↥K) : X × Y ≃+ X × Y

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

Equations

• ConnesRigidity.paperSplitAddAut k = (ConnesRigidity.kXLinear k).toAddEquiv.prodCongr (ConnesRigidity.kYLinear k).toAddEquiv

noncomputable def ConnesRigidity.paperSplitPerm : ↥K →* Equiv.Perm (X × Y)

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

Equations

• ConnesRigidity.paperSplitPerm = { toFun := fun (k : ↥ConnesRigidity.K) => (ConnesRigidity.paperSplitAddAut k).toEquiv, map_one' := ConnesRigidity.paperSplitPerm._proof_1, map_mul' := ⋯ }

noncomputable def ConnesRigidity.paperSplitHaarAction : HaarProbabilityAction (↥K) (X × Y)

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

Equations

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

noncomputable def ConnesRigidity.paperCarryPerm (n : ℕ) : ↥K →* Equiv.Perm (CarryGroup n)

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

Equations

• ConnesRigidity.paperCarryPerm n = { toFun := fun (k : ↥ConnesRigidity.K) => (ConnesRigidity.kCarryAddAut n k).toEquiv, map_one' := ⋯, map_mul' := ⋯ }

theorem ConnesRigidity.paperCarryPerm_add (n : ℕ) (k : ↥K) (z z' : CarryGroup n) : ((paperCarryPerm n) k) (z + z') = ((paperCarryPerm n) k) z + ((paperCarryPerm n) k) z'

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

noncomputable def ConnesRigidity.paperCarryHaarAction (n : ℕ) : HaarProbabilityAction (↥K) (CarryGroup n)

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

Equations

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

noncomputable def ConnesRigidity.paperCommonHaarEquiv (n : ℕ) : EquivariantHaarEquiv (paperCarryHaarAction n) paperSplitHaarAction

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

Equations

• ConnesRigidity.paperCommonHaarEquiv n = { toMeasurableEquiv := ConnesRigidity.carryCoordinatesMeasurableEquiv n, measure_preserving := ⋯, equivariant := ⋯ }

@[reducible, inline]

noncomputable abbrev ConnesRigidity.crossedBaseHilbert {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : AddSubgroup (Ω →ₘ[X.measure] ℂ)

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

Equations

• ConnesRigidity.crossedBaseHilbert X = MeasureTheory.Lp ℂ 2 X.measure

@[reducible, inline]

noncomputable abbrev ConnesRigidity.crossedHilbert {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : AddSubgroup (PreLp fun (x : K) => ↥(crossedBaseHilbert X))

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

Equations

• ConnesRigidity.crossedHilbert X = lp (fun (x : K) => ↥(ConnesRigidity.crossedBaseHilbert X)) 2

@[reducible, inline]

noncomputable abbrev ConnesRigidity.crossedCoefficient {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : AddSubgroup (Ω →ₘ[X.measure] ℂ)

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

Equations

• ConnesRigidity.crossedCoefficient X = MeasureTheory.Lp ℂ ⊤ X.measure

noncomputable def ConnesRigidity.crossedBaseMultiplier {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (f : ↥(crossedCoefficient X)) : ↥(crossedBaseHilbert X) →L[ℂ] ↥(crossedBaseHilbert X)

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

Equations

• ConnesRigidity.crossedBaseMultiplier X f = (ContinuousLinearMap.holderL X.measure ⊤ 2 2 (ContinuousLinearMap.mul ℂ ℂ)) f

noncomputable def ConnesRigidity.crossedFiberwiseOperator {K : Type u} {H : Type v} [NormedAddCommGroup H] [NormedSpace ℂ H] (T : H →L[ℂ] H) : ↥(lp (fun (x : K) => H) 2) →L[ℂ] ↥(lp (fun (x : K) => H) 2)

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

Equations

• ConnesRigidity.crossedFiberwiseOperator T = { toFun := fun (ξ : ↥(lp (fun (x : K) => H) 2)) => ⟨fun (k : K) => T (↑ξ k), ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous ‖T‖ ⋯

@[simp]

theorem ConnesRigidity.crossedFiberwiseOperator_apply {K : Type u} {H : Type v} [NormedAddCommGroup H] [NormedSpace ℂ H] (T : H →L[ℂ] H) (ξ : ↥(lp (fun (x : K) => H) 2)) (k : K) : ↑((crossedFiberwiseOperator T) ξ) k = T (↑ξ k)

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

noncomputable def ConnesRigidity.crossedMultiplier {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (f : ↥(crossedCoefficient X)) : ↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X)

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

Equations

• ConnesRigidity.crossedMultiplier X f = ConnesRigidity.crossedFiberwiseOperator (ConnesRigidity.crossedBaseMultiplier X f)

def ConnesRigidity.crossedFiberwiseEquiv {K : Type u} {H : Type v} {J : Type w} [NormedAddCommGroup H] [NormedSpace ℂ H] [NormedAddCommGroup J] [NormedSpace ℂ J] (e : H ≃ₗᵢ[ℂ] J) : ↥(lp (fun (x : K) => H) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : K) => J) 2)

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

Equations

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

def ConnesRigidity.crossedIndexEquiv {K : Type u} {H : Type v} [NormedAddCommGroup H] [NormedSpace ℂ H] (e : K ≃ K) : ↥(lp (fun (x : K) => H) 2) ≃ₗᵢ[ℂ] ↥(lp (fun (x : K) => H) 2)

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

Equations

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

noncomputable def ConnesRigidity.crossedBaseHaarEquiv {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) : ↥(crossedBaseHilbert X) ≃ₗᵢ[ℂ] ↥(crossedBaseHilbert Y)

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

Equations

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

noncomputable def ConnesRigidity.crossedActionL2Equiv {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (k : K) : ↥(crossedBaseHilbert X) ≃ₗᵢ[ℂ] ↥(crossedBaseHilbert X)

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

Equations

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

noncomputable def ConnesRigidity.crossedGroupUnitary {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) (k : K) : ↥(crossedHilbert X) ≃ₗᵢ[ℂ] ↥(crossedHilbert X)

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

Equations

• ConnesRigidity.crossedGroupUnitary X k = (ConnesRigidity.crossedIndexEquiv (Equiv.mulLeft k)).trans (ConnesRigidity.crossedFiberwiseEquiv (ConnesRigidity.crossedActionL2Equiv X k))

def ConnesRigidity.crossedGeneratorSet {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : Set (↥(crossedHilbert X) →L[ℂ] ↥(crossedHilbert X))

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

Equations

• ConnesRigidity.crossedGeneratorSet X = Set.range (ConnesRigidity.crossedMultiplier X) ∪ Set.range fun (k : K) => ↑↑(ConnesRigidity.crossedGroupUnitary X k)

noncomputable def ConnesRigidity.crossedVacuum {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : ↥(crossedHilbert X)

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

Equations

• ConnesRigidity.crossedVacuum X = lp.single 2 1 ((MeasureTheory.Lp.const 2 X.measure) 1)

noncomputable def ConnesRigidity.crossedProductModel {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] (X : HaarProbabilityAction K Ω) : CrossedProductModel ↥(crossedHilbert X)

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

Equations

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

noncomputable def ConnesRigidity.crossedHaarHilbertEquiv {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) : ↥(crossedHilbert X) ≃ₗᵢ[ℂ] ↥(crossedHilbert Y)

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

Equations

• ConnesRigidity.crossedHaarHilbertEquiv e = ConnesRigidity.crossedFiberwiseEquiv (ConnesRigidity.crossedBaseHaarEquiv e)

theorem ConnesRigidity.crossedHaarHilbertEquiv_vacuum {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) : (crossedHaarHilbertEquiv e) (crossedVacuum X) = crossedVacuum Y

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

theorem ConnesRigidity.crossedBaseHaarEquiv_multiplier_apply {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) (f : ↥(crossedCoefficient X)) (ξ : ↥(crossedBaseHilbert X)) : (crossedBaseHaarEquiv e) ((crossedBaseMultiplier X f) ξ) = (crossedBaseMultiplier Y ((MeasureTheory.Lp.compMeasurePreserving ⇑e.toMeasurableEquiv.symm ⋯) f)) ((crossedBaseHaarEquiv e) ξ)

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

theorem ConnesRigidity.crossedHaarHilbertEquiv_group_conj {K : Type u} [Group K] {Ω : Type v} [AddCommGroup Ω] [TopologicalSpace Ω] [MeasurableSpace Ω] {Ξ : Type w} [AddCommGroup Ξ] [TopologicalSpace Ξ] [MeasurableSpace Ξ] {X : HaarProbabilityAction K Ω} {Y : HaarProbabilityAction K Ξ} (e : EquivariantHaarEquiv X Y) (k : K) : (crossedHaarHilbertEquiv e).conjStarAlgEquiv ↑↑(crossedGroupUnitary X k) = ↑↑(crossedGroupUnitary Y k)

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

noncomputable def ConnesRigidity.carryCharacterFunction (n : ℕ) (η : E n) : CarryGroup n → ℂ

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

Equations

• ConnesRigidity.carryCharacterFunction n η z = ↑((Additive.toMul η) (Multiplicative.ofAdd z))

theorem ConnesRigidity.measurable_carryCharacterFunction (n : ℕ) (η : E n) : Measurable (carryCharacterFunction n η)

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

theorem ConnesRigidity.norm_carryCharacterFunction (n : ℕ) (η : E n) (z : CarryGroup n) : ‖carryCharacterFunction n η z‖ = 1

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

noncomputable def ConnesRigidity.carryCharacterCoefficient (n : ℕ) (η : E n) : ↥(crossedCoefficient (paperCarryHaarAction n))

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

Equations

• ConnesRigidity.carryCharacterCoefficient n η = MeasureTheory.MemLp.toLp (ConnesRigidity.carryCharacterFunction n η) ⋯

theorem ConnesRigidity.carryCharacterCoefficient_apply_ae (n : ℕ) (η : E n) : ↑↑(carryCharacterCoefficient n η) =ᵐ[carryHaar n] carryCharacterFunction n η

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

theorem ConnesRigidity.carryCharacterMultiplier_character (n : ℕ) (η θ : E n) : (crossedBaseMultiplier (paperCarryHaarAction n) (carryCharacterCoefficient n η)) (carryCharacterL2 n θ) = carryCharacterL2 n (η + θ)

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

noncomputable def ConnesRigidity.splitCharacterFunction (d : D) : X × Y → ℂ

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

Equations

• ConnesRigidity.splitCharacterFunction d z = ↑((ConnesRigidity.splitPontryaginCharacter d) (Multiplicative.ofAdd z))

theorem ConnesRigidity.measurable_splitCharacterFunction (d : D) : Measurable (splitCharacterFunction d)

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

theorem ConnesRigidity.norm_splitCharacterFunction (d : D) (z : X × Y) : ‖splitCharacterFunction d z‖ = 1

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

noncomputable def ConnesRigidity.splitCharacterCoefficient (d : D) : ↥(crossedCoefficient paperSplitHaarAction)

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

Equations

• ConnesRigidity.splitCharacterCoefficient d = MeasureTheory.MemLp.toLp (ConnesRigidity.splitCharacterFunction d) ⋯

theorem ConnesRigidity.splitCharacterCoefficient_apply_ae (d : D) : ↑↑(splitCharacterCoefficient d) =ᵐ[productHaar] splitCharacterFunction d

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

theorem ConnesRigidity.splitCharacterMultiplier_character (d e : D) : (crossedBaseMultiplier paperSplitHaarAction (splitCharacterCoefficient d)) (splitCharacterL2 e) = splitCharacterL2 (d + e)

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

theorem ConnesRigidity.carryFourierEquiv_zero_single (n : ℕ) [DecidableEq (E n)] : (carryFourierEquiv n) (lp.single 2 0 1) = (MeasureTheory.Lp.const 2 (carryHaar n)) 1

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

noncomputable def ConnesRigidity.carryEAddAction (n : ℕ) (k : ↥K) : E n ≃+ E n

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

Equations

• ConnesRigidity.carryEAddAction n k = MulEquiv.toAdditive ((ConnesRigidity.kEAction n) k)

theorem ConnesRigidity.carryFourier_kEAction (n : ℕ) (k : ↥K) (ξ : ↥(GroupL2 (E n))) : (carryFourierEquiv n) ((l2Reindex (carryEAddAction n k).toEquiv) ξ) = (crossedActionL2Equiv (paperCarryHaarAction n) k) ((carryFourierEquiv n) ξ)

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

noncomputable def ConnesRigidity.unitCoefficient {Ω : Type u} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (u : Ω → ℂ) (hu : Measurable u) (hunit : ∀ (x : Ω), ‖u x‖ = 1) : ↥(MeasureTheory.Lp ℂ ⊤ μ)

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

Equations

• ConnesRigidity.unitCoefficient μ u hu hunit = MeasureTheory.MemLp.toLp u ⋯

noncomputable def ConnesRigidity.unitMultiplier {Ω : Type u} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (u : Ω → ℂ) (hu : Measurable u) (hunit : ∀ (x : Ω), ‖u x‖ = 1) : ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)

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

Equations

• ConnesRigidity.unitMultiplier μ u hu hunit = (ContinuousLinearMap.holderL μ ⊤ 2 2 (ContinuousLinearMap.mul ℂ ℂ)) (ConnesRigidity.unitCoefficient μ u hu hunit)

noncomputable def ConnesRigidity.continuousMultiplier {Ω : Type u} [TopologicalSpace Ω] [CompactSpace Ω] [MeasurableSpace Ω] [BorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] : C(Ω, ℂ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)

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

Equations

• ConnesRigidity.continuousMultiplier μ = ContinuousLinearMap.holderL μ ⊤ 2 2 (ContinuousLinearMap.mul ℂ ℂ) ∘SL ContinuousMap.toLp ⊤ μ ℂ

theorem ConnesRigidity.commute_unitMultiplier_of_commute_characters {Ω : Type u} [TopologicalSpace Ω] [CompactSpace Ω] [T2Space Ω] [SecondCountableTopology Ω] [MeasurableSpace Ω] [BorelSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] [μ.WeaklyRegular] {ι : Type u_1} (χ : ι → C(Ω, ℂ)) (hdense : (Submodule.span ℂ (Set.range χ)).topologicalClosure = ⊤) (T : ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)) (hT : ∀ (i : ι), Commute T ((continuousMultiplier μ) (χ i))) (u : Ω → ℂ) (hu : Measurable u) (hunit : ∀ (x : Ω), ‖u x‖ = 1) : Commute T (unitMultiplier μ u hu hunit)

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

theorem ConnesRigidity.commute_multiplier_of_commute_units {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (T : ↥(MeasureTheory.Lp ℂ 2 μ) →L[ℂ] ↥(MeasureTheory.Lp ℂ 2 μ)) (hT : ∀ (u : Ω → ℂ) (hu : Measurable u) (hunit : ∀ (x : Ω), ‖u x‖ = 1), Commute T (unitMultiplier μ u hu hunit)) (f : ↥(MeasureTheory.Lp ℂ ⊤ μ)) : Commute T ((ContinuousLinearMap.holderL μ ⊤ 2 2 (ContinuousLinearMap.mul ℂ ℂ)) f)

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