The product decomposition of the profinite integers

The ring of profinite integers Additive zHat is the product of the rings of ℓ-adic integers over all primes ℓ: the ring homomorphism Additive zHat →+* ∀ ℓ : Nat.Primes, ℤ_[ℓ] whose components are the ℓ-adic components zHat.component ℓ is an isomorphism of topological rings (zHat.ringEquivPiPadicInt, with zHat.continuous_ringEquivPiPadicInt and zHat.continuous_ringEquivPiPadicInt_symm).

Both halves of the bijectivity are the Chinese remainder theorem at each finite level. A residue modulo n is determined by its reductions modulo the prime powers dividing n, and reduction modulo ℓ ^ k factors through the ℓ-adic component (zHat.cast_toZMod_eq_toZModPow_component), so a profinite integer is determined by its components (zHat.ext_of_component). Conversely, a family of ℓ-adic integers reduces, at each level n, to a residue modulo n assembled by Mathlib's ZMod.equivPi from its reductions modulo the prime powers exactly dividing n; these residues are compatible along divisibility, hence come from a profinite integer by the limit property zHat.existsUnique_forall_toZMod_eq, whose components are the given family (zHat.exists_forall_component_eq). Continuity of the inverse is the compactness of zHat.

The decomposition has idempotents: zHat.idem ℓ, written ω_ℓ in prose, is the profinite integer with ℓ-adic component 1 and all other components 0. It is idempotent, orthogonal to the idempotents of the other primes, multiplication by it keeps the ℓ-adic component and kills the others, and it reduces to 1 modulo every power of ℓ and to 0 modulo every n prime to ℓ. It is unequal to every integer (zHat.idem_ne_intCast), so ℤ → ℤ̂ is not surjective (zHat.not_surjective_ofInt). In particular ω_2 * (1 - ω_2) = 0 with both factors nonzero: the profinite integers are not a domain (zHat.not_isDomain). The finite sums of the prime idempotents tend to 1 (zHat.tendsto_sum_idem), expressing recovery from the prime factors in the product topology.

Main definitions

• TauCeti.zHat.ringEquivPiPadicInt: the ring isomorphism Additive zHat ≃+* ∀ ℓ : Nat.Primes, ℤ_[ℓ] with components zHat.component ℓ.
• TauCeti.zHat.idem: the idempotent ω_ℓ of the ℓ-adic factor.

Main results

• TauCeti.zHat.ext_of_component, TauCeti.zHat.exists_forall_component_eq: a profinite integer is determined by its ℓ-adic components, and every family of ℓ-adic integers occurs.
• TauCeti.zHat.continuous_ringEquivPiPadicInt, TauCeti.zHat.continuous_ringEquivPiPadicInt_symm: the decomposition is an isomorphism of topological rings.
• TauCeti.zHat.component_idem, TauCeti.zHat.isIdempotentElem_idem, TauCeti.zHat.idem_mul_idem, TauCeti.zHat.idem_mul_idem_of_ne, TauCeti.zHat.idem_mul_eq_self_iff: the components of ω_ℓ, its idempotence and orthogonality, and the characterization of ω_ℓ * a = a.
• TauCeti.zHat.toZMod_idem_of_dvd_pow, TauCeti.zHat.toZMod_idem_of_not_dvd: the reductions of ω_ℓ at the finite levels.
• TauCeti.zHat.idem_ne_intCast: ω_ℓ is not an integer.
• TauCeti.zHat.not_surjective_ofInt: the integers are a proper subgroup of ℤ̂.
• TauCeti.zHat.not_isDomain: the profinite integers are not a domain.

References

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

theorem TauCeti.zHat.cast_toZMod_eq_toZModPow_component (n : ℕ+) {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℕ} (h : p ^ k ∣ ↑n) (a : Additive ↑zHat.toProfinite.toTop) : ((toZMod n) a).cast = (PadicInt.toZModPow k) ((component p) a)

Reduction modulo a prime power factors through the component. For p ^ k ∣ n, reducing a modulo n and then modulo p ^ k is reducing the p-adic component of a modulo p ^ k.

