The p-adic integers as an inverse limit

The ring of p-adic integers is the inverse limit of the finite rings ZMod (p ^ n). This file gives that inverse limit a concrete carrier: a point is a family whose finer residues reduce to its coarser residues. Mathlib's universal maps PadicInt.toZModPow and PadicInt.lift identify this ring with ℤ_[p].

The topology on the inverse limit is the subspace topology from the product of the discrete finite rings; the compatibility conditions are closed, so the inverse limit is compact for every nonzero modulus. The algebraic equivalence is a homeomorphism because its forward map is continuous and ℤ_[p] is compact.

Main definitions

• PadicInt.inverseLimit: the ring of compatible families in ∏ n, ZMod (p ^ n).
• PadicInt.inverseLimit.lift: the universal map into the inverse limit determined by a compatible family of ring homomorphisms.
• PadicInt.toInverseLimit: the compatible family of residues of a p-adic integer.
• PadicInt.inverseLimitRingEquiv: the ring equivalence from ℤ_[p] to the inverse limit.
• PadicInt.inverseLimitHomeomorph: the same equivalence as a homeomorphism.
• PadicInt.inverseLimitContinuousMulEquiv: the corresponding topological isomorphism of additive groups, written multiplicatively.

References

• J.-P. Serre, Local Fields, Chapter II, Section 2.

def PadicInt.inverseLimit (p : ℕ) : Subring ((n : ℕ) → ZMod (p ^ n))

The inverse limit of the rings ZMod (p ^ n): compatible residue families, with the subspace topology inherited from their product.

Equations

