Units of the profinite integers

An element of the profinite integers Additive zHat is a unit exactly when all of its finite reductions are units, equivalently when all of its ℓ-adic components are units. The product decomposition of the profinite integers therefore restricts to a topological group isomorphism between their unit group and the product of the groups ℤ_[ℓ]ˣ.

A compatible family of characters G →* (ZMod n)ˣ consequently assembles uniquely into a character G →* (Additive zHat)ˣ. The assembled character is continuous whenever all of its finite-level characters are continuous.

Main definitions

• TauCeti.zHat.unitsEquivPiPadicInt: the topological group isomorphism (Additive zHat)ˣ ≃ₜ* ∀ ℓ : Nat.Primes, ℤ_[ℓ]ˣ.
• TauCeti.zHat.unitsLift: the character into the profinite units assembled from compatible characters at every finite level.

Main results

• TauCeti.zHat.isUnit_iff_toZMod, TauCeti.zHat.isUnit_iff_component: the finite-level and ℓ-adic unit criteria.
• TauCeti.zHat.map_toZMod_unitsLift, TauCeti.zHat.unitsLift_unique: the characterizing property of the assembled character.
• TauCeti.zHat.continuous_unitsLift: continuity is detected at the finite levels.

References

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

theorem TauCeti.zHat.isUnit_iff_component (a : Additive ↑zHat.toProfinite.toTop) : IsUnit a ↔ ∀ (ℓ : ℕ) (x : Fact (Nat.Prime ℓ)), IsUnit ((component ℓ) a)

A profinite integer is a unit exactly when each of its ℓ-adic components is a unit.

theorem TauCeti.zHat.isUnit_iff_toZMod (a : Additive ↑zHat.toProfinite.toTop) : IsUnit a ↔ ∀ (n : ℕ+), IsUnit ((toZMod n) a)

A profinite integer is a unit exactly when its reduction modulo every positive integer is a unit.

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

The unit-group decomposition of the profinite integers. The product decomposition Additive zHat ≃+* ∀ ℓ, ℤ_[ℓ] restricts to an isomorphism of topological groups on units.

@[simp]

theorem TauCeti.zHat.unitsEquivPiPadicInt_apply (a : (Additive ↑zHat.toProfinite.toTop)ˣ) (ℓ : Nat.Primes) : unitsEquivPiPadicInt a ℓ = (Units.map ↑(component ↑ℓ)) a

The ℓ-adic coordinate of the unit-group decomposition is induced by zHat.component ℓ.

@[simp]

theorem TauCeti.zHat.component_unitsEquivPiPadicInt_symm (a : (ℓ : Nat.Primes) → ℤ_[↑ℓ]ˣ) (ℓ : Nat.Primes) : (component ↑ℓ) ↑(unitsEquivPiPadicInt.symm a) = ↑(a ℓ)

The ℓ-adic component of the inverse unit-group decomposition is the prescribed unit.

noncomputable def TauCeti.zHat.unitsLift {G : Type v} [Monoid G] (χ : (n : ℕ+) → G →* (ZMod ↑n)ˣ) (hχ : ∀ (m n : ℕ+) (h : ↑n ∣ ↑m) (g : G), (ZMod.unitsMap h) ((χ m) g) = (χ n) g) : G →* (Additive ↑zHat.toProfinite.toTop)ˣ

Assembly of compatible finite-level characters. A family of characters χ n : G →* (ZMod n)ˣ compatible with reduction along divisibility assembles into a character G →* (Additive zHat)ˣ, characterized by zHat.map_toZMod_unitsLift.

@[simp]

theorem TauCeti.zHat.toZMod_coe_unitsLift {G : Type v} [Monoid G] (χ : (n : ℕ+) → G →* (ZMod ↑n)ˣ) (hχ : ∀ (m n : ℕ+) (h : ↑n ∣ ↑m) (g : G), (ZMod.unitsMap h) ((χ m) g) = (χ n) g) (n : ℕ+) (g : G) : (toZMod n) ↑((unitsLift χ hχ) g) = ↑((χ n) g)

The underlying profinite integer of the assembled character has the prescribed reduction modulo n.

@[simp]

theorem TauCeti.zHat.map_toZMod_unitsLift {G : Type v} [Monoid G] (χ : (n : ℕ+) → G →* (ZMod ↑n)ˣ) (hχ : ∀ (m n : ℕ+) (h : ↑n ∣ ↑m) (g : G), (ZMod.unitsMap h) ((χ m) g) = (χ n) g) (n : ℕ+) (g : G) : (Units.map ↑(toZMod n)) ((unitsLift χ hχ) g) = (χ n) g

The reduction modulo n of the assembled character is its prescribed level-n character.

theorem TauCeti.zHat.unitsLift_unique {G : Type v} [Monoid G] (χ : (n : ℕ+) → G →* (ZMod ↑n)ˣ) (hχ : ∀ (m n : ℕ+) (h : ↑n ∣ ↑m) (g : G), (ZMod.unitsMap h) ((χ m) g) = (χ n) g) (ψ : G →* (Additive ↑zHat.toProfinite.toTop)ˣ) (hψ : ∀ (n : ℕ+) (g : G), (Units.map ↑(toZMod n)) (ψ g) = (χ n) g) : ψ = unitsLift χ hχ

The compatible finite-level reductions uniquely determine the assembled character.

theorem TauCeti.zHat.continuous_unitsLift {G : Type v} [Monoid G] (χ : (n : ℕ+) → G →* (ZMod ↑n)ˣ) (hχ : ∀ (m n : ℕ+) (h : ↑n ∣ ↑m) (g : G), (ZMod.unitsMap h) ((χ m) g) = (χ n) g) [TopologicalSpace G] (hcont : ∀ (n : ℕ+), Continuous ⇑(χ n)) : Continuous ⇑(unitsLift χ hχ)

The assembled character is continuous whenever all of its finite-level characters are continuous.