The profinite integers as the inverse limit of the ZMod n

The ring of profinite integers Additive zHat (see TauCeti.Topology.Algebra.Group.Profinite.ZHat.Ring) projects onto every finite quotient ZMod n of ℤ, and is determined by these projections: it is the inverse limit of the rings ZMod n along the reduction maps ZMod.castHom. This file builds the projections and proves that limit property, in the form of a universal property for ring homomorphisms into Additive zHat.

The projection zHat.toZMod n is the continuous homomorphism zHat.lift (ofAdd 1) into the finite discrete group Multiplicative (ZMod n), read additively; it is a ring homomorphism for the product of Additive zHat, and the projections are compatible along divisibility (zHat.cast_toZMod). Every open normal subgroup of zHat contains the kernel of some projection (zHat.exists_monoidHom_mk_eq_toZMod), so two profinite integers with the same projections are equal (zHat.ext_of_toZMod), a map into the profinite integers is continuous as soon as its projections are (zHat.continuous_iff_forall_continuous_toZMod), and a compatible family of residues is realized by a unique profinite integer (zHat.existsUnique_forall_toZMod_eq). The last statement assembles a compatible family of ring homomorphisms R →+* ZMod n into a unique ring homomorphism zHat.ringLift f : R →+* Additive zHat, continuous when every member of the family is. The integers embed into the profinite integers: Additive zHat has characteristic zero.

The index n of the finite levels runs over ℕ+: for n = 0 the group Multiplicative (ZMod 0) is ℤ, which is not profinite, and no lift exists.

Main definitions

• TauCeti.zHat.toZMod: reduction of a profinite integer modulo n, a continuous ring homomorphism Additive zHat →+* ZMod n.
• TauCeti.zHat.ringLift: the ring homomorphism into Additive zHat assembled from a compatible family of ring homomorphisms into the ZMod n.

Main results

• TauCeti.zHat.cast_toZMod, TauCeti.zHat.castHom_comp_toZMod: the projections are compatible along divisibility.
• TauCeti.zHat.ext_of_toZMod, TauCeti.zHat.ext_iff_toZMod, TauCeti.zHat.existsUnique_forall_toZMod_eq: a profinite integer is determined by its projections, and every compatible family of residues comes from one.
• TauCeti.zHat.toZMod_ringLift, TauCeti.zHat.ringLift_unique, TauCeti.zHat.continuous_ringLift: the universal property of Additive zHat as the inverse limit of the ZMod n.
• TauCeti.zHat.continuous_iff_forall_continuous_toZMod: continuity into Additive zHat is detected by the projections.
• The CharZero (Additive zHat) instance and TauCeti.zHat.ofInt_injective: the integers embed into the profinite integers.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Sections 2.3 and 4.1.
• Mathlib's Mathlib.NumberTheory.Padics.RingHoms, the same inverse-limit API for the p-adic integers, whose structure this file follows: PadicInt.toZModPow, PadicInt.cast_toZModPow, PadicInt.zmod_cast_comp_toZModPow, PadicInt.ext_of_toZModPow, PadicInt.lift, PadicInt.lift_spec, PadicInt.lift_unique and PadicInt.lift_self correspond to TauCeti.zHat.toZMod, TauCeti.zHat.cast_toZMod, TauCeti.zHat.castHom_comp_toZMod, TauCeti.zHat.ext_iff_toZMod, TauCeti.zHat.ringLift, TauCeti.zHat.toZMod_comp_ringLift, TauCeti.zHat.ringLift_unique and TauCeti.zHat.ringLift_toZMod.

noncomputable def TauCeti.zHat.toZMod (n : ℕ+) : Additive ↑zHat.toProfinite.toTop →+* ZMod ↑n

Reduction modulo n. The projection of the profinite integers onto ZMod n is the continuous homomorphism zHat.lift (ofAdd 1) into the finite discrete group Multiplicative (ZMod n), read additively. It is a ring homomorphism for the product of Additive zHat, and the profinite integers are the inverse limit of these projections (zHat.existsUnique_forall_toZMod_eq).

Equations

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

