The additive group of the p-adic integers

The additive group of ℤ_[p], written multiplicatively as Multiplicative ℤ_[p], is a pro-p group. Its levels are the open normal subgroups p ^ m ℤ_p (TauCeti.padicIntLevel p m), the kernels of the truncations ℤ_[p] → ZMod (p ^ m); they have index p ^ m and every open subgroup contains one of them, so every open normal quotient is a quotient of a finite p-group.

The element 1 : ℤ_[p] topologically generates this group because the integers are dense in the p-adic integers. Consequently its topological generator rank is one.

The group is moreover the pro-p group on one generator: for every pro-p group P and a : P, the p-adic power l ↦ a ^ l is the unique continuous homomorphism Multiplicative ℤ_[p] →ₜ* P sending 1 to a. This universal property is what identifies Multiplicative ℤ_[p] with the free pro-p group on one generator.

The powers ℤ_[p] ^ X, for an arbitrary index type X, are treated at the end: they are pro-p, topologically generated by the coordinate vectors, so that a continuous homomorphism out of Multiplicative (X → ℤ_[p]) is determined by its values on them, and the p-adic power by l is scalar multiplication by l, that is coordinatewise multiplication by l.

Main results

• TauCeti.padicIntLevel: the level p ^ m ℤ_p of Multiplicative ℤ_[p], as an open normal subgroup, with TauCeti.mem_padicIntLevel_iff, TauCeti.index_padicIntLevel and TauCeti.exists_padicIntLevel_le: it consists of the multiples of p ^ m, has index p ^ m, and every open subgroup contains some level.
• TauCeti.isProP_multiplicative_padicInt: Multiplicative ℤ_[p] is pro-p.
• TauCeti.profiniteOrder_multiplicative_padicInt: its supernatural order is p ^ ∞.
• TauCeti.topologicallyGenerates_ofAdd_one_padicInt: the element 1 topologically generates Multiplicative ℤ_[p].
• TauCeti.topologicalGeneratorRank_multiplicative_padicInt: its topological generator rank is one.
• TauCeti.IsProP.padicPowHom: the continuous homomorphism Multiplicative ℤ_[p] →ₜ* P into a pro-p group P sending 1 to a given element, namely the p-adic power.
• TauCeti.IsProP.existsUnique_continuousMonoidHom_multiplicative_padicInt: the universal property, that this homomorphism is the unique one with that value at 1.
• TauCeti.IsProP.topologicalClosure_closure_singleton_eq_range_padicPowHom, TauCeti.IsProP.mem_topologicalClosure_closure_singleton_iff: the closed subgroup topologically generated by an element is the range of its p-adic power map.
• TauCeti.IsProP.exists_padicPow_mul_padicPow_eq_of_commute: a pro-p group topologically generated by two commuting elements consists of the products of their p-adic powers.
• TauCeti.toAdd_apply_multiplicative_padicInt: a continuous endomorphism of the additive group of ℤ_[p] is multiplication by its value at 1.
• TauCeti.isProP_multiplicative_pi_padicInt, TauCeti.topologicallyGenerates_ofAdd_single_padicInt, TauCeti.isTopologicallyFinitelyGenerated_multiplicative_pi_padicInt, TauCeti.continuousMonoidHom_ext_multiplicative_pi_padicInt: ℤ_[p] ^ X is pro-p, is topologically generated by the coordinate vectors (so is topologically finitely generated for finite X), and continuous homomorphisms out of it are determined by their values on them.
• TauCeti.IsProP.padicPow_ofAdd_pi, TauCeti.IsProP.map_padicPow_pi: in ℤ_[p] ^ X the p-adic power by l is scalar multiplication by l, also after a continuous homomorphism.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Sections 2.2 and 4.3.

theorem TauCeti.continuous_toMultiplicative_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (m : ℕ) : Continuous ⇑(AddMonoidHom.toMultiplicative (PadicInt.toZModPow m).toAddMonoidHom)

Reduction modulo p ^ m, as a homomorphism Multiplicative ℤ_[p] →* Multiplicative (ZMod (p ^ m)) of the additive groups written multiplicatively, is continuous.

theorem TauCeti.surjective_toMultiplicative_toZModPow (p : ℕ) [Fact (Nat.Prime p)] (m : ℕ) : Function.Surjective ⇑(AddMonoidHom.toMultiplicative (PadicInt.toZModPow m).toAddMonoidHom)

Reduction modulo p ^ m, as a homomorphism Multiplicative ℤ_[p] →* Multiplicative (ZMod (p ^ m)) of the additive groups written multiplicatively, is surjective.

