ℤ̂ and ẑ-exponentiation: the profinite home of ω₂

The paper's presentation Γ_A uses words with profinite exponents: τ^{ω₂}, x₀^{ω₂} for the idempotent ω₂ ∈ ℤ̂ (≡ 1 on the pro-2 part, ≡ 0 on the odd part). This file provides that machinery on top of Mathlib's ProfiniteGrp.ProfiniteCompletion:

• GQ2.Zhat — ℤ̂, the profinite completion of ℤ (as Multiplicative ℤ; the group law of Zhat is addition of exponents).
• GQ2.Zhat.ofInt — the canonical dense embedding ℤ → ℤ̂ (Zhat.denseRange_ofInt).
• GQ2.zpowHat (notation x ^ᶻ γ) — for x in any profinite group, the continuous extension of n ↦ xⁿ to exponents γ : ℤ̂, via the universal property of the completion. Naturality: map_zpowHat.
• GQ2.omega2 — ω₂ ∈ ℤ̂, constructed componentwise as the compatible family (omega2Exp N)_N (compatibility = GQ2.omega2Exp_modEq).
• Headline (zpowHat_omega2, map_zpowHat_omega2): through every finite quotient, the profinite ω₂-power computes the finite ω₂-calculus of Appendices A/B: f (x ^ᶻ ω₂) = powOmega2 (f x).

Only the group structure of ℤ̂ is provided; the ring structure (e.g. ω₂ · ω₂ = ω₂) is out of scope until something needs it.

Finite-index subgroups of ℤ

Everything about ℤ̂ = lim ℤ/H reduces to: classes in ℤ/H are integers mod the index of H. The two lemmas here make that precise without classifying the subgroups of ℤ: in the quotient, the generator 1 has order exactly [ℤ : H].

theorem GQ2.orderOf_mk_ofAdd_one (H : Subgroup (Multiplicative ℤ)) : orderOf ↑(Multiplicative.ofAdd 1) = H.index

In the quotient of Multiplicative ℤ by any subgroup, the class of the generator ofAdd 1 has order exactly the index (0 if the index is infinite).

theorem GQ2.ofAdd_mem_iff_index_dvd {H : Subgroup (Multiplicative ℤ)} {a : ℤ} : Multiplicative.ofAdd a ∈ H ↔ ↑H.index ∣ a

Membership in a subgroup of Multiplicative ℤ is divisibility by its index.

theorem GQ2.mk_ofAdd_eq_mk_ofAdd_iff {H : Subgroup (Multiplicative ℤ)} {a b : ℤ} : ↑(Multiplicative.ofAdd a) = ↑(Multiplicative.ofAdd b) ↔ ↑H.index ∣ b - a

Classes of integers in ℤ/H are congruence classes mod the index: [a] = [b] ↔ [ℤ : H] ∣ b - a.

A neighborhood-basis property of profinite completions

theorem GQ2.completion_exists_level {G : GrpCat} {γ : ↑(ProfiniteGrp.ProfiniteCompletion.completion G).toProfinite.toTop} {U : Set ↑(ProfiniteGrp.ProfiniteCompletion.completion G).toProfinite.toTop} (hU : IsOpen U) (hγ : γ ∈ U) : ∃ (H₀ : FiniteIndexNormalSubgroup ↑G), ∀ (δ : ↑(ProfiniteGrp.ProfiniteCompletion.completion G).toProfinite.toTop), ↑δ H₀ = ↑γ H₀ → δ ∈ U

Congruence neighborhoods are a basis: if U ∋ γ is open in the profinite completion of G, there is a single finite-index level H₀ such that every element agreeing with γ in G ⧸ H₀ already lies in U. (Same cofinality argument as ProfiniteCompletion.denseRange.)

ℤ̂

def GQ2.Zhat : ProfiniteGrp.{0}

ℤ̂ — the profinite completion of the integers, i.e. lim_N ℤ/N over all finite-index subgroups. The paper's profinite exponents (most importantly ω₂, cf. GQ2.omega2) live here.

Convention: Zhat is a completion of the multiplicative group Multiplicative ℤ, so the group operation of Zhat corresponds to addition of exponents: x ^ᶻ (γ * δ) = x ^ᶻ γ * x ^ᶻ δ. Only the group structure is provided (no ring structure yet).

Equations

• GQ2.Zhat = ProfiniteGrp.ProfiniteCompletion.completion (GrpCat.of (Multiplicative ℤ))

def GQ2.Zhat.ofInt (n : ℤ) : ↑Zhat.toProfinite.toTop

The canonical dense embedding ℤ → ℤ̂ (written multiplicatively: ofInt (a + b) = ofInt a * ofInt b).

Equations

• GQ2.Zhat.ofInt n = ProfiniteGrp.ProfiniteCompletion.etaFn (GrpCat.of (Multiplicative ℤ)) (Multiplicative.ofAdd n)

@[simp]

theorem GQ2.Zhat.ofInt_add (a b : ℤ) : ofInt (a + b) = ofInt a * ofInt b

@[simp]

theorem GQ2.Zhat.ofInt_zero : ofInt 0 = 1

theorem GQ2.Zhat.denseRange_ofInt : DenseRange ofInt

ℤ is dense in ℤ̂.

