Exponentiation of a pro-p group by the p-adic integers #
In a pro-p group every finite quotient is killed by a power of p, so the integer powers of
an element a only depend on the exponent modulo a power of p in each finite quotient. The
p-adic integers are the inverse limit of those exponent rings, and hA.padicPow a l is the
resulting power a ^ l for l : ℤ_[p]: it is the unique element whose class modulo an open
normal subgroup U is a ^ l.appr n, for any n with p ^ n killing the quotient by U.
The construction is the limit description of a profinite group applied to the compatible family
of truncated powers, so it needs no completeness or uniform-space input. It extends the integer
powers, is jointly continuous, and turns ℤ_[p] into a ring of exponents: it is additive and
multiplicative in the exponent, and it is the unique continuous extension of k ↦ a ^ k along
ℕ ⊆ ℤ_[p].
For an abelian pro-p group this action makes the group a ℤ_[p]-module,
TauCeti.IsProP.module, which is the form in which the structure theory of finitely generated
abelian pro-p groups is stated.
Main definitions #
TauCeti.IsProP.padicPow: the powera ^ lof an element of a pro-pgroup by ap-adic integer.TauCeti.IsProP.module: theℤ_[p]-module structure on an abelian pro-pgroup.TauCeti.IsProP.padicPowHomeomorph: for a unituofℤ_[p], the powera ↦ a ^ uas a homeomorphism of the group, with inversea ↦ a ^ u⁻¹.
Main results #
TauCeti.IsProP.mk_padicPow: the defining description of the power in each finite quotient.TauCeti.IsProP.padicPow_natCast,TauCeti.IsProP.padicPow_ofNat,TauCeti.IsProP.padicPow_intCast: the power extends the natural and integer powers.TauCeti.IsProP.padicPow_add,TauCeti.IsProP.padicPow_mul: the exponent laws; andTauCeti.IsProP.inv_padicPow,TauCeti.IsProP.mul_padicPowin the base, the latter for commuting elements.TauCeti.IsProP.continuous_padicPow: the actionℤ_[p] × A → Ais jointly continuous.TauCeti.IsProP.eq_padicPow_of_continuous,TauCeti.IsProP.map_padicPow: the power is the unique continuous extension of the natural powers, and continuous homomorphisms preserve it.TauCeti.IsProP.padicPow_mem: a closed subgroup containingacontains itsp-adic powers;TauCeti.IsProP.map_padicPow_eq_one_of_eq_one: a continuous homomorphism into aT1monoid trivial onais trivial on itsp-adic powers.TauCeti.IsProP.eq_zero_of_padicPow_mem: a closed subgroup containing nop-powera ^ (p ^ k)contains thep-adic powera ^ lonly forl = 0.TauCeti.IsProP.conj_padicPow: the power commutes with conjugation;TauCeti.IsProP.commute_padicPow: powers of commuting elements commute.TauCeti.IsProP.padicPow_padicPow_inv,TauCeti.IsProP.padicPow_left_inj,TauCeti.IsProP.closedZpowers_padicPow: a unit exponentuis undone byu⁻¹, its power map is injective, anda ^ ugenerates the same closed subgroup asa.TauCeti.IsProP.mk_padicPow_quotient,TauCeti.IsProP.ofMul_mk_padicPow_quotient: modulo a closed normal subgroup the power is the power of the class, and it is the scalar action ofℤ_[p]when the quotient is abelian.TauCeti.IsProP.padicPow_ofAdd_apply_one: along a continuous additive homomorphismg : ℤ_[p] →+ X, thep-adic power ofofAdd (g 1)inMultiplicative XisofAdd ∘ g.TauCeti.IsProP.module_smul,TauCeti.IsProP.continuousSMul_module: the module structure acts by thep-adic power, and is topological.TauCeti.IsProP.smul_padicPow,TauCeti.IsProP.smulCommClass_module: continuous actions by group endomorphisms commute withp-adic powers and the resulting scalar action.
References #
- L. Ribes and P. Zalesskii, Profinite Groups, Section 4.3.
The p-adic power of an element of a pro-p group. For l : ℤ_[p] the element
hA.padicPow a l is the unique element of A whose class in each finite quotient is the
corresponding truncated power of the class of a; see TauCeti.IsProP.mk_padicPow.
Equations
- hA.padicPow a l = Exists.choose ⋯
Instances For
The defining description of the p-adic power. In the quotient by an open normal
subgroup where the image of a is killed by p ^ n, the p-adic power of a by l is the
ordinary power of a by the truncation l.appr n.
The p-adic power extends the natural-number powers.
The p-adic power by a numeral is the corresponding natural power.
The p-adic power by 0 is trivial.
The p-adic power by 1 is the element itself.
The p-adic power is additive in the exponent.
Iterating the p-adic power multiplies the exponents.
Every p-adic power of 1 is 1.
The p-adic power of an inverse is the inverse of the p-adic power.
Negating the exponent inverts the p-adic power.
The p-adic power extends the integer powers.
The p-adic power is jointly continuous as an action ℤ_[p] × A → A.
The p-adic power is the unique continuous extension of the natural powers along the
dense inclusion of ℕ in ℤ_[p].
A closed subgroup containing a contains every p-adic power of a.
A continuous homomorphism into a T1 monoid that is trivial on a is trivial on every p-adic
power of a.
A p-adic power lying in a closed subgroup has exponent 0 unless a p-power of the base
does. If the closed subgroup H contains a ^ l but no a ^ (p ^ k), then l = 0: a nonzero
l is u pᵛ with u a unit, and then a ^ (pᵛ) = (a ^ l) ^ (u⁻¹) lies in H.
Continuous homomorphisms between pro-p groups preserve the p-adic power.
A continuous action by group endomorphisms commutes with p-adic powers.
The p-adic power is multiplicative on commuting base elements.
The p-adic power commutes with conjugation: (g * a * g⁻¹) ^ l = g * a ^ l * g⁻¹.
A p-adic power of an element commuting with b commutes with b.
An element commuting with b commutes with every p-adic power of b.
p-adic powers of commuting elements commute.
A p-adic power of a lies in the closed cyclic subgroup generated by a.
The closed cyclic subgroup generated by a p-adic power of a lies in the one generated by
a.
Unit exponents #
Raising to a unit u of ℤ_[p] and then to its inverse is the identity.
Raising to the inverse of a unit u of ℤ_[p] and then to u is the identity.
The p-adic power by a unit is a homeomorphism. For a unit u of ℤ_[p] the map
a ↦ a ^ u is a homeomorphism of A, with inverse a ↦ a ^ u⁻¹.
Equations
Instances For
The homeomorphism TauCeti.IsProP.padicPowHomeomorph u is the p-adic power by u.
The inverse of the p-adic power by u is the p-adic power by u⁻¹.
The p-adic power by a unit is injective. This can fail for non-units: when A has
an element of order p, the power by p identifies it with 1.
Two elements with the same p-adic power by a unit are equal.
A unit p-adic power of a generates the same closed cyclic subgroup as a.
Quotients #
The p-adic power passes to quotients: the class of a ^ l modulo a closed normal
subgroup N is the p-adic power of the class of a in the pro-p group A ⧸ N.
A p-adic power relation between the values of a continuous homomorphism holds in the
quotient by its kernel: if χ : A →ₜ* B is a continuous homomorphism of pro-p groups with
χ b = (χ a) ^ l, then b = a ^ l in A ⧸ ker χ.
An abelian pro-p group is a ℤ_[p]-module, with l acting as the p-adic power
by l. The prime is not determined by A, so this is a definition rather than an instance;
consumers introduce it with letI := hA.module.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The scalar action underlying TauCeti.IsProP.module is the p-adic power.
The ℤ_[p]-module structure on an abelian pro-p group is topological.
A continuous action by group endomorphisms is ℤ_p-linear: it commutes with the scalar
action of TauCeti.IsProP.module.
In an abelian quotient the p-adic power is the scalar action. If N is a closed normal
subgroup of the pro-p group A with commutative quotient, then the class of a ^ l in
A ⧸ N, written additively, is l times the class of a for the ℤ_[p]-module structure
TauCeti.IsProP.module of the quotient.
Along a continuous additive homomorphism g : ℤ_[p] →+ X into an additive group whose
multiplicative type tag is pro-p, the p-adic power of ofAdd (g 1) is ofAdd ∘ g: the
exponent acts through g. This computes the p-adic powers in a product of pro-p groups
coordinatewise.