• PadicInt.inverseLimit p = { carrier := {x : (n : ℕ) → ZMod (p ^ n) | ∀ ⦃m n : ℕ⦄, m ≤ n → (x n).cast = x m}, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

theorem PadicInt.mem_inverseLimit_iff {p : ℕ} {x : (n : ℕ) → ZMod (p ^ n)} : x ∈ inverseLimit p ↔ ∀ ⦃m n : ℕ⦄, m ≤ n → (x n).cast = x m

Membership in PadicInt.inverseLimit: a family belongs to the inverse limit exactly when each of its finer residues reduces to the coarser ones. Use .mpr to build an element of the inverse limit from a compatibility proof.

def PadicInt.inverseLimit.proj (p n : ℕ) : ↥(inverseLimit p) →+* ZMod (p ^ n)

The projection from the inverse limit to ZMod (p ^ n).

Equations

• PadicInt.inverseLimit.proj p n = (Pi.evalRingHom (fun (n : ℕ) => ZMod (p ^ n)) n).comp (PadicInt.inverseLimit p).subtype

@[simp]

theorem PadicInt.inverseLimit.proj_apply (p n : ℕ) (x : ↥(inverseLimit p)) : (proj p n) x = ↑x n

@[simp]

theorem PadicInt.inverseLimit.cast_proj (p m n : ℕ) (h : m ≤ n) : (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (proj p n) = proj p m

The projections from the inverse limit form a compatible family.

def PadicInt.inverseLimit.lift (p : ℕ) {R : Type u_1} [NonAssocSemiring R] (f : (n : ℕ) → R →+* ZMod (p ^ n)) (hf : ∀ (m n : ℕ) (h : m ≤ n), (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (f n) = f m) : R →+* ↥(inverseLimit p)

The universal property of the inverse limit: a family of ring homomorphisms f n : R →+* ZMod (p ^ n) compatible with the reduction maps assembles into a single ring homomorphism to PadicInt.inverseLimit p.

Equations

• PadicInt.inverseLimit.lift p f hf = (RingHom.pi f).codRestrict (PadicInt.inverseLimit p) ⋯

@[simp]

theorem PadicInt.inverseLimit.lift_apply (p : ℕ) {R : Type u_1} [NonAssocSemiring R] (f : (n : ℕ) → R →+* ZMod (p ^ n)) (hf : ∀ (m n : ℕ) (h : m ≤ n), (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (f n) = f m) (x : R) (n : ℕ) : ↑((lift p f hf) x) n = (f n) x

@[simp]

theorem PadicInt.inverseLimit.proj_comp_lift (p : ℕ) {R : Type u_1} [NonAssocSemiring R] (f : (n : ℕ) → R →+* ZMod (p ^ n)) (hf : ∀ (m n : ℕ) (h : m ≤ n), (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (f n) = f m) (n : ℕ) : (proj p n).comp (lift p f hf) = f n

PadicInt.inverseLimit.lift recovers the given family on each projection.

theorem PadicInt.inverseLimit.lift_unique (p : ℕ) {R : Type u_1} [NonAssocSemiring R] (f : (n : ℕ) → R →+* ZMod (p ^ n)) (hf : ∀ (m n : ℕ) (h : m ≤ n), (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (f n) = f m) (g : R →+* ↥(inverseLimit p)) (hg : ∀ (n : ℕ), (proj p n).comp g = f n) : g = lift p f hf

PadicInt.inverseLimit.lift is the only homomorphism recovering the given family on each projection.

theorem PadicInt.isClosed_inverseLimit (p : ℕ) : IsClosed ↑(inverseLimit p)

The compatible families are cut out of the product of the discrete rings ZMod (p ^ n) by closed conditions.

instance PadicInt.compactSpace_inverseLimit (p : ℕ) [NeZero p] : CompactSpace ↥(inverseLimit p)

The inverse limit of the finite rings ZMod (p ^ n) is compact.

noncomputable def PadicInt.toInverseLimit (p : ℕ) [Fact (Nat.Prime p)] : ℤ_[p] →+* ↥(inverseLimit p)

The residue family of a p-adic integer, regarded as a homomorphism to the inverse limit.

Equations

• PadicInt.toInverseLimit p = { toFun := fun (x : ℤ_[p]) => ⟨fun (n : ℕ) => (PadicInt.toZModPow n) x, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem PadicInt.inverseLimit_proj_toInverseLimit (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : (inverseLimit.proj p n).comp (toInverseLimit p) = toZModPow n

@[simp]

theorem PadicInt.toInverseLimit_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) (n : ℕ) : ↑((toInverseLimit p) x) n = (toZModPow n) x

noncomputable def PadicInt.fromInverseLimit (p : ℕ) [Fact (Nat.Prime p)] : ↥(inverseLimit p) →+* ℤ_[p]

A compatible residue family determines a p-adic integer by Mathlib's inverse-limit universal property.

Equations

• PadicInt.fromInverseLimit p = PadicInt.lift ⋯

@[simp]

theorem PadicInt.toZModPow_fromInverseLimit (p : ℕ) [Fact (Nat.Prime p)] (n : ℕ) : (toZModPow n).comp (fromInverseLimit p) = inverseLimit.proj p n

noncomputable def PadicInt.inverseLimitRingEquiv (p : ℕ) [Fact (Nat.Prime p)] : ℤ_[p] ≃+* ↥(inverseLimit p)

The ring of p-adic integers is the inverse limit of the rings ZMod (p ^ n).

Equations

• PadicInt.inverseLimitRingEquiv p = { toFun := ⇑(PadicInt.toInverseLimit p), invFun := ⇑(PadicInt.fromInverseLimit p), left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }

@[simp]

theorem PadicInt.inverseLimitRingEquiv_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) : (inverseLimitRingEquiv p) x = (toInverseLimit p) x

@[simp]

theorem PadicInt.inverseLimitRingEquiv_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ↥(inverseLimit p)) : (inverseLimitRingEquiv p).symm x = (fromInverseLimit p) x

theorem PadicInt.continuous_toInverseLimit (p : ℕ) [Fact (Nat.Prime p)] : Continuous ⇑(toInverseLimit p)

Taking all residues modulo p ^ n is continuous into their inverse limit.

theorem PadicInt.continuous_inverseLimitRingEquiv (p : ℕ) [Fact (Nat.Prime p)] : Continuous ⇑(inverseLimitRingEquiv p)

The ring equivalence from ℤ_[p] to its inverse-limit presentation is continuous.

noncomputable def PadicInt.inverseLimitHomeomorph (p : ℕ) [Fact (Nat.Prime p)] : ℤ_[p] ≃ₜ ↥(inverseLimit p)

The ring equivalence from ℤ_[p] to its inverse-limit presentation is a homeomorphism.

Equations

• PadicInt.inverseLimitHomeomorph p = ⋯.homeoOfEquivCompactToT2

@[simp]

theorem PadicInt.inverseLimitHomeomorph_toEquiv (p : ℕ) [Fact (Nat.Prime p)] : ↑(inverseLimitHomeomorph p) = ↑(inverseLimitRingEquiv p)

The underlying map of PadicInt.inverseLimitHomeomorph is the ring equivalence taking a p-adic integer to all of its residues.

noncomputable def PadicInt.inverseLimitContinuousMulEquiv (p : ℕ) [Fact (Nat.Prime p)] : Multiplicative ℤ_[p] ≃ₜ* Multiplicative ↥(inverseLimit p)

The additive group of ℤ_[p] is topologically isomorphic to the additive group of its inverse-limit presentation.

Equations

• PadicInt.inverseLimitContinuousMulEquiv p = { toMulEquiv := AddEquiv.toMultiplicative (PadicInt.inverseLimitRingEquiv p).toAddEquiv, continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem PadicInt.inverseLimitContinuousMulEquiv_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ℤ_[p]) : (inverseLimitContinuousMulEquiv p) (Multiplicative.ofAdd x) = Multiplicative.ofAdd ((toInverseLimit p) x)

@[simp]

theorem PadicInt.inverseLimitContinuousMulEquiv_symm_apply (p : ℕ) [Fact (Nat.Prime p)] (x : ↥(inverseLimit p)) : (inverseLimitContinuousMulEquiv p).symm (Multiplicative.ofAdd x) = Multiplicative.ofAdd ((fromInverseLimit p) x)