This file constructs the canonical map ℤ̂ → ∏ p : Nat.Primes, ℤ_p from the compatible finite reductions.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped Topology
noncomputable section
namespace ClassFormationinstance (p : Nat.Primes) : Fact p.1.PrimeThe product of the additive rings of p-adic integers over all rational primes.
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⟩abbrev ProfiniteIntegerPrimeProductThe ring form of the canonical reduction ℤ̂ → ℤ/nℤ.
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 zHatReductionRingHom (n : ℕ) (hn : 0 < n) :
ZHat →+* ZMod n where
toFun := zHatReduction n hn
map_zero' := rfl
map_one' := rfl
map_add' _ _ := rfl
map_mul' _ _ := rflSurrounding 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 zHatReductionRingHom_apply
(n : ℕ) (hn : 0 < n) (z : ZHat) :
zHatReductionRingHom n hn z = zHatReduction n hn zThe compatible p-power reductions of a profinite integer.
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 zHatPadicReduction (p : Nat.Primes) (n : ℕ) :
ZHat →+* ZMod (p.1 ^ n)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 zHatPadicReduction_compatible
(p : Nat.Primes) (m n : ℕ) (hmn : m ≤ n) :
(ZMod.castHom (pow_dvd_pow p.1 hmn) (ZMod (p.1 ^ m))).comp
(zHatPadicReduction p n) =
zHatPadicReduction p mThe p-adic coordinate of a profinite integer.
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 zHatToPadicInt (p : Nat.Primes) :
ZHat →+* ℤ_[p.1]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 toZModPow_zHatToPadicInt
(p : Nat.Primes) (n : ℕ) :
(PadicInt.toZModPow n).comp (zHatToPadicInt p) =
zHatPadicReduction p nThe canonical ring homomorphism ℤ̂ → ∏ₚ ℤ_p.
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 zHatToProfiniteIntegerPrimeProduct :
ZHat →+* ProfiniteIntegerPrimeProductSurrounding 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 zHatToProfiniteIntegerPrimeProduct_apply
(z : ZHat) (p : Nat.Primes) :
zHatToProfiniteIntegerPrimeProduct z p =
zHatToPadicInt p zThe prime-coordinate map separates profinite integers.
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 zHatToProfiniteIntegerPrimeProduct_injective :
Function.Injective zHatToProfiniteIntegerPrimeProductEach p-adic coordinate map is continuous.
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 continuous_zHatToPadicInt (p : Nat.Primes) :
Continuous (zHatToPadicInt p)The canonical map to the full prime product is continuous.
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 continuous_zHatToProfiniteIntegerPrimeProduct :
Continuous zHatToProfiniteIntegerPrimeProductThe diagonal copy of ℤ is dense in the product of all ℤ_p. This is the topological form of the finite Chinese remainder theorem.
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 denseRange_intCast_profiniteIntegerPrimeProduct :
DenseRange
(Int.castRingHom ProfiniteIntegerPrimeProduct)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 zHatToPadicInt_intCast
(p : Nat.Primes) (a : ℤ) :
zHatToPadicInt p (a : ZHat) = (a : ℤ_[p.1])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 zHatToProfiniteIntegerPrimeProduct_intCast
(a : ℤ) :
zHatToProfiniteIntegerPrimeProduct (a : ZHat) =
Int.castRingHom ProfiniteIntegerPrimeProduct aThe canonical map from the profinite integers to the product of all p-adic integers is onto. Compactness closes its range, while the finite Chinese remainder theorem makes that range dense.
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 zHatToProfiniteIntegerPrimeProduct_surjective :
Function.Surjective zHatToProfiniteIntegerPrimeProductThe Chinese-remainder ring equivalence ℤ̂ ≃ ∏ p : Nat.Primes, ℤ_p.
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 zHatRingEquivProfiniteIntegerPrimeProduct :
ZHat ≃+* ProfiniteIntegerPrimeProductSurrounding 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 zHatRingEquivProfiniteIntegerPrimeProduct_apply
(z : ZHat) :
zHatRingEquivProfiniteIntegerPrimeProduct z =
zHatToProfiniteIntegerPrimeProduct zThe Chinese-remainder ring equivalence is a homeomorphism.
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 isHomeomorph_zHatRingEquivProfiniteIntegerPrimeProduct :
IsHomeomorph zHatRingEquivProfiniteIntegerPrimeProduct