The maximal pro-p quotient of the profinite integers is ℤ_p

The maximal pro-p quotient of the profinite integers ℤ̂ is the additive group of the p-adic integers, maximalProPQuotient p zHat ≃ₜ* Multiplicative ℤ_[p], by an isomorphism carrying the class of the generator zHat.gen to 1. Since a Sylow pro-p subgroup of a commutative profinite group maps isomorphically onto the maximal pro-p quotient, every p-Sylow subgroup of ℤ̂ is topologically isomorphic to ℤ_p.

Equivalently, the quotient is the inverse limit of the finite cyclic groups Multiplicative (ZMod (p ^ n)). The comparison is the composite with the inverse-limit presentation of ℤ_[p], and sends the class of zHat.gen to the compatible family of ones.

These are the rank-one instances of the pro-p theory: a continuous homomorphism from ℤ̂ to a pro-p group factors through ℤ_p, and the p-part of ℤ̂ may be read off from either the quotient or a Sylow subgroup.

Main definitions

• TauCeti.zHat.maximalProPQuotientEquivPadicInt: the maximal pro-p quotient of ℤ̂ is the additive group of ℤ_[p].
• TauCeti.zHat.maximalProPQuotientEquivZModPowLimit: the same quotient is the inverse limit of the groups Multiplicative (ZMod (p ^ n)).
• TauCeti.IsProPSylow.continuousMulEquivPadicInt: every p-Sylow subgroup of ℤ̂ is the additive group of ℤ_[p].

Main results

• TauCeti.zHat.maximalProPQuotientEquivPadicInt_mk_gen, TauCeti.zHat.maximalProPQuotientEquivPadicInt_symm_apply: the isomorphism sends the class of the generator to 1, and its inverse is the p-adic power of that class.
• TauCeti.zHat.profiniteOrder_eq_top: the supernatural order of ℤ̂ is ∏_ℓ ℓ ^ ∞, since ℤ̂ maps onto every ℤ_ℓ.

References

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

noncomputable def TauCeti.zHat.maximalProPQuotientEquivPadicInt (p : ℕ) [Fact (Nat.Prime p)] : maximalProPQuotient p ↑zHat.toProfinite.toTop ≃ₜ* Multiplicative ℤ_[p]

The maximal pro-p quotient of ℤ̂ is ℤ_p. The isomorphism maximalProPQuotient p zHat ≃ₜ* Multiplicative ℤ_[p] is induced by the inclusion ℤ → ℤ_[p] and carries the class of the generator to 1; its inverse is the p-adic power of that class. Both groups represent the same functor on pro-p groups, a continuous homomorphism out of either being an element of the target, which is what forces the two to agree.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.zHat.maximalProPQuotientEquivPadicInt_mk (p : ℕ) [Fact (Nat.Prime p)] (x : ↑zHat.toProfinite.toTop) : (maximalProPQuotientEquivPadicInt p) ↑x = (lift (Multiplicative.ofAdd 1)) x

The isomorphism from the maximal pro-p quotient of ℤ̂ to ℤ_p is the factorisation of the lift of 1 ∈ ℤ_[p] through the quotient map.

theorem TauCeti.zHat.maximalProPQuotientEquivPadicInt_mk_gen (p : ℕ) [Fact (Nat.Prime p)] : (maximalProPQuotientEquivPadicInt p) ↑gen = Multiplicative.ofAdd 1

The isomorphism from the maximal pro-p quotient of ℤ̂ to ℤ_p sends the class of the generator to 1.

@[simp]

theorem TauCeti.zHat.maximalProPQuotientEquivPadicInt_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (l : Multiplicative ℤ_[p]) : (maximalProPQuotientEquivPadicInt p).symm l = ⋯.padicPow (↑gen) (Multiplicative.toAdd l)

The inverse isomorphism from ℤ_p to the maximal pro-p quotient of ℤ̂ is the p-adic power of the class of the generator.

noncomputable def TauCeti.zHat.maximalProPQuotientEquivZModPowLimit (p : ℕ) [Fact (Nat.Prime p)] : maximalProPQuotient p ↑zHat.toProfinite.toTop ≃ₜ* Multiplicative ↥(PadicInt.inverseLimit p)