theorem TauCeti.zHat.toZMod_apply (n : ℕ+) (a : Additive ↑zHat.toProfinite.toTop) : (toZMod n) a = Multiplicative.toAdd ((lift (Multiplicative.ofAdd 1)) (Additive.toMul a))

The reduction of a modulo n is the lift of the generator of Multiplicative (ZMod n), evaluated at a.toMul and read additively.

@[simp]

theorem TauCeti.zHat.lift_ofAdd_one_apply {n : ℕ+} (x : ↑zHat.toProfinite.toTop) : (lift (Multiplicative.ofAdd 1)) x = Multiplicative.ofAdd ((toZMod n) (Additive.ofMul x))

The lift of the generator of Multiplicative (ZMod n) is reduction modulo n, read multiplicatively.

theorem TauCeti.zHat.continuous_toZMod (n : ℕ+) : Continuous ⇑(toZMod n)

Reduction modulo n is continuous.

@[simp]

theorem TauCeti.zHat.cast_toZMod {m n : ℕ+} (h : ↑m ∣ ↑n) (a : Additive ↑zHat.toProfinite.toTop) : ((toZMod n) a).cast = (toZMod m) a

Compatibility of the projections along divisibility. Reducing modulo n and then modulo a divisor m of n is reducing modulo m.

theorem TauCeti.zHat.castHom_comp_toZMod {m n : ℕ+} (h : ↑m ∣ ↑n) : (ZMod.castHom h (ZMod ↑m)).comp (toZMod n) = toZMod m

Compatibility of the projections along divisibility, as an equality of ring homomorphisms: ZMod.castHom after reduction modulo n is reduction modulo a divisor m of n.

theorem TauCeti.zHat.exists_monoidHom_mk_eq_toZMod (U : OpenNormalSubgroup ↑zHat.toProfinite.toTop) : ∃ (n : ℕ+) (ψ : Multiplicative (ZMod ↑n) →* ↑zHat.toProfinite.toTop ⧸ ↑U.toOpenSubgroup), ∀ (a : Additive ↑zHat.toProfinite.toTop), ↑(Additive.toMul a) = ψ (Multiplicative.ofAdd ((toZMod n) a))

Every finite quotient of ℤ̂ factors through a finite level. For an open normal subgroup U of zHat there is a level n and a homomorphism ψ from Multiplicative (ZMod n) to zHat ⧸ U such that the quotient map is ψ after reduction modulo n. In particular U contains the kernel of toZMod n.

theorem TauCeti.zHat.ext_of_toZMod {a b : Additive ↑zHat.toProfinite.toTop} (h : ∀ (n : ℕ+), (toZMod n) a = (toZMod n) b) : a = b

A profinite integer is determined by its projections.

theorem TauCeti.zHat.ext_iff_toZMod {a b : Additive ↑zHat.toProfinite.toTop} : a = b ↔ ∀ (n : ℕ+), (toZMod n) a = (toZMod n) b

Two profinite integers are equal exactly when their reductions modulo every n agree.

theorem TauCeti.zHat.continuous_iff_forall_continuous_toZMod {X : Type u_1} [TopologicalSpace X] {f : X → Additive ↑zHat.toProfinite.toTop} : Continuous f ↔ ∀ (n : ℕ+), Continuous fun (x : X) => (toZMod n) (f x)

Continuity into ℤ̂ is detected by the projections. A map into the profinite integers is continuous exactly when all of its reductions modulo n are.

instance TauCeti.zHat.instCharZeroAdditiveCarrierToTopTotallyDisconnectedSpaceToProfinite : CharZero (Additive ↑zHat.toProfinite.toTop)

The integers embed into the profinite integers: no positive integer reduces to zero modulo every n.

theorem TauCeti.zHat.ofInt_injective : Function.Injective ⇑ofInt

The canonical homomorphism from ℤ to the profinite integers is injective.

theorem TauCeti.zHat.existsUnique_forall_toZMod_eq (x : (n : ℕ+) → ZMod ↑n) (hx : ∀ (m n : ℕ+) (h : ↑m ∣ ↑n), (ZMod.castHom h (ZMod ↑m)) (x n) = x m) : ∃! a : Additive ↑zHat.toProfinite.toTop, ∀ (n : ℕ+), (toZMod n) a = x n

