Profinite powers

An element x of a profinite group G can be raised to a profinite integer a ∈ ℤ̂: the universal property of ℤ̂ = zHat gives a unique continuous homomorphism zHat.lift x from ℤ̂ to G sending the generator to x, and x ^ᶻ a is its value at a, read multiplicatively (TauCeti.zpowHat). There is no integer representative of a in general, so this power is defined by the universal property and not by a formula.

The power extends the integer powers, and the ring structure of Additive zHat is exactly what makes it a ring of exponents: x ^ᶻ (a + b) = x ^ᶻ a * x ^ᶻ b, and (x ^ᶻ a) ^ᶻ b = x ^ᶻ (a * b) for the ring product. Continuous homomorphisms preserve it, so in particular it commutes with conjugation, and it is jointly continuous in the base and the exponent. On an element of finite order dividing n, the power only sees the residue of the exponent modulo n.

On a pro-ℓ group, Tau Ceti's ℓ-adic power TauCeti.IsProP.padicPow is the same operation seen through the ℓ-adic component of the exponent: x ^ᶻ a is the ℓ-adic power of x by zHat.component ℓ a (TauCeti.zpowHat_eq_padicPow_component).

Main definitions

• TauCeti.zpowHat: the profinite power x ^ᶻ a of an element of a profinite group by a profinite integer, with the notation x ^ᶻ a scoped in TauCeti.zHat.

Main results

• TauCeti.zpowHat_one, TauCeti.zpowHat_intCast, TauCeti.zpowHat_natCast: the power is pinned by x ^ᶻ 1 = x and extends the integer powers.
• TauCeti.zpowHat_add, TauCeti.zpowHat_neg, TauCeti.zpowHat_mul: the exponent laws, the last one for the ring product of Additive zHat.
• TauCeti.map_zpowHat, TauCeti.conj_zpowHat, TauCeti.inv_zpowHat: continuous homomorphisms preserve profinite powers.
• TauCeti.mul_zpowHat, Commute.zpowHat_left, Commute.zpowHat_zpowHat_self: powers of commuting elements.
• TauCeti.continuous_zpowHat, TauCeti.continuous_zpowHat_prod: continuity in the exponent, and joint continuity.
• TauCeti.toMul_zpowHat: on ℤ̂ itself the profinite power is the ring product.
• TauCeti.eq_zpowHat_of_continuous: the profinite power is the unique continuous extension of the integer powers.
• TauCeti.zpowHat_mem: a closed subgroup containing x contains all its profinite powers.
• TauCeti.zpowHat_eq_pow_val_toZMod: on an element killed by n, the profinite power is the natural power by the residue of the exponent modulo n.
• TauCeti.zpowHat_eq_padicPow_component: on a pro-ℓ group the profinite power is the ℓ-adic power by the ℓ-adic component of the exponent.

References

• L. Ribes and P. Zalesskii, Profinite Groups, Section 4.1.

noncomputable def TauCeti.zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a : Additive ↑zHat.toProfinite.toTop) : G

The profinite power x ^ᶻ a of an element x of a profinite group by a profinite integer a: the value at a, read multiplicatively, of the continuous homomorphism zHat.lift x from the profinite integers to G that sends the generator to x.

Equations

• TauCeti.zpowHat x a = (TauCeti.zHat.lift x) (Additive.toMul a)

def TauCeti.zHat.«term_^ᶻ_» : Lean.TrailingParserDescr

The profinite power x ^ᶻ a of an element x of a profinite group by a profinite integer a: the value at a, read multiplicatively, of the continuous homomorphism zHat.lift x from the profinite integers to G that sends the generator to x.

Equations

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

