The continuous `ZMod n`-dual of a topological group #

The continuous characters of a topological group with values in the multiplicative encoding Multiplicative (ZMod n) of ZMod n form a commutative group, written additively as the continuous ZMod n-dual TauCeti.continuousZModDual n G. Scalar n kills the target, hence the character group as well, so the dual is a ZMod n-module; for a prime p it is an 𝔽_p-vector space, the discrete companion of a compact 𝔽_p-vector group.

When the group is itself commutative with a ZMod p-module structure on its additive copy — for a prime p, an elementary abelian group — a continuous character of it is in particular a linear functional on that module, so TauCeti.continuousZModDualToDual reads the continuous dual inside the algebraic dual, injectively.

Main definitions #

TauCeti.continuousZModDual: the group of continuous ZMod n-valued characters of a topological group, written additively; for a prime p it is the continuous 𝔽_p-dual.
TauCeti.continuousZModDual.evalₗ: evaluation at a point, as a linear functional on the dual.
ContinuousMonoidHom.continuousZModDualMap: precomposition with a continuous homomorphism, the transpose map between continuous duals. The transpose of a topological group isomorphism is bijective (ContinuousMulEquiv.continuousZModDualMap_bijective).
TauCeti.continuousZModDualToDual: a continuous ZMod p-valued character of a commutative group whose additive copy is a ZMod p-module, read as a linear functional on that module.

source

@[reducible, inline]

abbrev TauCeti.continuousZModDual (n : ℕ) (G : Type u) [Group G] [TopologicalSpace G] :

Type u

The continuous ZMod n-dual of a topological group: its group of continuous characters with values in ZMod n, written additively so that it is a ZMod n-module. For a prime p it is the continuous 𝔽_p-dual, an 𝔽_p-vector space.

Equations

TauCeti.continuousZModDual n G = Additive (G →ₜ* Multiplicative (ZMod n))

Instances For

source

@[instance_reducible]

instance TauCeti.instModuleContinuousZModDual {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] :

Module (ZMod n) (continuousZModDual n G)

The continuous ZMod n-valued characters form a ZMod n-module: the target has exponent dividing n, hence so does the character group.

Equations

TauCeti.instModuleContinuousZModDual = AddCommGroup.zmodModule ⋯

source

def TauCeti.continuousZModDual.evalₗ {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (g : G) :

continuousZModDual n G →ₗ[ZMod n] ZMod n

Evaluation at a point g : G, as a ZMod n-linear functional on the continuous ZMod n-dual of G: a character χ goes to its value at g, read additively.

Equations

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

Instances For

source

@[simp]

theorem TauCeti.continuousZModDual.evalₗ_apply {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] (g : G) (χ : continuousZModDual n G) :

(evalₗ g) χ = Multiplicative.toAdd ((Additive.toMul χ) g)

Evaluation at g sends a character to its value at g.

source

def ContinuousMonoidHom.continuousZModDualMap {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] (f : G →ₜ* H) :

TauCeti.continuousZModDual n H →ₗ[ZMod n] TauCeti.continuousZModDual n G

Precomposition with a continuous homomorphism f : G →ₜ* H, as a ZMod n-linear map from the continuous ZMod n-dual of H to that of G: the transpose of f.

Equations

f.continuousZModDualMap = AddMonoidHom.toZModLinearMap n { toFun := fun (χ : TauCeti.continuousZModDual n H) => Additive.ofMul ((Additive.toMul χ).comp f), map_zero' := ⋯, map_add' := ⋯ }

Instances For

source

theorem ContinuousMonoidHom.toMul_continuousZModDualMap {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] (f : G →ₜ* H) (χ : TauCeti.continuousZModDual n H) :

Additive.toMul (f.continuousZModDualMap χ) = (Additive.toMul χ).comp f

The transpose of f precomposes a character of H with f.

source

@[simp]

theorem ContinuousMonoidHom.toMul_continuousZModDualMap_apply {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] (f : G →ₜ* H) (χ : TauCeti.continuousZModDual n H) (g : G) :

(Additive.toMul (f.continuousZModDualMap χ)) g = (Additive.toMul χ) (f g)

The transpose of f evaluates a character of H along f.

source

@[simp]

theorem ContinuousMonoidHom.continuousZModDualMap_id {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] :

(id G).continuousZModDualMap = LinearMap.id

The transpose of the identity is the identity.

source

@[simp]

theorem ContinuousMonoidHom.continuousZModDualMap_comp {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] {K : Type u_2} [Group K] [TopologicalSpace K] (g : H →ₜ* K) (f : G →ₜ* H) :

(g.comp f).continuousZModDualMap = f.continuousZModDualMap ∘ₗ g.continuousZModDualMap

The transpose of a composite is the composite of the transposes, in the reverse order.

source

theorem ContinuousMulEquiv.continuousZModDualMap_bijective {n : ℕ} {G : Type u} [Group G] [TopologicalSpace G] {H : Type u_1} [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) :

Function.Bijective ⇑(↑e).continuousZModDualMap

The transpose of a topological group isomorphism is bijective: its inverse is the transpose of the inverse isomorphism.

source

def TauCeti.continuousZModDualToDual {p : ℕ} {W : Type u} [CommGroup W] [TopologicalSpace W] [Module (ZMod p) (Additive W)] :

continuousZModDual p W →ₗ[ZMod p] Module.Dual (ZMod p) (Additive W)

A continuous ZMod p-valued character of a commutative group W whose additive copy is a ZMod p-module, read as a linear functional on that module; for a prime p and an elementary abelian W this is a functional on the 𝔽_p-vector space Additive W. It is injective (TauCeti.continuousZModDualToDual_injective), so the continuous dual is a subspace of the algebraic dual.

Equations