Documentation

TauCeti.Topology.Algebra.Group.Profinite.Procyclic

Closed procyclic subgroups and prime parts #

The closed subgroup generated by an element of a profinite group is precisely its set of profinite powers. Thus it is a quotient of the profinite integers and is abelian. The idempotent of a prime factor of the profinite integers extracts the corresponding prime part of an element: its closed procyclic subgroup is pro-p, and extraction fixes elements whose closed procyclic subgroup is already pro-p. The finite sums of all prime idempotents tend to 1, so the prime parts recover the original element as a limit of finite products.

The power operation is TauCeti.zpowHat, defined using TauCeti.zHat.lift; the prime idempotents and their product decomposition are TauCeti.zHat.idem and TauCeti.zHat.ringEquivPiPadicInt.

References #

source
noncomputable def TauCeti.closedZpowersLift {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) :
↑zHat.toProfinite.toTop →ₜ* ↥(closedZpowers x)

The canonical surjection from the profinite integers onto the closed procyclic subgroup.

Instances For
    source
    @[simp]
    theorem TauCeti.coe_closedZpowersLift {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a : ↑zHat.toProfinite.toTop) :
    ↑((closedZpowersLift x) a) = (zHat.lift x) a

    The canonical surjection is the existing lift, with its codomain restricted.

    source
    theorem TauCeti.closedZpowersLift_surjective {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) :
    Function.Surjective ⇑(closedZpowersLift x)

    Every element of the closed procyclic subgroup is reached by the canonical lift.

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

    The closed procyclic subgroup consists exactly of the profinite powers of its generator.

    source
    theorem TauCeti.mem_closedZpowers_iff {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {x y : G} :
    y ∈ closedZpowers x ↔ ∃ (a : Additive ↑zHat.toProfinite.toTop), zpowHat x a = y

    Membership in the closed procyclic subgroup is existence of a profinite exponent.

    source
    theorem TauCeti.closedZpowers_zpowHat_le {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) (a : Additive ↑zHat.toProfinite.toTop) :
    closedZpowers (zpowHat x a) ≤ closedZpowers x

    A profinite power generates a subgroup of the original closed procyclic subgroup.

    source
    @[simp]
    theorem TauCeti.zpowHat_idem_of_isProP {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} [Fact (Nat.Prime p)] (hG : IsProP p G) (x : G) :
    zpowHat x (zHat.idem p) = x

    Extracting the p-part fixes an element of a pro-p group.

    source
    @[simp]
    theorem TauCeti.zpowHat_idem_of_isProP_closedZpowers {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} [Fact (Nat.Prime p)] {x : G} (hx : IsProP p ↥(closedZpowers x)) :
    zpowHat x (zHat.idem p) = x

    Extracting the p-part fixes any element whose closed procyclic subgroup is pro-p, even when the ambient group is not pro-p.

    source
    theorem TauCeti.zpowHat_idem_mul_of_isProP_closedZpowers {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} [Fact (Nat.Prime p)] {x : G} (hx : IsProP p ↥(closedZpowers x)) (a : Additive ↑zHat.toProfinite.toTop) :
    zpowHat x (zHat.idem p * a) = zpowHat x a

    Only the p-component of a profinite exponent matters when the element's closed procyclic subgroup is pro-p.

    source
    theorem TauCeti.zpowHat_idem_mul_of_isProP {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {p : ℕ} [Fact (Nat.Prime p)] (hG : IsProP p G) (x : G) (a : Additive ↑zHat.toProfinite.toTop) :
    zpowHat x (zHat.idem p * a) = zpowHat x a

    In a pro-p group only the p-component of a profinite exponent matters.

    source
    theorem TauCeti.isProP_closedZpowers_zpowHat_idem {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (p : ℕ) [Fact (Nat.Prime p)] (x : G) :
    IsProP p ↥(closedZpowers (zpowHat x (zHat.idem p)))

    The closed subgroup generated by the p-part of an element is pro-p.

    source
    theorem TauCeti.zpowHat_idem_eq_self_iff {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (p : ℕ) [Fact (Nat.Prime p)] (x : G) :
    zpowHat x (zHat.idem p) = x ↔ IsProP p ↥(closedZpowers x)

    An element is its own p-part exactly when its closed procyclic subgroup is pro-p.

    source
    theorem TauCeti.tendsto_zpowHat_sum_idem {G : Type v} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (x : G) :
    Filter.Tendsto (fun (s : Finset Nat.Primes) => zpowHat x (∑ p ∈ s, zHat.idem ↑p)) Filter.atTop (nhds x)

    Finite collections of prime parts recover the original element in the limit.