noncomputable def TauCeti.padicIntLevel (p : ℕ) [Fact (Nat.Prime p)] (m : ℕ) : OpenNormalSubgroup (Multiplicative ℤ_[p])

The level p ^ m of ℤ_p. The open normal subgroup p ^ m ℤ_p of Multiplicative ℤ_[p], the kernel of reduction modulo p ^ m. It consists of the multiples of p ^ m (mem_padicIntLevel_iff), has index p ^ m (index_padicIntLevel), and the levels are cofinal among the open subgroups (exists_padicIntLevel_le).

Equations

• TauCeti.padicIntLevel p m = (TauCeti.openNormalSubgroupBot (Multiplicative (ZMod (p ^ m)))).comap (AddMonoidHom.toMultiplicative (PadicInt.toZModPow m).toAddMonoidHom) ⋯

theorem TauCeti.padicIntLevel_toSubgroup (p : ℕ) [Fact (Nat.Prime p)] (m : ℕ) : ↑(padicIntLevel p m).toOpenSubgroup = (AddMonoidHom.toMultiplicative (PadicInt.toZModPow m).toAddMonoidHom).ker

The underlying subgroup of the level p ^ m is the kernel of reduction modulo p ^ m.

@[simp]

theorem TauCeti.mem_padicIntLevel_iff (p : ℕ) [Fact (Nat.Prime p)] (m : ℕ) {x : Multiplicative ℤ_[p]} : x ∈ padicIntLevel p m ↔ ↑p ^ m ∣ Multiplicative.toAdd x

The level p ^ m of ℤ_p consists of the multiples of p ^ m.

@[simp]

theorem TauCeti.index_padicIntLevel (p : ℕ) [Fact (Nat.Prime p)] (m : ℕ) : (↑(padicIntLevel p m).toOpenSubgroup).index = p ^ m

The level p ^ m of ℤ_p has index p ^ m.

theorem TauCeti.exists_padicIntLevel_le (p : ℕ) [Fact (Nat.Prime p)] (U : OpenSubgroup (Multiplicative ℤ_[p])) : ∃ (m : ℕ), (padicIntLevel p m).toOpenSubgroup ≤ U

The levels of ℤ_p are cofinal. Every open subgroup of Multiplicative ℤ_[p] contains the level p ^ m ℤ_p for some m: an open subgroup contains a ball around 1, and the balls around 1 are the levels.

theorem TauCeti.isProP_multiplicative_padicInt (p : ℕ) [Fact (Nat.Prime p)] : IsProP p (Multiplicative ℤ_[p])

The additive group of the p-adic integers, written multiplicatively, is pro-p: every open normal subgroup contains a level p ^ m ℤ_p, whose quotient is ℤ ⧸ p ^ m.

@[simp]

theorem TauCeti.profiniteOrder_multiplicative_padicInt (p : ℕ) [Fact (Nat.Prime p)] : profiniteOrder (Multiplicative ℤ_[p]) = Supernatural.primePower ⟨p, ⋯⟩ ⊤

The supernatural order of ℤ_p is p ^ ∞. The additive group of the p-adic integers is pro-p, so no other prime divides its order, and its quotient by the level p ^ m ℤ_p has order p ^ m for every m.

@[simp]

theorem TauCeti.topologicallyGenerates_ofAdd_one_padicInt (p : ℕ) [Fact (Nat.Prime p)] : (Subgroup.closure {Multiplicative.ofAdd 1}).topologicalClosure = ⊤

The element 1 : ℤ_[p] topologically generates the additive group of the p-adic integers.

theorem TauCeti.isTopologicallyFinitelyGenerated_multiplicative_padicInt (p : ℕ) [Fact (Nat.Prime p)] : IsTopologicallyFinitelyGenerated (Multiplicative ℤ_[p])

The additive group of the p-adic integers is topologically finitely generated.

@[simp]

theorem TauCeti.topologicalGeneratorRankNat_multiplicative_padicInt (p : ℕ) [Fact (Nat.Prime p)] : topologicalGeneratorRankNat (Multiplicative ℤ_[p]) ⋯ = 1

The natural-number topological generator rank of the additive group of ℤ_[p] is one.

@[simp]

theorem TauCeti.topologicalGeneratorRank_multiplicative_padicInt (p : ℕ) [Fact (Nat.Prime p)] : topologicalGeneratorRank (Multiplicative ℤ_[p]) = 1

The cardinal-valued topological generator rank of the additive group of ℤ_[p] is one.

The universal property of ℤ_p among pro-p groups

