The supernatural order of a profinite group

The order of a profinite group is the least common multiple, in the supernatural-number lattice, of the orders of all its continuous finite quotients. We define it primewise using the quotients by open normal subgroups and identify it with the supremum of their finite supernatural orders.

For a finite group with the discrete topology, the trivial subgroup occurs among the open normal subgroups. Its quotient is the whole group, while every other quotient has order dividing the group order. Consequently the supernatural order recovers the ordinary finite order exactly.

Main results

• profiniteOrder: the supernatural order, defined from the Nat.card of quotients by open normal subgroups.
• profiniteOrder_eq_iSup_ofNat: its description as the supremum of the embedded quotient orders.
• profiniteOrder_eq_bot_iff: a profinite group has order ⊥ = 1 exactly when it is trivial.
• profiniteOrder_apply_eq_top_iff: a prime has infinite exponent exactly when its powers divide the orders of finite continuous quotients without bound.
• Subgroup.profiniteOrder_eq_iSup_image: a closed subgroup's order as the supremum of its images in the ambient finite quotients.
• Subgroup.profiniteOrder_apply_eq_iSup_image: the primewise form of this description.
• profiniteOrder_le_of_surjective: continuous surjections do not increase supernatural order.
• profiniteOrder_congr: topological group isomorphisms preserve supernatural order.
• profiniteOrder_eq_of_finite: agreement with Nat.card for a finite discrete group.

References

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

noncomputable def TauCeti.profiniteOrder (G : Type u) [Group G] [TopologicalSpace G] : Supernatural

The supernatural number whose exponent at a prime is the supremum of the corresponding valuations of the Nat.card of all quotients by open normal subgroups. For a profinite group, this is its order.

Equations

• TauCeti.profiniteOrder G = TauCeti.Supernatural.ofFun fun (p : Nat.Primes) => ⨆ (U : OpenNormalSubgroup G), ↑(padicValNat (↑p) (Nat.card (G ⧸ ↑U.toOpenSubgroup)))

@[simp]

theorem TauCeti.profiniteOrder_apply (G : Type u) [Group G] [TopologicalSpace G] (p : Nat.Primes) : profiniteOrder G p = ⨆ (U : OpenNormalSubgroup G), ↑(padicValNat (↑p) (Nat.card (G ⧸ ↑U.toOpenSubgroup)))

The exponent of a prime in profiniteOrder is the supremum of the valuations of the Nat.card of the quotients by open normal subgroups.

theorem TauCeti.profiniteOrder_le_of_surjective {G : Type u} {H : Type v} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (f : G →* H) (hf : Continuous ⇑f) (hsurj : Function.Surjective ⇑f) : profiniteOrder H ≤ profiniteOrder G

A continuous surjective homomorphism cannot increase profiniteOrder.

theorem TauCeti.profiniteOrder_congr {G : Type u} {H : Type v} [Group G] [TopologicalSpace G] [Group H] [TopologicalSpace H] (e : G ≃ₜ* H) : profiniteOrder G = profiniteOrder H

Topologically isomorphic groups have the same supernatural order.

theorem TauCeti.profiniteOrder_quotient_le {G : Type u} [Group G] [TopologicalSpace G] (N : Subgroup G) [N.Normal] : profiniteOrder (G ⧸ N) ≤ profiniteOrder G

Passing to a quotient cannot increase profiniteOrder.

theorem TauCeti.profiniteOrder_eq_iSup_ofNat (G : Type u) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] : profiniteOrder G = ⨆ (U : OpenNormalSubgroup G), Supernatural.ofNat ⟨Nat.card (G ⧸ ↑U.toOpenSubgroup), ⋯⟩

The supernatural order is the supremum of the ordinary orders of the finite continuous quotients, embedded into the supernatural numbers.

@[simp]

theorem TauCeti.profiniteOrder_le_iff (G : Type u) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] {n : Supernatural} : profiniteOrder G ≤ n ↔ ∀ (U : OpenNormalSubgroup G), Supernatural.ofNat ⟨Nat.card (G ⧸ ↑U.toOpenSubgroup), ⋯⟩ ≤ n

The supernatural order is bounded by n exactly when the order of every finite continuous quotient is bounded by n.

theorem TauCeti.ofNat_card_quotient_le_profiniteOrder (G : Type u) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] (U : OpenNormalSubgroup G) : Supernatural.ofNat ⟨Nat.card (G ⧸ ↑U.toOpenSubgroup), ⋯⟩ ≤ profiniteOrder G

The ordinary order of each finite continuous quotient divides profiniteOrder G.

@[simp]

theorem TauCeti.profiniteOrder_eq_bot_iff (G : Type u) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] [IsTopologicalGroup G] [TotallyDisconnectedSpace G] : profiniteOrder G = ⊥ ↔ Subsingleton G

A profinite group has supernatural order ⊥ = 1 exactly when it is trivial.

theorem TauCeti.profiniteOrder_apply_eq_top_iff (G : Type u) [Group G] [TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G] (p : Nat.Primes) : profiniteOrder G p = ⊤ ↔ ∀ (n : ℕ), ∃ (U : OpenNormalSubgroup G), ↑p ^ n ∣ Nat.card (G ⧸ ↑U.toOpenSubgroup)

The exponent of a prime p in profiniteOrder G is infinite exactly when every power of p divides the order of some finite continuous quotient.

theorem Subgroup.profiniteOrder_eq_iSup_image {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) : TauCeti.profiniteOrder ↥H = ⨆ (N : OpenNormalSubgroup G), TauCeti.Supernatural.ofNat ⟨Nat.card ↥(map (QuotientGroup.mk' ↑N.toOpenSubgroup) H), ⋯⟩

The supernatural order of a closed subgroup is the supremum of the orders of its images in the ambient finite continuous quotients.

theorem Subgroup.profiniteOrder_apply_eq_iSup_image {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) (ℓ : Nat.Primes) : TauCeti.profiniteOrder (↥H) ℓ = ⨆ (N : OpenNormalSubgroup G), ↑(padicValNat (↑ℓ) (Nat.card ↥(map (QuotientGroup.mk' ↑N.toOpenSubgroup) H)))

Primewise form of Subgroup.profiniteOrder_eq_iSup_image.

@[simp]

theorem TauCeti.profiniteOrder_eq_of_finite (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] : profiniteOrder G = Supernatural.ofNat ⟨Nat.card G, ⋯⟩

On a finite group with the discrete topology, supernatural order is the prime factorization of the ordinary group order.

@[simp]

theorem TauCeti.profiniteOrder_apply_of_finite (G : Type u) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (p : Nat.Primes) : profiniteOrder G p = ↑(padicValNat (↑p) (Nat.card G))

Pointwise form of profiniteOrder_eq_of_finite. Its simp priority is above that of profiniteOrder_apply, so that a finite discrete group simplifies to the valuation of its order rather than to the defining supremum.