The ℤ/n-dual of an additive group killed by n

An additive commutative group M killed by n ≠ 0 is a ℤ/n-module, and its additive homomorphisms to ZMod n are its ℤ/n-linear functionals. Written multiplicatively they are the characters of Multiplicative M with values in Multiplicative (ZMod n), a group with enough roots of unity for the exponent of M, so Mathlib's duality theory for finite abelian groups applies to them. This file records the two consequences that the duality of finite ℤ/n[G]-modules rests on, phrased on M →+ ZMod n so that no module instance has to be installed by the caller: for finite M there are exactly as many homomorphisms M →+ ZMod n as elements of M, and the homomorphisms to ZMod n separate the points of M, finite or not. The count is also recorded for ℤ/n-linear maps, for callers that already carry the module structures. The separation statement is first proved on the finite cyclic subgroup generated by a point, and then extended to M along the inclusion, using that ZMod n is an injective ℤ/n-module. Together they show that a pairing into ZMod n of a finite group killed by n is perfect as soon as one of its adjoints is bijective, the form in which duality theorems for finite Galois modules are stated. The case n = p prime is the linear algebra of the 𝔽_p-vector space M.

Main results

• TauCeti.natCard_addMonoidHom_zmod: Nat.card (M →+ ZMod n) = Nat.card M for finite M killed by n, and AddEquiv.natCard_addMonoidHom_zmod: the same count for the homomorphisms into any additive group N ≃+ ZMod n; AddEquiv.natCard_linearMap_zmod: the same count for the ℤ/n-linear maps of a finite ℤ/n-module.
• TauCeti.exists_addMonoidHom_zmod_apply_ne_zero: for a ≠ 0 in M killed by n, some f : M →+ ZMod n has f a ≠ 0; TauCeti.exists_distribMulActionHom_apply_ne_zero: the same for equivariant maps to any N ≃+ ZMod n when a monoid acts trivially on M and N.
• TauCeti.forall_eq_zero_and_exists_eq_of_bijective_flip: a pairing M × M' → ZMod n, M finite and killed by n, one of whose adjoints M' → (M →+ ZMod n) is bijective, is perfect; TauCeti.forall_eq_zero_and_exists_eq_of_bijective_flip_of_addEquiv reads it through additive equivalences.

theorem TauCeti.natCard_addMonoidHom_zmod {n : ℕ} [NeZero n] {M : Type u_1} [AddCommGroup M] [Finite M] (hM : ∀ (x : M), n • x = 0) : Nat.card (M →+ ZMod n) = Nat.card M

A finite additive commutative group killed by n ≠ 0 has as many additive homomorphisms to ZMod n as elements.

theorem TauCeti.exists_addMonoidHom_zmod_apply_ne_zero {n : ℕ} [NeZero n] {M : Type u_1} [AddCommGroup M] (hM : ∀ (x : M), n • x = 0) {a : M} (ha : a ≠ 0) : ∃ (f : M →+ ZMod n), f a ≠ 0

Additive homomorphisms to ZMod n detect every nonzero element of an additive commutative group killed by n ≠ 0. The group need not be finite.

theorem TauCeti.exists_distribMulActionHom_apply_ne_zero {n : ℕ} [NeZero n] {M : Type u_1} [AddCommGroup M] {G : Type u_2} [Monoid G] {N : Type u_3} [AddCommGroup N] [DistribMulAction G N] (hN : ∀ (g : G) (y : N), g • y = y) (e : N ≃+ ZMod n) [DistribMulAction G M] (hM : ∀ (x : M), n • x = 0) (hMtriv : ∀ (g : G) (x : M), g • x = x) {a : M} (ha : a ≠ 0) : ∃ (f : M →+[G] N), f a ≠ 0

For e : N ≃+ ZMod n with n ≠ 0 and a monoid G acting trivially on N and on an additive commutative group M killed by n, the equivariant maps M → N detect every nonzero element of M: they are all the additive maps, and those to ZMod n separate points.

theorem TauCeti.forall_eq_zero_and_exists_eq_of_bijective_flip {n : ℕ} [NeZero n] {M : Type u_1} [AddCommGroup M] {M' : Type u_2} [AddCommGroup M'] [Finite M] (hM : ∀ (x : M), n • x = 0) (Φ : M →+ M' →+ ZMod n) (hΦ : Function.Bijective ⇑Φ.flip) : (∀ (x : M), (∀ (y : M'), (Φ x) y = 0) → x = 0) ∧ ∀ (φ : M' →+ ZMod n), ∃ (x : M), ∀ (y : M'), (Φ x) y = φ y

A pairing into ZMod n with a bijective adjoint is perfect. Let Φ : M × M' → ZMod n be biadditive, with M finite and killed by n ≠ 0. If every homomorphism M →+ ZMod n is Φ (-, y) for exactly one y, then Φ separates the points of M, and every homomorphism M' →+ ZMod n is Φ (x, -) for some x: the homomorphisms to ZMod n separate the points of M, and M, M →+ ZMod n, M' and M' →+ ZMod n all have the same order.

theorem TauCeti.forall_eq_zero_and_exists_eq_of_bijective_flip_of_addEquiv {n : ℕ} [NeZero n] {X : Type u_2} {Y : Type u_3} {X₀ : Type u_4} {Y₀ : Type u_5} [AddCommGroup X] [AddCommGroup Y] [AddCommGroup X₀] [AddCommGroup Y₀] [Finite X₀] (hX₀ : ∀ (x : X₀), n • x = 0) (pair : X → Y → ZMod n) (eX : X₀ ≃+ X) (eY : Y₀ ≃+ Y) (Φ : X₀ →+ Y₀ →+ ZMod n) (hΦ : Function.Bijective ⇑Φ.flip) (h : ∀ (x : X₀) (y : Y₀), pair (eX x) (eY y) = (Φ x) y) : (∀ (x : X), (∀ (y : Y), pair x y = 0) → x = 0) ∧ ∀ (φ : Y →+ ZMod n), ∃ (x : X), ∀ (y : Y), pair x y = φ y

A pairing into ZMod n that is a perfect pairing up to additive equivalences is perfect. If pair : X → Y → ZMod n reads, through additive equivalences eX : X₀ ≃+ X and eY : Y₀ ≃+ Y, as a biadditive Φ, with X₀ finite and killed by n, whose adjoint Y₀ → (X₀ →+ ZMod n) is bijective, then pair separates the points of X, and every homomorphism Y →+ ZMod n is pair (x, -) for some x (TauCeti.forall_eq_zero_and_exists_eq_of_bijective_flip).

theorem AddEquiv.natCard_addMonoidHom_zmod {n : ℕ} [NeZero n] {M : Type u_1} [AddCommGroup M] {N : Type u_2} [AddCommGroup N] (e : N ≃+ ZMod n) [Finite M] (hM : ∀ (x : M), n • x = 0) : Nat.card (M →+ N) = Nat.card M

For e : N ≃+ ZMod n with n ≠ 0, a finite additive commutative group killed by n has as many additive homomorphisms to N as elements.

theorem AddEquiv.natCard_linearMap_zmod {n : ℕ} [NeZero n] {M : Type u_1} [AddCommGroup M] {N : Type u_2} [AddCommGroup N] [Module (ZMod n) N] (e : N ≃+ ZMod n) [Module (ZMod n) M] [Finite M] : Nat.card (M →ₗ[ZMod n] N) = Nat.card M

For e : N ≃+ ZMod n with n ≠ 0, a finite ℤ/n-module has as many ℤ/n-linear maps to N as elements.