The profinite group ℤ₂ as an inverse limit (Stage C, work order C1)

ProfiniteZ2 is the profinite group of 2-adic integers, realised as the inverse limit, in the category ProfiniteGrp, of the finite cyclic groups ZMod (2 ^ n) along the reduction maps ZMod (2 ^ m) → ZMod (2 ^ n) (n ≤ m).

Because ProfiniteGrp is a category of multiplicative groups we carry the layers as Multiplicative (ZMod (2 ^ n)) (C2Pow n); additively this is ℤ / 2ⁿℤ, so the 2-adic integers 0, 1, -2 appear here as z2Zero, z2One, z2NegTwo (with z2Zero = 1, the multiplicative identity).

This is a self-contained boundary building block, independent of the Q₂ word and of Stages A/B. It supplies:

• ProfiniteZ2 : ProfiniteGrp — the inverse limit;
• C2Pow n and z2Projection n : ProfiniteZ2 ⟶ ProfiniteGrp.of (C2Pow n);
• ProfiniteZ2_ext — two points agree once all projections agree;
• the marked elements z2Zero, z2One, z2NegTwo.

@[reducible, inline]

abbrev Q2Presentation.C2Pow (n : ℕ) : Type

The n-th finite layer ZMod (2 ^ n) of ℤ₂, written multiplicatively so that it is (a carrier of) an object of ProfiniteGrp.

Equations

• Q2Presentation.C2Pow n = Multiplicative (ZMod (2 ^ n))

instance Q2Presentation.instFiniteC2Pow (n : ℕ) : Finite (C2Pow n)

instance Q2Presentation.instTopologicalSpaceC2Pow (n : ℕ) : TopologicalSpace (C2Pow n)

Equations

• Q2Presentation.instTopologicalSpaceC2Pow n = ⊥

instance Q2Presentation.instDiscreteTopologyC2Pow (n : ℕ) : DiscreteTopology (C2Pow n)

def Q2Presentation.castCMH {a b : ℕ} (h : 2 ^ a ∣ 2 ^ b) : C2Pow b →ₜ* C2Pow a

The reduction homomorphism C2Pow b → C2Pow a attached to a divisibility 2 ^ a ∣ 2 ^ b (i.e. a ≤ b), as a continuous monoid hom; it is the multiplicative repackaging of ZMod.castHom.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Q2Presentation.castCMH_apply {a b : ℕ} (h : 2 ^ a ∣ 2 ^ b) (x : C2Pow b) : (castCMH h) x = Multiplicative.ofAdd ((ZMod.castHom h (ZMod (2 ^ a))) (Multiplicative.toAdd x))

theorem Q2Presentation.castCMH_id {n : ℕ} (h : 2 ^ n ∣ 2 ^ n) : castCMH h = ContinuousMonoidHom.id (C2Pow n)

A reduction map indexed by a reflexive divisibility is the identity.

theorem Q2Presentation.castCMH_comp {x y z : ℕ} (hg : 2 ^ z ∣ 2 ^ y) (hf : 2 ^ y ∣ 2 ^ x) : (castCMH hg).comp (castCMH hf) = castCMH ⋯

Reduction maps compose: reducing through an intermediate layer agrees with the direct reduction (using that ring homs out of ZMod are unique).

def Q2Presentation.C2System : CategoryTheory.Functor ℕᵒᵖ ProfiniteGrp.{0}

The inverse system n ↦ C2Pow n of finite 2-power layers and reduction maps, as a functor ℕᵒᵖ ⥤ ProfiniteGrp.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Q2Presentation.C2System_obj (X : ℕᵒᵖ) : C2System.obj X = ProfiniteGrp.of (C2Pow (Opposite.unop X))

@[simp]

theorem Q2Presentation.C2System_map_apply {X Y : ℕᵒᵖ} (π : X ⟶ Y) (x : C2Pow (Opposite.unop X)) : (ProfiniteGrp.Hom.hom (C2System.map π)) x = Multiplicative.ofAdd ((ZMod.castHom ⋯ (ZMod (2 ^ Opposite.unop Y))) (Multiplicative.toAdd x))

@[reducible, inline]

abbrev Q2Presentation.ProfiniteZ2 : ProfiniteGrp.{0}

The profinite group ℤ₂, the inverse limit of the layers C2Pow n.

Equations

• Q2Presentation.ProfiniteZ2 = ProfiniteGrp.limit Q2Presentation.C2System

def Q2Presentation.z2Projection (n : ℕ) : ProfiniteZ2 ⟶ ProfiniteGrp.of (C2Pow n)

The canonical projection ℤ₂ → ZMod (2 ^ n) onto the n-th layer.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Q2Presentation.z2Projection_apply (n : ℕ) (x : ↑ProfiniteZ2.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (z2Projection n)) x = ↑x (Opposite.op n)

theorem Q2Presentation.ProfiniteZ2_ext {x y : ↑ProfiniteZ2.toProfinite.toTop} (h : ∀ (n : ℕ), (ProfiniteGrp.Hom.hom (z2Projection n)) x = (ProfiniteGrp.Hom.hom (z2Projection n)) y) : x = y

Two 2-adic integers coincide once all of their finite reductions do.

def Q2Presentation.z2OfInt (k : ℤ) : ↑ProfiniteZ2.toProfinite.toTop

The 2-adic integer represented by an ordinary integer k, as the compatible family of its reductions mod 2 ^ n.

Equations

• Q2Presentation.z2OfInt k = ⟨fun (j : ℕᵒᵖ) => Multiplicative.ofAdd ↑k, ⋯⟩

def Q2Presentation.z2Zero : ↑ProfiniteZ2.toProfinite.toTop

The 2-adic integer 0 (which is the multiplicative identity of ℤ₂).

Equations

• Q2Presentation.z2Zero = Q2Presentation.z2OfInt 0

def Q2Presentation.z2One : ↑ProfiniteZ2.toProfinite.toTop

The 2-adic integer 1.

Equations

• Q2Presentation.z2One = Q2Presentation.z2OfInt 1

def Q2Presentation.z2NegTwo : ↑ProfiniteZ2.toProfinite.toTop

The 2-adic integer -2, used in the marked Demushkin statements.

Equations

• Q2Presentation.z2NegTwo = Q2Presentation.z2OfInt (-2)

@[simp]

theorem Q2Presentation.z2Projection_z2OfInt (k : ℤ) (n : ℕ) : (ProfiniteGrp.Hom.hom (z2Projection n)) (z2OfInt k) = Multiplicative.ofAdd ↑k

@[simp]

theorem Q2Presentation.z2Projection_z2Zero (n : ℕ) : (ProfiniteGrp.Hom.hom (z2Projection n)) z2Zero = Multiplicative.ofAdd 0

The 2-adic integer 0 is, as expected, the n-th reduction 0 for every n (z2Zero reduces to 0 ∈ ZMod (2 ^ n) at every layer).