Continuous maps from a profinite relation module #
Lyndon's isomorphism identifies the abelian pro-p quotient of the relation subgroup of a
finite profinite presentation with its algebraic ℤ_p[G]-relation module. Every ℤ_p-linear
map out of that relation module into a topological ℤ_p-module gives a continuous additive
map on the abelian pro-p quotient. This permits algebraic relation-module maps to act on the
kernels of profinite group extensions, without installing a second topology on the relation
module.
References #
- J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., (5.6.6) and the proof of (7.4.1).
theorem
TauCeti.freeProfiniteGroup.continuous_comp_abelianizationProPEquivRelationModule
(p : ℕ)
[Fact (Nat.Prime p)]
{G : Type u}
[Group G]
[Finite G]
[TopologicalSpace G]
[DiscreteTopology G]
{ι : Type u}
[Fintype ι]
[DecidableEq ι]
{g : ι → G}
(hg : Subgroup.closure (Set.range g) = ⊤)
{M : Type u_1}
[AddCommMonoid M]
[Module ℤ_[p] M]
[TopologicalSpace M]
[ContinuousAdd M]
[ContinuousSMul ℤ_[p] M]
(β : ↥(MonoidAlgebra.relationModule ℤ_[p] G g) →ₗ[ℤ_[p]] M)
:
Continuous (⇑β ∘ ⇑(abelianizationProPEquivRelationModule p hg))
A linear map out of the algebraic relation module, read on the abelian pro-p quotient
of the relation subgroup through Lyndon's isomorphism, is continuous. The codomain need not
be finitely generated or Hausdorff.