Indices of subgroups of profinite groups

The index of a subgroup of a profinite group is a supernatural number. Its exponent at a prime ℓ is the supremum of the ℓ-adic valuations of the indices of the subgroup's images in all finite continuous quotients.

The definition applies to an arbitrary subgroup. It only sees the subgroup's topological closure, as every finite continuous quotient has discrete topology. In particular, its index is one exactly when the subgroup is dense; for closed subgroups, this says exactly that the subgroup is the whole group. These closure comparisons are the starting point for the usual description as the least common multiple of the indices of open overgroups.

Main results

• Subgroup.profiniteIndex: the supernatural index of a subgroup of a profinite group.
• Subgroup.profiniteIndex_anti: subgroup inclusion reverses supernatural indices.
• Subgroup.profiniteIndex_eq_iSup_openSubgroup: the description as the least common multiple of the indices of open overgroups.
• OpenSubgroup.profiniteIndex_eq_ofNat_index: agreement with the ordinary index for an open subgroup.
• Subgroup.profiniteIndex_eq_primePower: an open subgroup whose ordinary index is a power of a prime has that supernatural prime power as its index.
• Subgroup.profiniteIndex_topologicalClosure: taking topological closure does not change the index.
• Subgroup.profiniteIndex_eq_one_iff_topologicalClosure_eq_top: the index is one exactly for dense subgroups.
• Subgroup.profiniteIndex_eq_one_iff: the closed-subgroup specialization.
• Subgroup.not_dvd_profiniteIndex_iff_forall_not_dvd_index: a prime divides the supernatural index exactly when it divides the index of some image in a finite continuous quotient.
• Subgroup.profiniteIndex_eq_bot_iff_topologicalClosure_eq_top and Subgroup.profiniteIndex_eq_bot_iff: the simp-normal forms of the two previous results, since the supernatural unit is the bottom element.
• Subgroup.isOpen_iff_isClosed_and_isNatural_profiniteIndex: openness is equivalent to closedness and natural supernatural index.

References

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

noncomputable def Subgroup.profiniteIndex {G : Type u_1} [Group G] [TopologicalSpace G] (H : Subgroup G) : TauCeti.Supernatural

The index of a subgroup of a profinite group, as a supernatural number. At a prime ℓ, it is the supremum over open normal subgroups N of the ℓ-adic valuations of [G/N : HN/N].

The definition makes sense for an arbitrary subgroup; closedness is required only by results that regard the subgroup itself as profinite.

Equations

