Double duality for internal homs of discrete modules

Let a group G act on additive monoids M and N, and let InternalHom G M N be the internal hom M →+ N with its conjugation action. Evaluation

eval : m ↦ (φ ↦ φ m)

is a G-equivariant additive homomorphism from M to the double internal dual InternalHom G (InternalHom G M N) N, and it is natural in M: precomposing twice with an equivariant f : M →+[G] M' carries eval m to eval (f m). When N = ZMod n for n ≠ 0 and M is killed by n, evaluation is injective, because the homomorphisms to ZMod n separate the points of M; when M is moreover finite it is bijective, by counting: the internal hom InternalHom G M (ZMod n) has the order of M. So a finite discrete G-module killed by n is canonically and equivariantly its own double dual, which is what identifies the dual of the dual of a short exact sequence of such modules with the sequence itself, and what turns the duality statements about a module M into statements about its dual InternalHom G M (ZMod n). The coefficient systems ℤ/pⁱ of a pro-p group are the case n = pⁱ.

Main definitions

• TauCeti.InternalHom.eval: the evaluation map M →+[G] InternalHom G (InternalHom G M N) N, with TauCeti.InternalHom.evalPairing_eval as its defining equation and TauCeti.InternalHom.precomp_precomp_eval as its naturality.

Main results

• TauCeti.InternalHom.natCard_of_addEquiv_zmod: Nat.card (InternalHom G M N) = Nat.card M for finite M killed by n ≠ 0 and values in any additive group N ≃+ ZMod n.
• TauCeti.InternalHom.eval_injective_of_addEquiv_zmod and TauCeti.InternalHom.eval_bijective_of_addEquiv_zmod: evaluation into the double dual with values in any additive group N ≃+ ZMod n, whatever the action of G on N, is injective on a module killed by n ≠ 0, and bijective when that module is finite. The untwisted coefficients ZMod n are the case e = AddEquiv.refl _, and the twisted coefficients ℤ/pⁱ of a character are the case in use.

def TauCeti.InternalHom.eval (G : Type u_1) [Group G] (M : Type u_2) [AddMonoid M] [DistribMulAction G M] (N : Type u_3) [AddCommMonoid N] [DistribMulAction G N] : M →+[G] InternalHom G (InternalHom G M N) N

Evaluation into the double dual. The equivariant additive homomorphism M →+[G] InternalHom G (InternalHom G M N) N sending m to φ ↦ φ m. Its values are characterized by evalPairing_eval, and it is natural in M by precomp_precomp_eval.

Equations

• TauCeti.InternalHom.eval G M N = { toFun := fun (m : M) => { toAddMonoidHom := (TauCeti.InternalHom.evalPairing G).flip m }, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.InternalHom.toAddMonoidHom_eval {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddCommMonoid N] [DistribMulAction G N] (m : M) : ((eval G M N) m).toAddMonoidHom = (evalPairing G).flip m

Forgetting the action, eval m is the flipped evaluation pairing at m, the additive homomorphism φ ↦ φ m on InternalHom G M N.

theorem TauCeti.InternalHom.evalPairing_eval {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddCommMonoid N] [DistribMulAction G N] (m : M) (φ : InternalHom G M N) : ((evalPairing G) ((eval G M N) m)) φ = ((evalPairing G) φ) m

Evaluation into the double dual evaluates: (eval m) φ = φ m. Not a simp lemma, since evalPairing_apply already rewrites its left-hand side to toAddMonoidHom_eval.

theorem TauCeti.InternalHom.precomp_precomp_eval {G : Type u_1} [Group G] {M : Type u_2} [AddMonoid M] [DistribMulAction G M] {N : Type u_3} [AddCommMonoid N] [DistribMulAction G N] {M' : Type u_4} [AddMonoid M'] [DistribMulAction G M'] (f : M →+[G] M') (m : M) : (precomp G (precomp G f)) ((eval G M N) m) = (eval G M' N) (f m)

Evaluation into the double dual is natural in the module: for an equivariant f : M →+[G] M', precomposing twice with f carries eval m to eval (f m).

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

The internal dual of a finite module killed by n has the same order, for values in any additive group N ≃+ ZMod n.

theorem TauCeti.InternalHom.eval_injective_of_addEquiv_zmod {G : Type u_1} {M : Type u_2} [AddCommGroup M] {n : ℕ} [NeZero n] {N : Type u_3} [AddCommGroup N] (e : N ≃+ ZMod n) [Group G] [DistribMulAction G M] [DistribMulAction G N] (hM : ∀ (x : M), n • x = 0) : Function.Injective ⇑(eval G M N)

For a module M killed by n ≠ 0, evaluation into the double dual with values in any additive group N ≃+ ZMod n is injective: the homomorphisms M →+ N separate the points of M.

theorem TauCeti.InternalHom.eval_bijective_of_addEquiv_zmod {G : Type u_1} {M : Type u_2} [AddCommGroup M] {n : ℕ} [NeZero n] {N : Type u_3} [AddCommGroup N] (e : N ≃+ ZMod n) [Group G] [DistribMulAction G M] [DistribMulAction G N] [Finite M] (hM : ∀ (x : M), n • x = 0) : Function.Bijective ⇑(eval G M N)

Double duality. For a finite module M killed by n ≠ 0, evaluation into the double dual with values in any additive group N ≃+ ZMod n is bijective: M is equivariantly its own double dual.