The internal hom out of a coinduced module #
Let U be a subgroup of finite index of a topological group G, let A be a U-module and N
a G-module. The additive homomorphisms out of the coinduced module Coind_U^G A, carrying the
conjugation action of G of TauCeti.InternalHom, receive a G-equivariant homomorphism from a
coinduced module:
Coind_U^G Hom(A, N) → Hom(Coind_U^G A, N), F ↦ (f ↦ tr (g ↦ F g (f g))),
the trace along G ⧸ U of the pointwise evaluation pairing (TauCeti.DiscreteCoind.toInternalHom).
For an open U and a discrete U-module A it is injective, and it is bijective as soon as
moreover the conjugation action of U on Hom(A, N) is continuous
(TauCeti.DiscreteCoind.toInternalHomEquiv), which is the case for a finite A and a discrete
G-module N. This is the finite-index coincidence of induction and coinduction read on the dual:
for finite index, Hom(Ind_U^G A, N) ≅ Coind_U^G Hom(A, N).
On the single single g a, the coinduced function supported on the right coset U * g with
value a at g, the image of F evaluates to g⁻¹ • F g a (toInternalHom_single). Since the
singles span Coind_U^G A this gives injectivity. The preimage of φ : Coind_U^G A →+ N is
g ↦ (a ↦ g • φ (single g a)) (toInternalHomEquiv_symm_apply), which is U-equivariant, hence
locally constant when the conjugation action of U on Hom(A, N) is continuous; for a finite
discrete A and a discrete N this continuity is the ContinuousSMul instance of
TauCeti.InternalHom.
For the permutation module Coind_U^G 𝔽_p of an open subgroup U of a pro-p group this says
that Hom(Coind_U^G 𝔽_p, 𝔽_p) ≅ Coind_U^G 𝔽_p: the permutation module is self-dual, so its
G-invariant functionals are, through Shapiro's isomorphism in degree zero, the U-invariants of
𝔽_p, a line. That identifies the source of the target of Tate's duality map
H²(G, M) → Hom(H⁰(G, Hom(M, 𝔽_p)), H²(G, 𝔽_p)) at M = Coind_U^G 𝔽_p, which is how the second
cohomology of an open subgroup of a Demushkin group is computed through the duality of the ambient
group (Serre, Structure de certains pro-p-groupes, §9.2).
Main definitions #
TauCeti.DiscreteCoind.toInternalHom: theG-equivariant homomorphismCoind_U^G Hom(A, N) →+[G] Hom(Coind_U^G A, N), trace of the pointwise evaluation pairing, for a subgroupUof finite index.TauCeti.DiscreteCoind.toInternalHomEquiv: the additive equivalenceCoind_U^G Hom(A, N) ≃+ Hom(Coind_U^G A, N)it induces for an openU, a discreteU-moduleAand a continuous conjugation action ofUonHom(A, N).
Main results #
TauCeti.DiscreteCoind.toAddMonoidHom_toInternalHom_applyandTauCeti.DiscreteCoind.toInternalHom_apply_eq_sum: the value oftoInternalHom Fatfis the trace ofg ↦ F g (f g), that is∑_{x : G ⧸ U} x.out • F x.out⁻¹ (f x.out⁻¹).TauCeti.DiscreteCoind.toInternalHom_single:toInternalHom F (single g a) = g⁻¹ • F g a, for an openUand a discreteU-moduleA.TauCeti.DiscreteCoind.toInternalHom_injective:toInternalHomis injective for an openUand a discreteU-moduleA.TauCeti.DiscreteCoind.toInternalHom_surjectiveandTauCeti.DiscreteCoind.toInternalHom_bijective:toInternalHomis bijective for an openUand a discreteU-moduleAwhenever the conjugation action ofUonHom(A, N)is continuous, in particular for a finiteAand a discreteG-moduleN.TauCeti.DiscreteCoind.toInternalHomEquiv_symm_apply: the inverse oftoInternalHomEquivsendsφtog ↦ (a ↦ g • φ (single g a)).TauCeti.DiscreteCoind.toInternalHomEquiv_smulandTauCeti.DiscreteCoind.toInternalHomEquiv_symm_smul: both directions oftoInternalHomEquivareG-equivariant.
References #
- K. S. Brown, Cohomology of Groups, GTM 87, Springer (1982), Chapter III, §5: induced and coinduced modules along a subgroup of finite index.
- J.-P. Serre, Structure de certains pro-p-groupes (d'après Demuškin), Séminaire Bourbaki 8 (1962/63), exposé 252, §9.2.
The internal hom out of a coinduced module. For a subgroup U of finite index, a
coinduced homomorphism F : Coind_U^G Hom(A, N) defines the homomorphism
f ↦ tr (g ↦ F g (f g)) on Coind_U^G A, the trace along G ⧸ U of the pointwise evaluation
pairing. The assignment is G-equivariant for the conjugation action on the internal hom. For an
open U and a discrete U-module A it is injective (toInternalHom_injective), and it is a
bijection when moreover the conjugation action of U on Hom(A, N) is continuous
(toInternalHom_bijective), as it is for a finite A and a discrete N.
Instances For
The value of toInternalHom F at f is the trace of the pointwise evaluation pairing
g ↦ F g (f g).
The value of toInternalHom F at f, as a sum over the cosets:
∑_{x : G ⧸ U} x.out • F x.out⁻¹ (f x.out⁻¹).
toInternalHom on a single: toInternalHom F (single g a) = g⁻¹ • F g a. The pointwise
pairing g' ↦ F g' (single g a g') is supported on the right coset U * g, so only that coset
contributes to the trace. Not a simp lemma, because
TauCeti.DiscreteCoind.toAddMonoidHom_toInternalHom_apply already takes its left-hand side
apart.
toInternalHom is injective for an open subgroup U and a discrete U-module A: a
coinduced homomorphism is recovered from its image by evaluating on singles.
toInternalHom is surjective for an open subgroup U and a discrete U-module A whose
internal hom Hom(A, N) carries a continuous conjugation action of U, as it does for a finite A
and a discrete N: a homomorphism φ : Coind_U^G A →+ N is the image of
g ↦ (a ↦ g • φ (single g a)), which is U-equivariant by single_mul, hence locally constant
by the continuity of the action on Hom(A, N), and which toInternalHom sends back to φ by the
decomposition of a coinduced function into its singles.
The internal hom out of a coinduced module is coinduced: for an open subgroup U of
finite index and a discrete U-module A whose internal hom Hom(A, N) carries a continuous
conjugation action of U, in particular for a finite A and a discrete N, toInternalHom is a
G-equivariant bijection Coind_U^G Hom(A, N) ≅ Hom(Coind_U^G A, N).
The internal hom out of a coinduced module is coinduced, as an additive equivalence
Coind_U^G Hom(A, N) ≃+ Hom(Coind_U^G A, N): toInternalHom bundled with its inverse, under the
hypotheses of toInternalHom_bijective. Its forward map is toInternalHom
(toInternalHomEquiv_apply), its inverse sends φ to g ↦ (a ↦ g • φ (single g a))
(toInternalHomEquiv_symm_apply), and both directions are G-equivariant
(toInternalHomEquiv_smul, toInternalHomEquiv_symm_smul).
Instances For
toInternalHomEquiv is toInternalHom on elements.
The inverse of toInternalHomEquiv sends φ : Coind_U^G A →+ N to the coinduced homomorphism
g ↦ (a ↦ g • φ (single g a)): evaluating φ on the single single g a recovers g⁻¹ • F g a
(toInternalHom_single), so g • φ (single g a) = F g a.
toInternalHomEquiv is G-equivariant.
The inverse of toInternalHomEquiv is G-equivariant.