• H.profiniteIndex = TauCeti.Supernatural.ofFun fun (ℓ : Nat.Primes) => ⨆ (N : OpenNormalSubgroup G), ↑(padicValNat (↑ℓ) (Subgroup.map (QuotientGroup.mk' ↑N.toOpenSubgroup) H).index)

@[simp]

theorem Subgroup.profiniteIndex_apply {G : Type u_1} [Group G] [TopologicalSpace G] (H : Subgroup G) (ℓ : Nat.Primes) : H.profiniteIndex ℓ = ⨆ (N : OpenNormalSubgroup G), ↑(padicValNat (↑ℓ) (map (QuotientGroup.mk' ↑N.toOpenSubgroup) H).index)

The exponent of a profinite index at a prime is the supremum of the valuations of the indices in the finite continuous quotients.

@[simp]

theorem Subgroup.profiniteIndex_top {G : Type u_1} [Group G] [TopologicalSpace G] : ⊤.profiniteIndex = 1

The whole group has supernatural index one.

theorem Subgroup.profiniteIndex_eq_iSup_ofNat {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (H : Subgroup G) : H.profiniteIndex = ⨆ (N : OpenNormalSubgroup G), TauCeti.Supernatural.ofNat ⟨(map (QuotientGroup.mk' ↑N.toOpenSubgroup) H).index, ⋯⟩

The supernatural index is equivalently the supremum of the ordinary positive indices of the images in finite continuous quotients.

theorem Subgroup.profiniteIndex_anti {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H K : Subgroup G} (h : H ≤ K) : K.profiniteIndex ≤ H.profiniteIndex

Inclusion of subgroups reverses their supernatural indices.

theorem Subgroup.profiniteIndex_eq_iSup_openSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (H : Subgroup G) : H.profiniteIndex = ⨆ (U : { U : OpenSubgroup G // H ≤ ↑U }), TauCeti.Supernatural.ofNat ⟨(↑↑U).index, ⋯⟩

The profinite index is the least common multiple, in the supernatural lattice, of the ordinary indices of the open subgroups containing H.

Although the usual statement assumes that H is closed, the formula holds for every subgroup: an open subgroup contains H exactly when it contains its closure.

theorem Subgroup.profiniteIndex_apply_eq_iSup_openSubgroup {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (H : Subgroup G) (ℓ : Nat.Primes) : H.profiniteIndex ℓ = ⨆ (U : { U : OpenSubgroup G // H ≤ ↑U }), ↑(padicValNat (↑ℓ) (↑↑U).index)

Primewise form of profiniteIndex_eq_iSup_openSubgroup.

@[simp]

theorem OpenSubgroup.profiniteIndex_eq_ofNat_index {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) : (↑U).profiniteIndex = TauCeti.Supernatural.ofNat ⟨(↑U).index, ⋯⟩

For an open subgroup, the supernatural index is the prime factorization of its ordinary index.

theorem OpenSubgroup.profiniteIndex_apply_eq_padicValNat {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (U : OpenSubgroup G) (ℓ : Nat.Primes) : (↑U).profiniteIndex ℓ = ↑(padicValNat (↑ℓ) (↑U).index)

Primewise, the profinite index of an open subgroup is the valuation of its ordinary index.

theorem Subgroup.profiniteIndex_eq_primePower {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {H : Subgroup G} (hH : IsOpen ↑H) {q : Nat.Primes} {k : ℕ} (h : H.index = ↑q ^ k) : H.profiniteIndex = TauCeti.Supernatural.primePower q ↑k

An open subgroup of prime-power index has that supernatural prime power as its index. This is the shape every open-subgroup index in a pro-q group takes, and it avoids the positivity side condition of OpenSubgroup.profiniteIndex_eq_ofNat_index. Openness is not superfluous: by Subgroup.isOpen_iff_isClosed_and_isNatural_profiniteIndex a closed subgroup that is not open has an index no finite exponent describes.

theorem Subgroup.not_dvd_profiniteIndex_iff_forall_not_dvd_index {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] (H : Subgroup G) (ℓ : Nat.Primes) : ¬TauCeti.Supernatural.primePower ℓ 1 ∣ H.profiniteIndex ↔ ∀ (N : OpenNormalSubgroup G), ¬↑ℓ ∣ (map (QuotientGroup.mk' ↑N.toOpenSubgroup) H).index

The finite-quotient and supernatural-index formulations of the prime-to-ℓ condition for a subgroup of a profinite group agree.

@[simp]

theorem Subgroup.profiniteIndex_topologicalClosure {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] (H : Subgroup G) : H.topologicalClosure.profiniteIndex = H.profiniteIndex

Taking the topological closure of a subgroup does not change its supernatural index.

theorem Subgroup.profiniteIndex_eq_one_iff_topologicalClosure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) : H.profiniteIndex = 1 ↔ H.topologicalClosure = ⊤

A subgroup of a profinite group has supernatural index one exactly when it is dense.

@[simp]

theorem Subgroup.profiniteIndex_eq_bot_iff_topologicalClosure_eq_top {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) : H.profiniteIndex = ⊥ ↔ H.topologicalClosure = ⊤

Simp-normal form of profiniteIndex_eq_one_iff_topologicalClosure_eq_top: the supernatural unit is the bottom element, so simp states index one as profiniteIndex H = ⊥.

theorem Subgroup.profiniteIndex_eq_one_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) : H.profiniteIndex = 1 ↔ H = ⊤

A closed subgroup of a profinite group has supernatural index one exactly when it is the whole group.

@[simp]

theorem Subgroup.profiniteIndex_eq_bot_iff {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) (hH : IsClosed ↑H) : H.profiniteIndex = ⊥ ↔ H = ⊤

Simp-normal form of profiniteIndex_eq_one_iff, stating index one for a closed subgroup as profiniteIndex H = ⊥. Its priority is above profiniteIndex_eq_bot_iff_topologicalClosure_eq_top, so that a closed subgroup simplifies to H = ⊤ rather than to a statement about its closure.

theorem Subgroup.isOpen_iff_isClosed_and_isNatural_profiniteIndex {G : Type u_1} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (H : Subgroup G) : IsOpen ↑H ↔ IsClosed ↑H ∧ H.profiniteIndex.IsNatural

A subgroup of a profinite group is open exactly when it is closed and its supernatural index is a natural number.