theorem TauCeti.zHat.ext_of_component {a b : Additive ↑zHat.toProfinite.toTop} (h : ∀ (ℓ : ℕ) [inst : Fact (Nat.Prime ℓ)], (component ℓ) a = (component ℓ) b) : a = b

A profinite integer is determined by its ℓ-adic components.

theorem TauCeti.zHat.ext_iff_component {a b : Additive ↑zHat.toProfinite.toTop} : a = b ↔ ∀ (ℓ : ℕ) [inst : Fact (Nat.Prime ℓ)], (component ℓ) a = (component ℓ) b

Two profinite integers are equal exactly when all their ℓ-adic components agree.

theorem TauCeti.zHat.exists_forall_component_eq (u : (ℓ : Nat.Primes) → ℤ_[↑ℓ]) : ∃ (a : Additive ↑zHat.toProfinite.toTop), ∀ (ℓ : Nat.Primes), (component ↑ℓ) a = u ℓ

Every family of ℓ-adic integers is the family of components of a profinite integer.

noncomputable def TauCeti.zHat.ringEquivPiPadicInt : Additive ↑zHat.toProfinite.toTop ≃+* ((ℓ : Nat.Primes) → ℤ_[↑ℓ])

The product decomposition of the profinite integers. The ring homomorphism from Additive zHat to ∀ ℓ : Nat.Primes, ℤ_[ℓ] with components the ℓ-adic components zHat.component ℓ is a ring isomorphism: injective by zHat.ext_of_component and surjective by zHat.exists_forall_component_eq. It is a homeomorphism (zHat.continuous_ringEquivPiPadicInt, zHat.continuous_ringEquivPiPadicInt_symm), so an isomorphism of topological rings.

@[simp]

theorem TauCeti.zHat.ringEquivPiPadicInt_apply (a : Additive ↑zHat.toProfinite.toTop) (ℓ : Nat.Primes) : ringEquivPiPadicInt a ℓ = (component ↑ℓ) a

The components of the product decomposition are the ℓ-adic components.

@[simp]

theorem TauCeti.zHat.component_ringEquivPiPadicInt_symm (u : (ℓ : Nat.Primes) → ℤ_[↑ℓ]) (ℓ : Nat.Primes) : (component ↑ℓ) (ringEquivPiPadicInt.symm u) = u ℓ

The ℓ-adic component of the profinite integer with prescribed components is the prescribed one.

theorem TauCeti.zHat.continuous_ringEquivPiPadicInt : Continuous ⇑ringEquivPiPadicInt

The product decomposition is continuous: each component is.

theorem TauCeti.zHat.continuous_ringEquivPiPadicInt_symm : Continuous ⇑ringEquivPiPadicInt.symm

The inverse of the product decomposition is continuous: a continuous bijection from the compact space Additive zHat to the Hausdorff space ∀ ℓ, ℤ_[ℓ] is a homeomorphism.

