Predecessor transversals and the sharp Schreier index formula

Schreier's lemma, Subgroup.closure_mul_image_eq in Mathlib, says that a subgroup H of a group G = ⟨S⟩ is generated by the Schreier generators r * s * (r * s)‾⁻¹, where r runs over a right transversal R of H containing 1, s runs over S, and g ↦ g‾ is the map Subgroup.IsComplement.toRightFun sending an element to its representative in R. Counting these generators gives [G : H] * |S| of them (Subgroup.exists_finset_card_le_mul). This file sharpens the count to 1 + [G : H] * (|S| - 1), the classical Schreier index formula.

The saving comes from the choice of transversal. A predecessor transversal is a right transversal R of H that contains 1 and satisfies the predecessor condition: every r ≠ 1 in R is r' * s for some r' ∈ R and s ∈ S. Along such a transversal the Schreier generators at the pairs (r', s) with r' * s ∈ R are trivial, and there are at least |R| - 1 such pairs, one for each r ≠ 1. Every subgroup of finite index has a finite predecessor transversal with respect to every generating set.

The predecessor condition is a one-step condition: it does not ask that every element of R be reached from 1 by a chain of such steps, so it allows cycles: if S contains both s and s⁻¹, then r = r' * s and r' = r * s⁻¹ satisfy it with neither r nor r' reached from 1. It is therefore weaker than a Schreier transversal in the sense of the references below, a prefix-closed set of reduced words in S ∪ S⁻¹, and it only uses letters from S, not from S⁻¹; the name records the condition that is actually imposed. The one-step condition is all that the index formula needs. The transversal built in Subgroup.exists_finset_isPredecessorTransversal starts from {1} and adds elements of the form r * s with r already present, so it is reached from 1 by chains of steps, but the predicate does not record this.

Main results

• Subgroup.IsPredecessorTransversal: a right transversal containing 1 in which every other element is an element of the transversal times an element of S.
• Subgroup.exists_finset_isPredecessorTransversal: a finite-index subgroup has a finite predecessor transversal with respect to every generating set.
• Subgroup.exists_finset_card_le_one_add_index_mul: Schreier's index formula: a subgroup of index n in a group generated by d elements is generated by 1 + n * (d - 1) elements.
• Subgroup.rank_le_one_add_index_mul_rank_sub_one: the same for Group.rank, sharpening Mathlib's Subgroup.rank_le_index_mul_rank.

References

• D. L. Johnson, Presentations of Groups, 2nd ed., Cambridge University Press, 1997, Chapter 9.
• W. Magnus, A. Karrass and D. Solitar, Combinatorial Group Theory, Section 2.3.

@[simp]

theorem Subgroup.IsComplement.coe_toRightFun_of_mem {G : Type u_1} [Group G] {H : Subgroup G} {R : Set G} (hR : IsComplement (↑H) R) {r : G} (hr : r ∈ R) : ↑(hR.toRightFun r) = r

The representative of an element of a right transversal is that element.

structure Subgroup.IsPredecessorTransversal {G : Type u_1} [Group G] (H : Subgroup G) (S R : Set G) : Prop

A predecessor transversal of a subgroup H with respect to a set S: a right transversal R of H, so that H * R = G with unique factorization, which contains 1 and satisfies the predecessor condition that every r ≠ 1 in R is r' * s for some r' ∈ R and s ∈ S. This is a one-step condition: it does not require r to be reached from 1 by a chain of such steps, so it is weaker than a Schreier transversal in the usual prefix-closed sense, and it is all that the index formula uses. When S generates G, the Schreier generators of H at the pairs (r', s) with r' * s ∈ R are trivial, which is what sharpens Schreier's lemma to the index formula Subgroup.exists_finset_card_le_one_add_index_mul.

• isComplement : IsComplement (↑H) R

  R is a right transversal of H.

• one_mem : 1 ∈ R

  R contains the identity.

• exists_mul_eq (r : G) : r ∈ R → r ≠ 1 → ∃ r' ∈ R, ∃ s ∈ S, r' * s = r

  Every element of R other than 1 is an element of R times an element of S.

theorem Subgroup.exists_finset_isPredecessorTransversal {G : Type u_1} [Group G] {S : Set G} (H : Subgroup G) [H.FiniteIndex] (hS : closure S = ⊤) : ∃ (R : Finset G), H.IsPredecessorTransversal S ↑R

Existence of predecessor transversals. A subgroup of finite index has a finite predecessor transversal with respect to every generating set of the ambient group.

theorem Subgroup.exists_finset_card_le_one_add_index_mul {G : Type u_1} [Group G] (H : Subgroup G) [H.FiniteIndex] {S : Finset G} (hS : closure ↑S = ⊤) : ∃ (T : Finset ↥H), T.card ≤ 1 + H.index * (S.card - 1) ∧ closure ↑T = ⊤

Schreier's index formula. If H has finite index n in a group generated by a finite set S of d elements, then H is generated by at most 1 + n * (d - 1) elements. This sharpens Mathlib's Subgroup.exists_finset_card_le_mul, which gives n * d.

theorem Subgroup.rank_le_one_add_index_mul_rank_sub_one {G : Type u_1} [Group G] {H : Subgroup G} [Group.FG G] [H.FiniteIndex] : Group.rank ↥H ≤ 1 + H.index * (Group.rank G - 1)

Schreier's index formula for Group.rank: rank H ≤ 1 + [G : H] * (rank G - 1) for a finite-index subgroup H of a finitely generated group G. This sharpens Mathlib's Subgroup.rank_le_index_mul_rank.