Lyndon's theorem for the relation module of a profinite presentation #
Let G be a finite group, g : ι → G a generating family indexed by a finite type, F the free
profinite group on ι, and R the kernel of the continuous homomorphism π = lift g : F → G
sending the generators to the g i. This file identifies the abelian pro-p group
R^ab(p) = abelianizationProP p F R, with the conjugation action of F ⧸ R, with the relation
module relationModule ℤ_[p] G g of the family g, the kernel of ℤ_p[G]^ι → ℤ_p[G],
e_i ↦ g i - 1. Through this identification a ℤ_p[G]-module map out of the relation module acts
on the kernel R^ab(p) of the group extension F ⧸ K → G, for K the kernel of R → R^ab(p);
this is how the relation module enters the computation of the number of generators of the
absolute Galois group of a p-adic field (NSW (7.4.1)).
The comparison map is the Fox derivative read in ℤ_p[G]: the unique continuous map
D : F → ℤ_p[G]^ι with D (f * f') = D f + π f • D f' and D (of i) = e_i
(TauCeti.freeProfiniteGroup.foxDerivative). It exists because a continuous homomorphism from
F to the semidirect product of G by ℤ_p^{G × ι} may take any values on the generators. Its
values satisfy the fundamental formula of Fox calculus ∑ i, D f i * (g i - 1) = π f - 1, so on
R it is an equivariant homomorphism into the relation module, and it factors through R^ab(p).
The inverse is written down on the Schreier generators: for a set-theoretic section s of π
the elements r h i = s h * of i * s (h * g i)⁻¹ lie in R, and m ↦ ∑ (m i)(h) • [r h i] is
inverse to the Fox derivative on the relation module. That it is a left inverse is the uniqueness
of crossed homomorphisms on F with given values on the generators, applied to the crossed
homomorphism f ↦ (x ↦ [s x⁻¹ * f * s (x⁻¹ * π f)⁻¹]) with values in the coinduced module
G → R^ab(p); that it is a right inverse is a computation with the relation
∑ m i * (g i - 1) = 0.
Main definitions #
TauCeti.freeProfiniteGroup.foxDerivative: the Fox derivativeF → ℤ_p[G]^ιalonglift g.TauCeti.freeProfiniteGroup.abelianizationProPEquivRelationModule: Lyndon's isomorphismR^ab(p) ≃+ relationModule ℤ_[p] G g.TauCeti.freeProfiniteGroup.abelianizationProPLinearEquivRelationModule: Lyndon's isomorphism as aℤ_p-linear equivalence, with scalar multiplication onR^ab(p)given by p-adic powers.
Main results #
TauCeti.freeProfiniteGroup.foxDerivative_unique: the Fox derivative is the unique continuous crossed homomorphism with valuese_ion the generators.TauCeti.freeProfiniteGroup.sum_foxDerivative_mul_sub_one: the fundamental formula of Fox calculus,∑ i, D f i * (g i - 1) = π f - 1.TauCeti.freeProfiniteGroup.foxDerivative_mem_relationModule: the Fox derivative mapsRinto the relation module.TauCeti.freeProfiniteGroup.coe_abelianizationProPEquivRelationModule_ofMul: Lyndon's isomorphism sends the class ofr ∈ Rto the Fox derivative ofr.TauCeti.freeProfiniteGroup.abelianizationProPEquivRelationModule_padicPow: Lyndon's isomorphism is compatible withp-adic powers onR^ab(p)andℤ_p-scalars on the relation module.TauCeti.freeProfiniteGroup.abelianizationProPEquivRelationModule_smul: Lyndon's isomorphism is equivariant for conjugation byF ⧸ RonR^ab(p)and multiplication byπ fon the relation module.
References #
- J. Neukirch, A. Schmidt and K. Wingberg, Cohomology of Number Fields, 2nd ed., Propositions (5.6.5) and (5.6.6).
- R. C. Lyndon, Cohomology theory of groups with a single defining relation, Ann. of Math. 52 (1950).
- R. H. Fox, Free differential calculus. I, Ann. of Math. 57 (1953).
The Fox derivative along lift g, read in ℤ_p[G]: the unique continuous map
D : F → ℤ_p[G]^ι with D (f * f') = D f + lift g f • D f' and D (of i) = e_i
(foxDerivative_unique). Its i-th coordinate is the image in ℤ_p[G] of the Fox derivative
∂f/∂x_i of f.
Instances For
The coefficients of the Fox derivative depend continuously on the element of F.
The Leibniz rule of the Fox derivative: D (f * f') = D f + lift g f • D f'.
The Fox derivative of the generator of i is the standard basis vector e_i.
The Fox derivative of 1 is 0.
The Fox derivative of an inverse: D f⁻¹ = -(lift g f)⁻¹ • D f.
The Fox derivative of a quotient: D (f * f'⁻¹) = D f - lift g (f * f'⁻¹) • D f'.
On the kernel of lift g the Fox derivative is additive.
On the kernel of lift g the Fox derivative is equivariant for conjugation:
D (f * r * f⁻¹) = lift g f • D r.
The Fox derivative is unique: a continuous map D : F → ℤ_p[G]^ι with
D (f * f') = D f + lift g f • D f' and D (of i) = e_i is foxDerivative p g.
The fundamental formula of Fox calculus, read in ℤ_p[G]:
∑ i, D f i * (g i - 1) = lift g f - 1.
The Fox derivative maps the kernel of lift g into the relation module of g.
The Fox derivative on R^ab(p) #
The Schreier inverse #
Lyndon's isomorphism #
Lyndon's theorem for the relation module (NSW (5.6.6)). For a finite group G generated by
the family g : ι → G, the maximal abelian pro-p quotient R^ab(p) of the kernel R of
lift g : F → G is isomorphic to the relation module relationModule ℤ_[p] G g. The isomorphism
sends the class of r ∈ R to its Fox derivative
(coe_abelianizationProPEquivRelationModule_ofMul), it is ℤ_p-linear
(abelianizationProPEquivRelationModule_padicPow), and it is equivariant
(abelianizationProPEquivRelationModule_smul).
Instances For
Lyndon's isomorphism sends the class of r ∈ R to the Fox derivative of r.
Lyndon's isomorphism is ℤ_p-linear: it sends the p-adic power a ^ c in R^ab(p) to
c times the image of a.
Lyndon's isomorphism as a ℤ_p-linear equivalence, for the module structure on R^ab(p)
given by p-adic exponentiation. Its underlying map is abelianizationProPEquivRelationModule.
Instances For
The linear form of Lyndon's isomorphism evaluates as its additive form.
Lyndon's isomorphism is equivariant: conjugation by f ∈ F on R^ab(p), through
F ⧸ R, corresponds to multiplication by lift g f on the relation module.