noncomputable def TauCeti.zHat.idem (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : Additive ↑zHat.toProfinite.toTop

The idempotent of the ℓ-adic factor. zHat.idem ℓ, written ω_ℓ, is the profinite integer with ℓ-adic component 1 and all other components 0 (zHat.component_idem).

@[simp]

theorem TauCeti.zHat.ringEquivPiPadicInt_idem (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : ringEquivPiPadicInt (idem ℓ) = Pi.single ⟨ℓ, ⋯⟩ 1

Under the product decomposition, ω_ℓ is the family with 1 at ℓ and 0 elsewhere.

@[simp]

theorem TauCeti.zHat.component_idem_self (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : (component ℓ) (idem ℓ) = 1

The ℓ-adic component of ω_ℓ is 1.

@[simp]

theorem TauCeti.zHat.component_idem_of_ne (ℓ : ℕ) [Fact (Nat.Prime ℓ)] {ℓ' : ℕ} [Fact (Nat.Prime ℓ')] (h : ℓ' ≠ ℓ) : (component ℓ') (idem ℓ) = 0

The components of ω_ℓ at the other primes vanish.

theorem TauCeti.zHat.component_idem (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (ℓ' : ℕ) [Fact (Nat.Prime ℓ')] : (component ℓ') (idem ℓ) = if ℓ' = ℓ then 1 else 0

The components of ω_ℓ: 1 at ℓ and 0 at every other prime.

theorem TauCeti.zHat.isIdempotentElem_idem (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : IsIdempotentElem (idem ℓ)

ω_ℓ is idempotent.

@[simp]

theorem TauCeti.zHat.idem_mul_idem (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : idem ℓ * idem ℓ = idem ℓ

ω_ℓ * ω_ℓ = ω_ℓ: the idempotence of ω_ℓ as a rewrite rule.

@[simp]

theorem TauCeti.zHat.idem_mul_idem_of_ne (ℓ : ℕ) [Fact (Nat.Prime ℓ)] {ℓ' : ℕ} [Fact (Nat.Prime ℓ')] (h : ℓ ≠ ℓ') : idem ℓ * idem ℓ' = 0

The idempotents of distinct primes are orthogonal.

theorem TauCeti.zHat.component_idem_mul (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (a : Additive ↑zHat.toProfinite.toTop) : (component ℓ) (idem ℓ * a) = (component ℓ) a

Multiplication by ω_ℓ keeps the ℓ-adic component.

theorem TauCeti.zHat.component_idem_mul_of_ne (ℓ : ℕ) [Fact (Nat.Prime ℓ)] {ℓ' : ℕ} [Fact (Nat.Prime ℓ')] (h : ℓ' ≠ ℓ) (a : Additive ↑zHat.toProfinite.toTop) : (component ℓ') (idem ℓ * a) = 0

Multiplication by ω_ℓ kills every other component.

theorem TauCeti.zHat.idem_mul_eq_self_iff (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (a : Additive ↑zHat.toProfinite.toTop) : idem ℓ * a = a ↔ ∀ (ℓ' : ℕ) [inst : Fact (Nat.Prime ℓ')], ℓ' ≠ ℓ → (component ℓ') a = 0

ω_ℓ * a = a exactly when every component of a other than the ℓ-adic one vanishes.

theorem TauCeti.zHat.toZMod_idem_of_dvd_pow (ℓ : ℕ) [Fact (Nat.Prime ℓ)] {n : ℕ+} {k : ℕ} (h : ↑n ∣ ℓ ^ k) : (toZMod n) (idem ℓ) = 1

Reduction of ω_ℓ modulo a power of ℓ. ω_ℓ reduces to 1 modulo every n dividing a power of ℓ, in particular modulo every ℓ ^ k.

theorem TauCeti.zHat.toZMod_idem_of_not_dvd (ℓ : ℕ) [Fact (Nat.Prime ℓ)] {n : ℕ+} (h : ¬ℓ ∣ ↑n) : (toZMod n) (idem ℓ) = 0

Reduction of ω_ℓ modulo a level prime to ℓ. ω_ℓ reduces to 0 modulo every n not divisible by ℓ.

theorem TauCeti.zHat.idem_ne_zero (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : idem ℓ ≠ 0

ω_ℓ is not zero: its ℓ-adic component is 1.

theorem TauCeti.zHat.idem_ne_one (ℓ : ℕ) [Fact (Nat.Prime ℓ)] : idem ℓ ≠ 1

ω_ℓ is not one: its components at the other primes vanish.

theorem TauCeti.zHat.idem_ne_intCast (ℓ : ℕ) [Fact (Nat.Prime ℓ)] (n : ℤ) : idem ℓ ≠ ↑n

The prime idempotent ω_ℓ is unequal to every integer in the profinite integers.

theorem TauCeti.zHat.not_surjective_ofInt : ¬Function.Surjective ⇑ofInt

The integers are a proper subgroup of the profinite integers: the canonical homomorphism ℤ → ℤ̂ is not surjective, since ω_2 is not an integer.

theorem TauCeti.zHat.not_isDomain : ¬IsDomain (Additive ↑zHat.toProfinite.toTop)

The profinite integers are not a domain: ω_2 * (1 - ω_2) = 0 with both factors nonzero.

theorem TauCeti.zHat.tendsto_sum_idem : Filter.Tendsto (fun (s : Finset Nat.Primes) => ∑ p ∈ s, idem ↑p) Filter.atTop (nhds 1)

The finite sums of the prime idempotents tend to 1 as the finite set of primes grows.