The binary pontryagin dual component of the Connes rigidity formalization.

@[reducible, inline]

abbrev Connes.BinaryPontryaginDual.F : Type

The F construction used in the Connes rigidity formalization.

Equations

• Connes.BinaryPontryaginDual.F = ZMod 2

@[reducible]

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

The pointwiseDualTopology construction used in the Connes rigidity formalization.

Equations

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

@[instance_reducible]

def Connes.BinaryPontryaginDual.instPointwiseDualTopology {M : Type u_1} [AddCommGroup M] [Module F M] : TopologicalSpace (M →ₗ[F] F)

The instPointwiseDualTopology construction used in the Connes rigidity formalization.

Equations

• Connes.BinaryPontryaginDual.instPointwiseDualTopology = Connes.BinaryPontryaginDual.pointwiseDualTopology M

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

The two-valued character group is identified with the binary roots. Paper: §3.

Equations

• Connes.BinaryPontryaginDual.binaryRootsEquiv = MulEquiv.ofBijective (AddChar.toMonoidHomEquiv (ZMod.rootsOfUnityAddChar 2)) Connes.BinaryPontryaginDual.binaryRootsEquiv._proof_3

@[simp]

theorem Connes.BinaryPontryaginDual.binaryRootsEquiv_apply (a : F) : binaryRootsEquiv (Multiplicative.ofAdd a) = (ZMod.rootsOfUnityAddChar 2) a

@[simp]

theorem Connes.BinaryPontryaginDual.binaryRootsEquiv_val (a : Multiplicative F) : ↑↑(binaryRootsEquiv a) = ZMod.toCircle (Multiplicative.toAdd a)

theorem Connes.BinaryPontryaginDual.character_sq (M : Type u_1) [AddCommGroup M] [Module F M] [TopologicalSpace M] (χ : PontryaginDual (Multiplicative M)) (x : Multiplicative M) : χ x ^ 2 = 1

Binary characters have order dividing two. Paper: §3.

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

The characterIntoRoots construction used in the Connes rigidity formalization.

Equations

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

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

The additive binary character underlying a Pontryagin character. Paper: §3.

Equations

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

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

The linear form underlying a Pontryagin character. Paper: §3.

Equations

• Connes.BinaryPontryaginDual.characterLinear χ = AddMonoidHom.toZModLinearMap 2 (Connes.BinaryPontryaginDual.characterAdd χ)

@[simp]

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

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

The extracted linear character is continuous in the pointwise dual topology. Paper: §3.

theorem Connes.BinaryPontryaginDual.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

def Connes.BinaryPontryaginDual.continuousBinaryBidual (M : Type u_1) [AddCommGroup M] [Module F M] : Submodule F ((M →ₗ[F] F) →ₗ[F] F)

The continuousBinaryBidual construction used in the Connes rigidity formalization.

Equations

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

def Connes.BinaryPontryaginDual.continuousBinaryBidualEvaluation (M : Type u_1) [AddCommGroup M] [Module F M] : M →ₗ[F] ↥(continuousBinaryBidual M)

The continuousBinaryBidualEvaluation construction used in the Connes rigidity formalization.

Equations

• Connes.BinaryPontryaginDual.continuousBinaryBidualEvaluation M = { toFun := fun (m : M) => ⟨(Module.Dual.eval Connes.BinaryPontryaginDual.F M) m, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem Connes.BinaryPontryaginDual.continuousBinaryBidualEvaluation_apply (M : Type u_1) [AddCommGroup M] [Module F M] (m : M) (ℓ : M →ₗ[F] F) : ↑((continuousBinaryBidualEvaluation M) m) ℓ = ℓ m

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

The binary Pontryagin dual of a linear dual is its evaluation module. Paper: §3.

Equations

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

@[simp]

theorem Connes.BinaryPontryaginDual.pointwiseEvaluationCharacter_apply (M : Type u_1) [AddCommGroup M] [Module F M] (m : M) (ℓ : M →ₗ[F] F) : (pointwiseEvaluationCharacter M m) (Multiplicative.ofAdd ℓ) = ZMod.toCircle (ℓ m)

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

The pointwiseEvaluationHom construction used in the Connes rigidity formalization.

Equations

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

@[simp]

theorem Connes.BinaryPontryaginDual.pointwiseEvaluationHom_apply (M : Type u_1) [AddCommGroup M] [Module F M] (m : M) (ℓ : M →ₗ[F] F) : (Additive.toMul ((pointwiseEvaluationHom M) m)) (Multiplicative.ofAdd ℓ) = ZMod.toCircle (ℓ m)

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

The Pontryagin dual isomorphism used by the Zhou Fourier model. Paper: §3.

Equations

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

@[simp]

theorem Connes.BinaryPontryaginDual.pointwisePontryaginDualEquiv_symm_apply (M : Type u_1) [AddCommGroup M] [Module F M] (m : M) : (pointwisePontryaginDualEquiv M).symm m = (pointwiseEvaluationHom M) m

@[simp]

theorem Connes.BinaryPontryaginDual.pointwisePontryaginDualEquiv_apply_character (M : Type u_1) [AddCommGroup M] [Module F M] (χ : Additive (PontryaginDual (Multiplicative (M →ₗ[F] F)))) (ℓ : M →ₗ[F] F) : ZMod.toCircle (ℓ ((pointwisePontryaginDualEquiv M) χ)) = (Additive.toMul χ) (Multiplicative.ofAdd ℓ)