The profinite integers are the inverse limit of the ZMod n. A family of residues x n : ZMod n, compatible along the reduction maps, is realized by a unique profinite integer.

noncomputable def TauCeti.zHat.ringLift {R : Type v} [NonAssocSemiring R] (f : (n : ℕ+) → R →+* ZMod ↑n) (hf : ∀ (m n : ℕ+) (h : ↑m ∣ ↑n), (ZMod.castHom h (ZMod ↑m)).comp (f n) = f m) : R →+* Additive ↑zHat.toProfinite.toTop

The universal property of ℤ̂ as an inverse limit. A family of ring homomorphisms f n : R →+* ZMod n, compatible along the reduction maps, assembles into the ring homomorphism R →+* Additive zHat whose reduction modulo n is f n (zHat.toZMod_ringLift); it is the only one (zHat.ringLift_unique).

Equations

• TauCeti.zHat.ringLift f hf = { toFun := fun (r : R) => ⋯.choose, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem TauCeti.zHat.toZMod_ringLift {R : Type v} [NonAssocSemiring R] (f : (n : ℕ+) → R →+* ZMod ↑n) (hf : ∀ (m n : ℕ+) (h : ↑m ∣ ↑n), (ZMod.castHom h (ZMod ↑m)).comp (f n) = f m) (n : ℕ+) (r : R) : (toZMod n) ((ringLift f hf) r) = (f n) r

The reduction modulo n of the assembled ring homomorphism is the n-th member of the family.

theorem TauCeti.zHat.toZMod_comp_ringLift {R : Type v} [NonAssocSemiring R] (f : (n : ℕ+) → R →+* ZMod ↑n) (hf : ∀ (m n : ℕ+) (h : ↑m ∣ ↑n), (ZMod.castHom h (ZMod ↑m)).comp (f n) = f m) (n : ℕ+) : (toZMod n).comp (ringLift f hf) = f n

The reduction modulo n of the assembled ring homomorphism is the n-th member of the family, as an equality of ring homomorphisms.

theorem TauCeti.zHat.ringLift_unique {R : Type v} [NonAssocSemiring R] (f : (n : ℕ+) → R →+* ZMod ↑n) (hf : ∀ (m n : ℕ+) (h : ↑m ∣ ↑n), (ZMod.castHom h (ZMod ↑m)).comp (f n) = f m) (g : R →+* Additive ↑zHat.toProfinite.toTop) (hg : ∀ (n : ℕ+), (toZMod n).comp g = f n) : g = ringLift f hf

A ring homomorphism into ℤ̂ whose reductions are the members of the family is the assembled ring homomorphism.

theorem TauCeti.zHat.ringLift_comp {R : Type v} [NonAssocSemiring R] (f : (n : ℕ+) → R →+* ZMod ↑n) (hf : ∀ (m n : ℕ+) (h : ↑m ∣ ↑n), (ZMod.castHom h (ZMod ↑m)).comp (f n) = f m) {S : Type u_1} [NonAssocSemiring S] (g : S →+* R) : (ringLift f hf).comp g = ringLift (fun (n : ℕ+) => (f n).comp g) ⋯

Naturality of the universal property in R. Precomposing the assembled ring homomorphism with g : S →+* R assembles the precomposed family.

theorem TauCeti.zHat.continuous_ringLift {R : Type v} [NonAssocSemiring R] (f : (n : ℕ+) → R →+* ZMod ↑n) (hf : ∀ (m n : ℕ+) (h : ↑m ∣ ↑n), (ZMod.castHom h (ZMod ↑m)).comp (f n) = f m) [TopologicalSpace R] (hcont : ∀ (n : ℕ+), Continuous ⇑(f n)) : Continuous ⇑(ringLift f hf)

The assembled ring homomorphism is continuous as soon as every member of the family is.

theorem TauCeti.zHat.ringLift_toZMod : ringLift (fun (n : ℕ+) => toZMod n) ⋯ = RingHom.id (Additive ↑zHat.toProfinite.toTop)

Assembling the projections themselves gives the identity of ℤ̂.