theorem TauCeti.zpowHat_def {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat x a = (zHat.lift x) (Additive.toMul a)

The profinite power by a is the lift of x evaluated at a, read multiplicatively.

@[simp]

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

Raising to the profinite integer 1 is the identity.

@[simp]

theorem TauCeti.zpowHat_zero {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) : zpowHat x 0 = 1

Raising to the profinite integer 0 gives 1.

@[simp]

theorem TauCeti.zpowHat_intCast {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (n : ℤ) : zpowHat x ↑n = x ^ n

The profinite power agrees with the integer power on the integers.

@[simp]

theorem TauCeti.zpowHat_natCast {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (n : ℕ) : zpowHat x ↑n = x ^ n

The profinite power agrees with the natural power on the natural numbers.

@[simp]

theorem TauCeti.zpowHat_ofNat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (n : ℕ) [n.AtLeastTwo] : zpowHat x (OfNat.ofNat n) = x ^ OfNat.ofNat n

The profinite power by a numeral is the corresponding natural power.

@[simp]

theorem TauCeti.one_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (a : Additive ↑zHat.toProfinite.toTop) : zpowHat 1 a = 1

Every profinite power of 1 is 1.

@[simp]

theorem TauCeti.zpowHat_add {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a b : Additive ↑zHat.toProfinite.toTop) : zpowHat x (a + b) = zpowHat x a * zpowHat x b

The additive law.

@[simp]

theorem TauCeti.zpowHat_neg {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat x (-a) = (zpowHat x a)⁻¹

Raising to -a inverts the power by a.

theorem TauCeti.zpowHat_sub {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a b : Additive ↑zHat.toProfinite.toTop) : zpowHat x (a - b) = zpowHat x a * (zpowHat x b)⁻¹

Raising to a - b is the power by a times the inverse of the power by b.

@[simp]

theorem TauCeti.zpowHat_mul {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a b : Additive ↑zHat.toProfinite.toTop) : zpowHat x (a * b) = zpowHat (zpowHat x a) b

The multiplicative law, for the ring product of the profinite integers: raising to a and then to b is raising to a * b.

theorem TauCeti.toMul_zpowHat (b a : Additive ↑zHat.toProfinite.toTop) : zpowHat (Additive.toMul b) a = Additive.toMul (b * a)

On the profinite integers themselves, the profinite power is the ring product: toMul b ^ᶻ a is b * a, read multiplicatively.

@[simp]

theorem TauCeti.map_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {H : Type w} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [CompactSpace H] [TotallyDisconnectedSpace H] {F : Type u_1} [FunLike F G H] [MonoidHomClass F G H] [ContinuousMapClass F G H] (f : F) (x : G) (a : Additive ↑zHat.toProfinite.toTop) : f (zpowHat x a) = zpowHat (f x) a

Naturality. A continuous homomorphism of profinite groups preserves profinite powers.

@[simp]

theorem TauCeti.smul_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {Γ : Type u_1} [Monoid Γ] [MulDistribMulAction Γ G] [ContinuousConstSMul Γ G] (γ : Γ) (x : G) (a : Additive ↑zHat.toProfinite.toTop) : γ • zpowHat x a = zpowHat (γ • x) a

A continuous action by group endomorphisms commutes with profinite powers.

@[simp]

theorem TauCeti.conj_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (g x : G) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat (g * x * g⁻¹) a = g * zpowHat x a * g⁻¹

Profinite powers commute with conjugation.

@[simp]

theorem TauCeti.conj_inv_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (c x : G) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat (c⁻¹ * x * c) a = c⁻¹ * zpowHat x a * c

Profinite powers commute with conjugation by an inverse.

@[simp]

theorem TauCeti.inv_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat x⁻¹ a = (zpowHat x a)⁻¹

The profinite power of an inverse is the inverse of the profinite power.

@[simp]

theorem TauCeti.mul_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x y : G} (h : Commute x y) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat (x * y) a = zpowHat x a * zpowHat y a

The profinite power is multiplicative on commuting base elements.

theorem Commute.zpowHat_left {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x y : G} (h : Commute x y) (a : Additive ↑TauCeti.zHat.toProfinite.toTop) : Commute (TauCeti.zpowHat x a) y

A profinite power of an element commuting with y commutes with y.

theorem Commute.zpowHat_right {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x y : G} (h : Commute x y) (a : Additive ↑TauCeti.zHat.toProfinite.toTop) : Commute x (TauCeti.zpowHat y a)

An element commuting with y commutes with every profinite power of y.

theorem Commute.zpowHat_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x y : G} (h : Commute x y) (a b : Additive ↑TauCeti.zHat.toProfinite.toTop) : Commute (TauCeti.zpowHat x a) (TauCeti.zpowHat y b)

Profinite powers of commuting elements commute.

theorem Commute.zpowHat_zpowHat_self {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a b : Additive ↑TauCeti.zHat.toProfinite.toTop) : Commute (TauCeti.zpowHat x a) (TauCeti.zpowHat x b)

Two profinite powers of the same element commute.

theorem TauCeti.zpowHat_comm {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a b : Additive ↑zHat.toProfinite.toTop) : zpowHat x a * zpowHat x b = zpowHat x b * zpowHat x a

Two profinite powers of the same element commute under multiplication.

theorem TauCeti.continuous_zpowHat {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) : Continuous fun (a : Additive ↑zHat.toProfinite.toTop) => zpowHat x a

The profinite powers of x depend continuously on the exponent.

theorem TauCeti.continuous_zpowHat_prod {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] : Continuous fun (q : G × Additive ↑zHat.toProfinite.toTop) => zpowHat q.1 q.2

Joint continuity. The profinite power (x, a) ↦ x ^ᶻ a is continuous on G × ℤ̂.

theorem TauCeti.zpowHat_mem {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {K : Subgroup G} (hK : IsClosed ↑K) {x : G} (hx : x ∈ K) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat x a ∈ K

A closed subgroup containing x contains every profinite power of x.

theorem TauCeti.eq_zpowHat_of_continuous {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x : G} {f : Additive ↑zHat.toProfinite.toTop → G} (hf : Continuous f) (hint : ∀ (n : ℤ), f ↑n = x ^ n) (a : Additive ↑zHat.toProfinite.toTop) : f a = zpowHat x a

Uniqueness. The profinite power is the unique continuous extension of the integer powers of x along the dense inclusion of ℤ in ℤ̂.

theorem TauCeti.zpowHat_eq_pow_val_toZMod {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x : G} {n : ℕ+} (hx : x ^ ↑n = 1) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat x a = x ^ ((zHat.toZMod n) a).val

Powers of an element of finite order. If x ^ n = 1, the profinite power x ^ᶻ a is the natural power of x by the residue of a modulo n.

theorem TauCeti.zpowHat_eq_pow_val_toZMod_natCard {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] [Finite G] (x : G) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat x a = x ^ ((zHat.toZMod ⟨Nat.card G, ⋯⟩) a).val

In a finite group, the profinite power depends only on the exponent modulo the group order.

theorem TauCeti.zpowHat_eq_padicPow_component {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {ℓ : ℕ} [Fact (Nat.Prime ℓ)] (hG : IsProP ℓ G) (x : G) (a : Additive ↑zHat.toProfinite.toTop) : zpowHat x a = hG.padicPow x ((zHat.component ℓ) a)

The ℓ-adic comparison. On a pro-ℓ group, the profinite power by a is Tau Ceti's ℓ-adic power by the ℓ-adic component of a.