Profinite index in a subgroup tower

This file proves multiplicativity of supernatural index in a tower H ≤ K ≤ G, where K is a closed subgroup of a profinite group. The relative factor is the profinite index of H, regarded as a subgroup of K. The subgroup H need not be closed because profinite index only sees its topological closure.

The primewise proof compares the finite images of both subgroups in a common finite quotient of G. Closedness of K makes it a profinite group in its own right, while cofinality of ambient open normal subgroups identifies the relative indices of these finite images with the profinite index computed inside K.

Main results

• Subgroup.profiniteIndex_subgroupOf_apply_eq_iSup_relIndex: computes the relative factor from the finite images of a pair of subgroups when the larger one is closed.
• Subgroup.profiniteIndex_subgroupOf_eq_primePower: the relative factor of a subgroup closed inside a larger closed subgroup, when their relative index is a prime power.
• Subgroup.profiniteIndex_subgroupOf_add_profiniteIndex: primewise index multiplicativity.
• Subgroup.profiniteIndex_subgroupOf_mul_profiniteIndex: supernatural index multiplicativity.

References

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

theorem Subgroup.profiniteIndex_subgroupOf_apply_eq_iSup_relIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H K : Subgroup G) (hHK : H ≤ K) (hK : IsClosed ↑K) (ell : Nat.Primes) : (H.subgroupOf K).profiniteIndex ell = ⨆ (N : OpenNormalSubgroup G), ↑(padicValNat (↑ell) ((map (QuotientGroup.mk' ↑N.toOpenSubgroup) H).relIndex (map (QuotientGroup.mk' ↑N.toOpenSubgroup) K)))

The exponent of ell in the relative supernatural index of H in K is the supremum of the ell-adic valuations of the relative indices of the images of H and K in the finite quotients of G.

This is the relative-index counterpart of Subgroup.profiniteOrder_apply_eq_iSup_image and is the comparison that lets all three terms of the tower formula use the same ambient quotients.

theorem Subgroup.profiniteIndex_subgroupOf_add_profiniteIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H K : Subgroup G) (hHK : H ≤ K) (hK : IsClosed ↑K) (ell : Nat.Primes) : (H.subgroupOf K).profiniteIndex ell + K.profiniteIndex ell = H.profiniteIndex ell

Primewise multiplicativity of profinite index through a closed intermediate subgroup.

theorem Subgroup.profiniteIndex_subgroupOf_eq_primePower {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H K : Subgroup G} (hHK : IsClosed ↑(H.subgroupOf K)) (hK : IsClosed ↑K) {q : Nat.Primes} {k : ℕ} (h : H.relIndex K = ↑q ^ k) : (H.subgroupOf K).profiniteIndex = TauCeti.Supernatural.primePower q ↑k

A closed subgroup of prime-power relative index. If H ∩ K is closed in K and the relative index [K : H ∩ K] is the prime power q ^ k, then the supernatural index of H ∩ K inside the profinite group K is that same prime power.

theorem Subgroup.profiniteIndex_subgroupOf_mul_profiniteIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H K : Subgroup G) (hHK : H ≤ K) (hK : IsClosed ↑K) : (H.subgroupOf K).profiniteIndex * K.profiniteIndex = H.profiniteIndex

Multiplicativity of profinite index through a closed subgroup. If H ≤ K ≤ G and K is closed, then [G : H] = [K : H] [G : K] as supernatural numbers.