theorem GQ2.Zhat.funext_ofInt {X : Type u_1} [TopologicalSpace X] [T2Space X] {f g : ↑Zhat.toProfinite.toTop → X} (hf : Continuous f) (hg : Continuous g) (h : ∀ (n : ℤ), f (ofInt n) = g (ofInt n)) : f = g

Two continuous maps out of ℤ̂ agreeing on ℤ agree everywhere.

ω₂ as an element of ℤ̂

noncomputable def GQ2.omega2 : ↑Zhat.toProfinite.toTop

The profinite idempotent ω₂ ∈ ℤ̂ (paper §1 and App. A/B): the unique element of ℤ̂ = lim_N ℤ/N that is ≡ 1 on the pro-2 part and ≡ 0 on the odd part. Constructed componentwise: at a finite-index subgroup H ≤ ℤ the component is the integer representative omega2Exp [ℤ:H] (at the Appendix-B modulus 85667662080 this is the paper's serialized value 40491355905, cf. omega2Exp_appendixB_value); compatibility of the family is exactly omega2Exp_modEq.

Equations

• GQ2.omega2 = ⟨fun (H : FiniteIndexNormalSubgroup ↑(GrpCat.of (Multiplicative ℤ))) => ↑(Multiplicative.ofAdd ↑(GQ2.omega2Exp H.index)), ⋯⟩

ẑ-exponentiation

noncomputable def GQ2.zpowHatHom {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) : Zhat ⟶ ProfiniteGrp.of G

The ẑ-power morphism: for x in a profinite group G, the unique continuous extension of n ↦ xⁿ to a morphism ℤ̂ ⟶ G, via the universal property of the profinite completion.

Equations

• GQ2.zpowHatHom x = ProfiniteGrp.ProfiniteCompletion.lift (GrpCat.ofHom ((zpowersHom G) x))

noncomputable def GQ2.zpowHat {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (γ : ↑Zhat.toProfinite.toTop) : G

x ^ᶻ γ: the γ-th power of x : G for a profinite exponent γ : ℤ̂ (G profinite). Extends ordinary powers (zpowHat_ofInt : x ^ᶻ ofInt n = x ^ n) continuously; the paper's words τ^{ω₂}, x₀^{ω₂} are instances (with γ = GQ2.omega2).

Equations

• GQ2.zpowHat x γ = (ProfiniteGrp.Hom.hom (GQ2.zpowHatHom x)) γ

def GQ2.«term_^ᶻ_» : Lean.TrailingParserDescr

x ^ᶻ γ: the γ-th power of x : G for a profinite exponent γ : ℤ̂ (G profinite). Extends ordinary powers (zpowHat_ofInt : x ^ᶻ ofInt n = x ^ n) continuously; the paper's words τ^{ω₂}, x₀^{ω₂} are instances (with γ = GQ2.omega2).

Equations

• GQ2.«term_^ᶻ_» = Lean.ParserDescr.trailingNode `GQ2.«term_^ᶻ_» 75 76 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^ᶻ ") (Lean.ParserDescr.cat `term 75))

theorem GQ2.continuous_zpowHat {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) : Continuous fun (x_1 : ↑Zhat.toProfinite.toTop) => zpowHat x x_1

@[simp]

theorem GQ2.zpowHat_ofInt {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (n : ℤ) : zpowHat x (Zhat.ofInt n) = x ^ n

ẑ-exponentiation extends ordinary (ℤ-)powers.

@[simp]

theorem GQ2.zpowHat_mul {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (γ δ : ↑Zhat.toProfinite.toTop) : zpowHat x (γ * δ) = zpowHat x γ * zpowHat x δ

The exponent group law: Zhat-multiplication is addition of exponents.

@[simp]

theorem GQ2.zpowHat_one {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) : zpowHat x 1 = 1

theorem GQ2.map_zpowHat {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] (f : G →ₜ* H) (x : G) (γ : ↑Zhat.toProfinite.toTop) : f (zpowHat x γ) = zpowHat (f x) γ

Naturality of ẑ-exponentiation: continuous homomorphisms of profinite groups commute with ^ᶻ. Both sides are continuous extensions of n ↦ f x ^ n, so this is uniqueness of the lift through the completion (ProfiniteCompletion.lift_unique).

Evaluation of ω₂ through finite quotients

theorem GQ2.zpowHat_omega2 {P : Type} [Group P] [TopologicalSpace P] [DiscreteTopology P] [Finite P] (x : P) : zpowHat x omega2 = powOmega2 x

ω₂ acts on finite groups as the 2-primary projection: in a finite (discrete) group, x ^ᶻ ω₂ = powOmega2 x = x ^ omega2Exp (orderOf x). This ties the profinite element omega2 to the entire finite ω₂-calculus of Appendices A/B (GQ2.powOmega2, GQ2.markOmega2, the word ledger of GQ2/Words.lean).

theorem GQ2.map_zpowHat_omega2 {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {P : Type} [Group P] [TopologicalSpace P] [DiscreteTopology P] [Finite P] (f : G →ₜ* P) (x : G) : f (zpowHat x omega2) = powOmega2 (f x)

Headline lemma of the profinite-exponentiation API: for any continuous homomorphism f from a profinite group to a finite (discrete) group, f (x ^ᶻ ω₂) = powOmega2 (f x) — the profinite ω₂ and the paper's finite ω₂-calculus compute the same thing through every finite quotient. In particular the Γ_A-relator words, once written with ^ᶻ omega2, evaluate in finite markings to exactly the words of GQ2/Words.lean.