Primary torsion of discrete coinduction #
Over a compact group, a locally constant function to a discrete group has finite image.
Consequently coinduction preserves p-primary torsion, even when the source group has unbounded
p-power exponent. The result applies to every subgroup, and passes to the cokernel
Coind_U^G M ⧸ M of the unit of coinduction, in particular to the dimension-shifting quotient
Coind_1^G M ⧸ M. This lets the dimension-shifting sequence stay within the coefficient class used
to define p-cohomological dimension.
References #
- J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., Chapter III, §3, (3.3.2).
theorem
TauCeti.isPPrimaryTorsion_discreteCoind
{p : ℕ}
(G : Type u_1)
[Group G]
[TopologicalSpace G]
[CompactSpace G]
(U : Subgroup G)
(M : Type u_2)
[AddCommGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
[DistribMulAction (↥U) M]
(hM : IsPPrimaryTorsion p M)
:
IsPPrimaryTorsion p (DiscreteCoind G U M)
Discrete coinduction from a subgroup preserves p-primary torsion over a compact group.
theorem
TauCeti.ContCohomology.isPPrimaryTorsion_coindQuotient
{p : ℕ}
(G : Type u_1)
[Group G]
[TopologicalSpace G]
[CompactSpace G]
(U : Subgroup G)
(M : Type u_2)
[AddCommGroup M]
[TopologicalSpace M]
[DiscreteTopology M]
[ContinuousMul G]
[DistribMulAction G M]
[ContinuousSMul G M]
(hM : IsPPrimaryTorsion p M)
:
IsPPrimaryTorsion p (CoindQuotient G U M)
The quotient Coind_U^G M ⧸ M remains p-primary torsion whenever M is p-primary
torsion.