We construct ℤ̂ as the topological closure of the diagonal image of ℤ inside the product of all positive cyclic quotients ZMod n. This realizes the canonical reduction maps and the dense integer embedding directly in Mathlib.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologystructure ZHatIndex where
modulus : ℕ
positive : 0 < modulusSurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyinstance (i : ZHatIndex) : NeZero i.modulusSurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologydef zHatIndex (n : ℕ) (hn : 0 < n) : ZHatIndexSurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyabbrev ZHatAmbient : Type 0Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologydef zHatDiagonal : ℤ →+* ZHatAmbient where
toFun a i := (a : ZMod i.modulus)
map_zero' := by
funext i
exact Int.cast_zero
map_one' := by
funext i
exact Int.cast_one
map_add' a b := by
funext i
exact Int.cast_add a b
map_mul' a b := by
funext i
exact Int.cast_mul a bSurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologydef zHatIntegerSubring : Subring ZHatAmbientSurrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyabbrev ZHatClosureModel : Type 0The profinite completion ℤ̂ = lim ℤ/nℤ over all positive moduli.
This is deliberately a def, rather than an abbrev: clients use the reduction maps and the representation equivalence below instead of depending on the closure subtype.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologydef ZHat : Type 0The closure model equips ZHat with its canonical commutative ring structure.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyinstance : CommRing ZHatThe closure model equips ZHat with its subspace topology.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyinstance : TopologicalSpace ZHatRing operations on ZHat are continuous for the closure-model topology.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyinstance : IsTopologicalRing ZHatThe closure-model topology on ZHat is Hausdorff.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyinstance : T2Space ZHatThe profinite integer model is totally disconnected.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyinstance : TotallyDisconnectedSpace ZHatThe profinite integer closure model is compact.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyinstance : CompactSpace ZHatZHat as Mathlib's bundled profinite additive group.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologydef zHatProfiniteAddGrp : ProfiniteAddGrpThe multiplicative presentation of ZHat remains totally disconnected.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologyinstance : TotallyDisconnectedSpace (Multiplicative ZHat)The multiplicative presentation of ZHat as Mathlib's bundled profinite group. Its multiplication is addition in ZHat.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologydef zHatMulProfiniteGrp : ProfiniteGrpThe canonical continuous reduction ℤ̂ → ℤ/nℤ.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologydef zHatReduction (n : ℕ) (hn : 0 < n) :
ContinuousAddMonoidHom ZHat (ZMod n) where
toFun x := (show ZHatClosureModel from x).1 (zHatIndex n hn)
map_zero' := rfl
map_add' _ _ := rfl
continuous_toFun := by
change Continuous
(fun x : ZHatClosureModel => x.1 (zHatIndex n hn))
exact (continuous_apply (zHatIndex n hn)).comp continuous_subtype_valReduction agrees with the ordinary integer cast. This is the public computation rule; it does not expose the closure model used to construct ZHat.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologytheorem zHatReduction_intCast (n : ℕ) (hn : 0 < n) (a : ℤ) :
zHatReduction n hn (a : ZHat) = (a : ZMod n)Reduction modulo one sends every profinite integer to the unique residue class.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologytheorem zHatReduction_one (n : ℕ) (hn : 0 < n) :
zHatReduction n hn (1 : ZHat) = 1Profinite integers are determined by all positive-modulus reductions.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topology
namespace ZHattheorem ext {x y : ZHat}
(h : ∀ n (hn : 0 < n), zHatReduction n hn x = zHatReduction n hn y) :
x = yReduction maps commute with reduction along a divisibility relation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologytheorem zHatReduction_transition {m n : ℕ}
(hm : 0 < m) (hn : 0 < n) (hmn : m ∣ n) (x : ZHat) :
ZMod.castHom hmn (ZMod m) (zHatReduction n hn x) =
zHatReduction m hm xThe ordinary integers have dense image in their profinite completion.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologytheorem denseRange_intCast_zHat :
DenseRange (Int.castRingHom ZHat)The element 1 topologically generates the additive profinite integers, written multiplicatively.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace ClassFormation
open scoped Topologytheorem zHatOne_topologicallyGenerates :
TopologicallyGenerates
(G := Multiplicative ZHat)
({Multiplicative.ofAdd (1 : ZHat)} : Set (Multiplicative ZHat))