theorem TauCeti.continuousMonoidHom_ext_multiplicative_padicInt {p : ℕ} [Fact (Nat.Prime p)] {Q : Type u_1} [Monoid Q] [TopologicalSpace Q] [T2Space Q] {f g : Multiplicative ℤ_[p] →ₜ* Q} (h : f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)) : f = g

Two continuous homomorphisms out of the additive group of the p-adic integers into a Hausdorff monoid that agree at 1 are equal.

theorem TauCeti.continuousMonoidHom_ext_multiplicative_padicInt_iff {p : ℕ} [Fact (Nat.Prime p)] {Q : Type u_1} [Monoid Q] [TopologicalSpace Q] [T2Space Q] {f g : Multiplicative ℤ_[p] →ₜ* Q} : f = g ↔ f (Multiplicative.ofAdd 1) = g (Multiplicative.ofAdd 1)

noncomputable def TauCeti.IsProP.padicPowHom {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (a : P) : Multiplicative ℤ_[p] →ₜ* P

The p-adic power as a homomorphism out of ℤ_p. For an element a of a pro-p group, hP.padicPowHom a is the continuous homomorphism Multiplicative ℤ_[p] →ₜ* P sending l to the p-adic power a ^ l, so 1 ↦ a. It is the unique continuous homomorphism with that value at 1, by TauCeti.IsProP.padicPowHom_unique.

Equations

• hP.padicPowHom a = { toFun := fun (l : Multiplicative ℤ_[p]) => hP.padicPow a (Multiplicative.toAdd l), map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }

@[simp]

theorem TauCeti.IsProP.padicPowHom_apply {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (a : P) (l : Multiplicative ℤ_[p]) : (hP.padicPowHom a) l = hP.padicPow a (Multiplicative.toAdd l)

The homomorphism TauCeti.IsProP.padicPowHom evaluates as the p-adic power.

theorem TauCeti.IsProP.padicPowHom_ofAdd_one {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (a : P) : (hP.padicPowHom a) (Multiplicative.ofAdd 1) = a

The homomorphism TauCeti.IsProP.padicPowHom a sends 1 to a.

theorem TauCeti.IsProP.eq_padicPowHom {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : Multiplicative ℤ_[p] →ₜ* P) : f = hP.padicPowHom (f (Multiplicative.ofAdd 1))

A continuous homomorphism from the additive group of ℤ_[p] into a pro-p group is the p-adic power map of its value at 1.

theorem TauCeti.IsProP.padicPowHom_unique {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a : P} (f : Multiplicative ℤ_[p] →ₜ* P) (hf : f (Multiplicative.ofAdd 1) = a) : f = hP.padicPowHom a

A continuous homomorphism from the additive group of ℤ_[p] into a pro-p group sending 1 to a is TauCeti.IsProP.padicPowHom a.

theorem TauCeti.IsProP.existsUnique_continuousMonoidHom_multiplicative_padicInt {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (a : P) : ∃! f : Multiplicative ℤ_[p] →ₜ* P, f (Multiplicative.ofAdd 1) = a

The universal property of ℤ_p among pro-p groups. For every element a of a pro-p group there is a unique continuous homomorphism from the additive group of ℤ_[p] sending 1 to a.

@[simp]

theorem TauCeti.IsProP.comp_padicPowHom {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] {Q : Type u_2} [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] [CompactSpace Q] [TotallyDisconnectedSpace Q] (hP : IsProP p P) (hQ : IsProP p Q) (g : P →ₜ* Q) (a : P) : g.comp (hP.padicPowHom a) = hQ.padicPowHom (g a)

The homomorphism TauCeti.IsProP.padicPowHom is natural in the target.

theorem TauCeti.IsProP.topologicalClosure_closure_singleton_eq_range_padicPowHom {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (a : P) : (Subgroup.closure {a}).topologicalClosure = (↑(hP.padicPowHom a)).range

The closed subgroup topologically generated by an element a of a pro-p group is the range of its p-adic power map l ↦ a ^ l.

theorem TauCeti.IsProP.mem_topologicalClosure_closure_singleton_iff {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a x : P} : x ∈ (Subgroup.closure {a}).topologicalClosure ↔ ∃ (l : ℤ_[p]), hP.padicPow a l = x

An element of a pro-p group lies in the closed subgroup topologically generated by a exactly when it is a p-adic power of a.

theorem TauCeti.IsProP.exists_padicPow_mul_padicPow_eq_of_commute {p : ℕ} [Fact (Nat.Prime p)] {P : Type u_1} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) {a b : P} (hab : Commute a b) (hgen : (Subgroup.closure {a, b}).topologicalClosure = ⊤) (g : P) : ∃ (s : ℤ_[p]) (t : ℤ_[p]), hP.padicPow a s * hP.padicPow b t = g

A pro-p group topologically generated by two commuting elements consists of the products of their p-adic powers: every element is a ^ s * b ^ t for some s t : ℤ_[p].

@[simp]

theorem TauCeti.IsProP.padicPow_ofAdd_one_padicInt (p : ℕ) [Fact (Nat.Prime p)] (l : ℤ_[p]) : ⋯.padicPow (Multiplicative.ofAdd 1) l = Multiplicative.ofAdd l

In the additive group of ℤ_[p], the p-adic power of 1 by l is l itself.

@[simp]

theorem TauCeti.IsProP.padicPowHom_ofAdd_one_padicInt (p : ℕ) [Fact (Nat.Prime p)] : ⋯.padicPowHom (Multiplicative.ofAdd 1) = ContinuousMonoidHom.id (Multiplicative ℤ_[p])

The p-adic power homomorphism of 1 in the additive group of ℤ_[p] is the identity.

theorem TauCeti.toAdd_apply_multiplicative_padicInt {p : ℕ} [Fact (Nat.Prime p)] (f : Multiplicative ℤ_[p] →ₜ* Multiplicative ℤ_[p]) (x : Multiplicative ℤ_[p]) : Multiplicative.toAdd (f x) = Multiplicative.toAdd (f (Multiplicative.ofAdd 1)) * Multiplicative.toAdd x

A continuous endomorphism of the additive group of ℤ_[p] is multiplication by its value at 1.

Powers of ℤ_p

theorem TauCeti.isProP_multiplicative_pi_padicInt (p : ℕ) [Fact (Nat.Prime p)] (X : Type u_1) : IsProP p (Multiplicative (X → ℤ_[p]))

The additive group ℤ_[p] ^ X is pro-p.

@[simp]

theorem TauCeti.IsProP.padicPow_ofAdd_pi (p : ℕ) [Fact (Nat.Prime p)] (X : Type u_1) (v : X → ℤ_[p]) (l : ℤ_[p]) : ⋯.padicPow (Multiplicative.ofAdd v) l = Multiplicative.ofAdd (l • v)

In ℤ_[p] ^ X the p-adic power of a vector v by l is l • v.

theorem TauCeti.IsProP.map_padicPow_pi {p : ℕ} [Fact (Nat.Prime p)] {X : Type u_1} {P : Type u_2} [Group P] [TopologicalSpace P] [IsTopologicalGroup P] [CompactSpace P] [TotallyDisconnectedSpace P] (hP : IsProP p P) (f : P →ₜ* Multiplicative (X → ℤ_[p])) (y : P) (l : ℤ_[p]) : f (hP.padicPow y l) = Multiplicative.ofAdd (l • Multiplicative.toAdd (f y))

A continuous homomorphism from a pro-p group to ℤ_[p] ^ X carries the p-adic power by l to the scalar multiple by l.

theorem TauCeti.topologicallyGenerates_ofAdd_single_padicInt (p : ℕ) [Fact (Nat.Prime p)] (X : Type u_1) [DecidableEq X] : (Subgroup.closure (Set.range fun (x : X) => Multiplicative.ofAdd (Pi.single x 1))).topologicalClosure = ⊤

The coordinate vectors topologically generate the additive group ℤ_[p] ^ X: the closed subgroup they generate contains every vector supported at one coordinate, because the integers are dense in ℤ_[p], hence every finitely supported vector, and these are dense in the product topology.

theorem TauCeti.isTopologicallyFinitelyGenerated_multiplicative_pi_padicInt (p : ℕ) [Fact (Nat.Prime p)] (X : Type u_1) [Finite X] : IsTopologicallyFinitelyGenerated (Multiplicative (X → ℤ_[p]))

ℤ_p^X is topologically finitely generated for finite X, by the coordinate vectors.

theorem TauCeti.continuousMonoidHom_ext_multiplicative_pi_padicInt (p : ℕ) [Fact (Nat.Prime p)] (X : Type u_1) [DecidableEq X] {Q : Type u_2} [Monoid Q] [TopologicalSpace Q] [T2Space Q] {f g : Multiplicative (X → ℤ_[p]) →ₜ* Q} (h : ∀ (x : X), f (Multiplicative.ofAdd (Pi.single x 1)) = g (Multiplicative.ofAdd (Pi.single x 1))) : f = g

Two continuous homomorphisms out of the additive group ℤ_[p] ^ X into a Hausdorff monoid that agree on the coordinate vectors are equal.