The profinite integers as a profinite group #
The profinite integers ℤ̂, written zHat, form the profinite completion of the additive
group of ℤ, written multiplicatively. The defining copy of ℤ is universe-lifted so that
zHat.{u} can live in any universe; this does not change the completed group. This file records
the group-theoretic facts about ℤ̂ that the pro-p theory uses, together with the calculus of
zHat.lift (naturality, joint continuity, and its behaviour in the first argument) on which the
ring structure rests; that ring structure lives on Additive zHat in
TauCeti.Topology.Algebra.Group.Profinite.ZHat.Ring.
The generator 1 ∈ ℤ gives the topological generator zHat.gen, and the universal property of
the profinite completion becomes: continuous homomorphisms from ℤ̂ to a profinite group P
are exactly the elements of P, through the value at zHat.gen. Since the image of ℤ is
dense, ℤ̂ is commutative. The identification of the maximal pro-p quotient of ℤ̂ with the
p-adic integers, and of its p-Sylow subgroups with ℤ_p, is in
TauCeti.Topology.Algebra.Group.Profinite.ZHat.PadicInt.
Main definitions #
TauCeti.zHat: the profinite integers, as a profinite group.TauCeti.zHat.ofInt,TauCeti.zHat.gen: the canonical homomorphism fromℤand the image of1.TauCeti.zHat.lift: the continuous homomorphism to a profinite group sendingzHat.gento a given element.TauCeti.zHat.liftEquiv:liftas an equivalence between a profinite group and the continuous homomorphisms fromℤ̂to it, with inverse evaluation atzHat.gen.
Main results #
TauCeti.zHat.hom_ext,TauCeti.zHat.existsUnique_lift: the universal property ofℤ̂.TauCeti.zHat.denseRange_ofInt, and theIsMulCommutative zHatinstance: the image ofℤis dense, soℤ̂is commutative.TauCeti.zHat.comp_lift,TauCeti.zHat.continuous_lift: the lift is natural in the target and jointly continuous in the element and the exponent.TauCeti.zHat.lift_mul_apply,TauCeti.zHat.lift_zpow_apply,TauCeti.zHat.lift_comm: the lift is multiplicative on commuting base elements and compatible with powers, and onℤ̂itself it is symmetric.
References #
- L. Ribes and P. Zalesskii, Profinite Groups, Sections 2.3 and 4.3.
The profinite integers ℤ̂: the profinite completion of a universe lift of the additive
group of ℤ, written multiplicatively. The lift only places the completion in universe u.
This is the profinite group; its ring structure is put on Additive zHat in
TauCeti.Topology.Algebra.Group.Profinite.ZHat.Ring.
Equations
Instances For
The canonical homomorphism from ℤ, written multiplicatively, to the profinite integers. It
sends z through ULift.up into the defining copy ULift.{u} (Multiplicative ℤ), and then
through Mathlib's unit ProfiniteGrp.ProfiniteCompletion.eta at that copy, read as a plain
monoid homomorphism.
Equations
Instances For
The underlying function of ofInt is ULift.up followed by the unit map of the profinite
completion of ULift.{u} (Multiplicative ℤ).
The image of 1 ∈ ℤ in the profinite integers: the element whose value determines a
continuous homomorphism out of ℤ̂, by zHat.hom_ext.
Equations
Instances For
The canonical homomorphism from ℤ sends n to the n-th power of the generator.
The image of ℤ is dense in the profinite integers.
The profinite integers are commutative, since the image of ℤ is dense.
Two continuous homomorphisms out of the profinite integers into a Hausdorff topological monoid that agree on the generator are equal.
The continuous homomorphism from the profinite integers to a profinite group P, in any
universe, sending the generator to a.
Equations
Instances For
The lift of a sends the image of n ∈ ℤ to a ^ n.
The lift of a sends the generator to a.
A continuous homomorphism sending the generator to a is the lift of a.
The universal property of the profinite integers. For every element a of a profinite
group there is a unique continuous homomorphism from ℤ̂ sending the generator to a.
The universal property of the profinite integers, bundled. Continuous homomorphisms from
ℤ̂ to a profinite group P correspond to elements of P, via TauCeti.zHat.lift and
evaluation at the generator.
Equations
- TauCeti.zHat.liftEquiv P = { toFun := TauCeti.zHat.lift, invFun := fun (φ : ↑TauCeti.zHat.toProfinite.toTop →ₜ* P) => φ TauCeti.zHat.gen, left_inv := ⋯, right_inv := ⋯ }
Instances For
The bundled universal property sends a to its lift.
The inverse of the bundled universal property is evaluation at the generator.
The lift of the generator is the identity of the profinite integers.
The lift of the generator fixes every element.
The lift of 1 is the trivial homomorphism.
The lift of 1 is constant equal to 1.
Naturality of the lift. A continuous homomorphism f between profinite groups carries
the lift of a to the lift of f a.
A continuous homomorphism between profinite groups commutes with the lift: it carries
lift a x to lift (f a) x.
Joint continuity of the lift: (a, x) ↦ lift a x is continuous on P × ℤ̂.
The lift is multiplicative on commuting base elements.
The lift of a power is the power of the lift.
The lift of a topological generator of a profinite group is surjective.
The lift of a is injective when every finite quotient of the defining copy of ℤ is
detected by a continuous quotient of the target carrying a to the canonical generator. This is
the finite-coordinate criterion used to identify a procyclic group having quotients of every
finite order with the profinite integers.