This file upgrades the prime-product Chinese-remainder equivalence for ℤ̂ to topological additive, multiplicative, and unit-group equivalences.
The Chinese-remainder isomorphism as a topological monoid equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormationdef zHatContinuousMulEquivPrimeProduct :
ZHat ≃ₜ* ProfiniteIntegerPrimeProductThe additive form of the topological Chinese-remainder isomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormationdef zHatContinuousAddEquivPrimeProduct :
ZHat ≃ₜ+ ProfiniteIntegerPrimeProductSurrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormationinstance (p : Nat.Primes) : Fact p.1.PrimeThe canonical topological Chinese-remainder equivalence on unit groups.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩def zHatUnitsContinuousMulEquivPrimeProduct :
ZHatˣ ≃ₜ* ((p : Nat.Primes) → ℤ_[p.1]ˣ)On underlying ring elements, the unit-group Chinese-remainder equivalence is the canonical p-adic coordinate map.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormation
local instance (p : Nat.Primes) : Fact p.1.Prime :=
⟨p.2⟩theorem zHatUnitsContinuousMulEquivPrimeProduct_coe_apply
(u : ZHatˣ) (p : Nat.Primes) :
(zHatUnitsContinuousMulEquivPrimeProduct u p : ℤ_[p.1]) =
zHatToPadicInt p (u : ZHat)