Lagrange's theorem for profinite groups

For a closed subgroup H of a profinite group G, the supernatural order of G is the product of the supernatural order of H and its supernatural index in G. The order of H is represented by its finite images in the quotients of G, and finite Lagrange formulas in these quotients relate their orders to the corresponding finite indices. This yields both the primewise additive formula and the multiplicative supernatural-number formula.

Main results

• Subgroup.profiniteOrder_apply_eq_add_profiniteIndex: the primewise profinite Lagrange formula.
• Subgroup.profiniteOrder_eq_mul_profiniteIndex: the supernatural-number form of profinite Lagrange's theorem.

References

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

theorem Subgroup.profiniteOrder_apply_eq_add_profiniteIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) (ℓ : Nat.Primes) : TauCeti.profiniteOrder G ℓ = TauCeti.profiniteOrder (↥H) ℓ + H.profiniteIndex ℓ

Primewise Lagrange formula for a closed subgroup of a profinite group: the exponent in the ambient order is the exponent in the subgroup order plus the exponent in the index.

theorem Subgroup.profiniteOrder_eq_mul_profiniteIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) : TauCeti.profiniteOrder G = TauCeti.profiniteOrder ↥H * H.profiniteIndex

Lagrange's theorem for profinite groups: the supernatural order of the ambient group is the order of a closed subgroup times its supernatural index.