The maximal pro-p quotient of ℤ̂ is the inverse limit of ℤ/p^nℤ. This is the canonical comparison obtained by taking all residues of the p-adic integer associated to an element of the maximal pro-p quotient.

Equations

• TauCeti.zHat.maximalProPQuotientEquivZModPowLimit p = (TauCeti.zHat.maximalProPQuotientEquivPadicInt p).trans (PadicInt.inverseLimitContinuousMulEquiv p)

@[simp]

theorem TauCeti.zHat.maximalProPQuotientEquivZModPowLimit_mk (p : ℕ) [Fact (Nat.Prime p)] (x : ↑zHat.toProfinite.toTop) : (maximalProPQuotientEquivZModPowLimit p) ↑x = Multiplicative.ofAdd ((PadicInt.toInverseLimit p) (Multiplicative.toAdd ((lift (Multiplicative.ofAdd 1)) x)))

The inverse-limit comparison takes a class from ℤ̂ to the compatible family of residues of its image in ℤ_p.

theorem TauCeti.zHat.maximalProPQuotientEquivZModPowLimit_mk_gen (p : ℕ) [Fact (Nat.Prime p)] : (maximalProPQuotientEquivZModPowLimit p) ↑gen = Multiplicative.ofAdd ((PadicInt.toInverseLimit p) 1)

The inverse-limit comparison sends the class of the generator of ℤ̂ to the compatible family of residues of 1.

theorem TauCeti.zHat.maximalProPQuotientEquivZModPowLimit_mk_proj (p : ℕ) [Fact (Nat.Prime p)] (x : ↑zHat.toProfinite.toTop) (n : ℕ) : (PadicInt.inverseLimit.proj p n) (Multiplicative.toAdd ((maximalProPQuotientEquivZModPowLimit p) ↑x)) = (PadicInt.toZModPow n) (Multiplicative.toAdd ((lift (Multiplicative.ofAdd 1)) x))

The nth coordinate of the inverse-limit comparison is reduction modulo p ^ n after the canonical map from ℤ̂ to ℤ_p.

theorem TauCeti.zHat.maximalProPQuotientEquivZModPowLimit_mk_gen_proj (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : (PadicInt.inverseLimit.proj p n) (Multiplicative.toAdd ((maximalProPQuotientEquivZModPowLimit p) ↑gen)) = 1

Each coordinate of the image of the generator of ℤ̂ in the inverse limit is 1.

@[simp]

theorem TauCeti.zHat.profiniteOrder_eq_top : profiniteOrder ↑zHat.toProfinite.toTop = ⊤

The supernatural order of ℤ̂ is ∏_ℓ ℓ ^ ∞, the greatest supernatural number. For every prime ℓ, ℤ̂ maps continuously onto its maximal pro-ℓ quotient ℤ_ℓ, whose order is ℓ ^ ∞.

noncomputable def TauCeti.IsProPSylow.continuousMulEquivPadicInt {p : ℕ} [Fact (Nat.Prime p)] {P : Subgroup ↑zHat.toProfinite.toTop} (hP : IsProPSylow p P) : ↥P ≃ₜ* Multiplicative ℤ_[p]

Every p-Sylow subgroup of ℤ̂ is ℤ_p: the quotient map to the maximal pro-p quotient restricts to a topological group isomorphism from the Sylow subgroup, and that quotient is the additive group of ℤ_[p].

Equations

• hP.continuousMulEquivPadicInt = hP.continuousMulEquivMaximalProPQuotient.trans (TauCeti.zHat.maximalProPQuotientEquivPadicInt p)

@[simp]

theorem TauCeti.IsProPSylow.continuousMulEquivPadicInt_apply {p : ℕ} [Fact (Nat.Prime p)] {P : Subgroup ↑zHat.toProfinite.toTop} (hP : IsProPSylow p P) (x : ↥P) : hP.continuousMulEquivPadicInt x = (zHat.maximalProPQuotientEquivPadicInt p) ((maximalProPQuotient.mk p ↑zHat.toProfinite.toTop) ↑x)

The isomorphism from a p-Sylow subgroup of ℤ̂ to ℤ_p is the composite of the quotient map to the maximal pro-p quotient with its identification with ℤ_p.