Consequences of the index formula

Adjoining the centre to a finite-index subgroup keeps the index finite, since it only enlarges the subgroup.

Because the order of a subgroup divides the order of the group -- with the index as cofactor -- invertibility of the order of a finite group in a semiring passes to every subgroup.

Adjoining a two-element subgroup N ⊄ Γ normalised by Γ is also quantified: Γ then has relative index exactly 2 in Γ ⊔ N, so Γ.index = 2 * (Γ ⊔ N).index. Taking N to be the centre gives the Γ.withCenter readings.

Main results

• Subgroup.mem_withCenter_iff: an element of Γ·Z(G) is one of Γ times a central one.
• TauCeti.index_eq_of_natCard_eq_mul: cancel a known nonzero subgroup order from the order-index formula.
• Subgroup.withCenter_le_iff: the universal property — containing Γ·Z(G) is containing both.
• Subgroup.withCenter_eq_self_iff: adjoining the centre changes nothing exactly when the centre already lies inside Γ.
• Subgroup.relIndex_sup_eq_two, Subgroup.index_eq_two_mul_index_sup: the relative index 2 and the index doubling, for an N normalised by Γ whose elements are 1 and a ∉ Γ.
• Subgroup.instCountableQuotient: a coset space of a countable group is countable.
• Subgroup.finiteIndex_of_finiteIndex_subgroupOf: finite index composes along V ≤ U ≤ G.
• Subgroup.compositeTransversal: representatives for G/V obtained by composing representatives for G/U and U/V.
• Subgroup.finiteIndex_inf_comap: H ⊓ f⁻¹(K) has finite index when H does and K has finite index relative to f(H).
• Subgroup.finiteIndex_of_map_eq: the image of a finite-index subgroup under a surjective homomorphism has finite index.
• MonoidHom.finiteIndex_range_comp: finite index of ranges is preserved by composition with a homomorphism of finite-index range.
• MonoidHom.mk_mul_out_bijective: right cosets of a composite range are represented by products of representatives for the two successive ranges.
• Subgroup.relIndex_withCenter_eq_two, Subgroup.index_eq_two_mul_index_withCenter: the same two facts on Γ.withCenter, when the centre is {1, a}.

theorem Subgroup.exists_mul_out_eq {G : Type u} [Group G] (S : Subgroup G) (x : G) : ∃ s ∈ S, s * ⟦x⟧.out = x

A chosen representative of the right coset S x differs from x by an element of S.

def Subgroup.compositeTransversal (G : Type u) [Group G] (U V : Subgroup G) (hVU : V ≤ U) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (s : ↥U ⧸ V.subgroupOf U → ↥U) (q : G ⧸ V) : G

The composite transversal for a subgroup tower. Given V ≤ U ≤ G, representatives t for G/U, and representatives s for U/V, this chooses the representative t a * s b of a coset of V, where (a, b) are its coordinates under Subgroup.quotientEquivProdOfLE'.

Equations

• Subgroup.compositeTransversal G U V hVU t ht s q = t ((Subgroup.quotientEquivProdOfLE' hVU t ht) q).1 * ↑(s ((Subgroup.quotientEquivProdOfLE' hVU t ht) q).2)

@[simp]

theorem Subgroup.compositeTransversal_apply (G : Type u) [Group G] (U V : Subgroup G) (hVU : V ≤ U) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (s : ↥U ⧸ V.subgroupOf U → ↥U) (q : G ⧸ V) : compositeTransversal G U V hVU t ht s q = t ((quotientEquivProdOfLE' hVU t ht) q).1 * ↑(s ((quotientEquivProdOfLE' hVU t ht) q).2)

Evaluation of the composite transversal in the coordinates of the subgroup tower.

theorem Subgroup.compositeTransversal_spec (G : Type u) [Group G] (U V : Subgroup G) (hVU : V ≤ U) (t : G ⧸ U → G) (ht : ∀ (u : G ⧸ U), ↑(t u) = u) (s : ↥U ⧸ V.subgroupOf U → ↥U) (hs : ∀ (v : ↥U ⧸ V.subgroupOf U), ↑(s v) = v) (q : G ⧸ V) : ↑(compositeTransversal G U V hVU t ht s q) = q

The composite transversal for V ≤ U ≤ G represents each coset of V.

theorem MonoidHom.mk_mul_out_bijective {A : Type u} {B : Type v} {C : Type w} [Group A] [Group B] [Group C] (φ₁ : A →* B) (φ₂ : B →* C) (hker : φ₂.ker ≤ φ₁.range) : Function.Bijective fun (x : Quotient (QuotientGroup.rightRel φ₂.range) × Quotient (QuotientGroup.rightRel φ₁.range)) => ⟦φ₂ x.2.out * x.1.out⟧

If φ₂.ker ≤ φ₁.range, the right cosets of (φ₂.comp φ₁).range are represented uniquely by products φ₂ b * c, where b and c are the chosen representatives of right cosets for the two successive ranges.

@[reducible, inline]

abbrev MonoidHom.rangeCompHom {A : Type u} {B : Type v} {C : Type w} [Group A] [Group B] [Group C] (φ₁ : A →* B) (φ₂ : B →* C) : ↥φ₁.range →* ↥(φ₂.comp φ₁).range

The homomorphism from the range of φ₁ to the range of φ₂.comp φ₁ induced by φ₂.

Equations

• φ₁.rangeCompHom φ₂ = (φ₂.comp φ₁.range.subtype).codRestrict (φ₂.comp φ₁).range ⋯

theorem MonoidHom.finiteIndex_range_comp {A : Type u} {B : Type v} {C : Type w} [Group A] [Group B] [Group C] (φ₁ : A →* B) (φ₂ : B →* C) [φ₁.range.FiniteIndex] [φ₂.range.FiniteIndex] : (φ₂.comp φ₁).range.FiniteIndex

If the ranges of φ₁ and φ₂ have finite index, then the range of their composite has finite index.

theorem AddMonoidHom.finiteIndex_range_comp {A : Type u} {B : Type v} {C : Type w} [AddGroup A] [AddGroup B] [AddGroup C] (φ₁ : A →+ B) (φ₂ : B →+ C) [φ₁.range.FiniteIndex] [φ₂.range.FiniteIndex] : (φ₂.comp φ₁).range.FiniteIndex

If the ranges of two additive homomorphisms have finite index, then the range of their composite has finite index.

instance Subgroup.instCountableQuotient {G : Type u_1} [Group G] [Countable G] (H : Subgroup G) : Countable (G ⧸ H)

A coset space of a countable group is countable. A countable group has only countably many cosets of any subgroup. Where a construction runs over G ⧸ H one coset at a time it is this that keeps the family countable — as in ModularGroup.isFundamentalDomain_iUnion_out_inv_smul_fdo, which tiles a fundamental domain for H ≤ PSL(2, ℤ) by one translate of 𝒟ᵒ per coset.

instance AddSubgroup.instCountableQuotient {G : Type u_1} [AddGroup G] [Countable G] (H : AddSubgroup G) : Countable (G ⧸ H)

A coset space of a countable additive group is countable. A countable additive group has only countably many cosets of any subgroup.

theorem Subgroup.finiteIndex_of_finiteIndex_subgroupOf {G : Type u_1} [Group G] (H K : Subgroup G) [K.FiniteIndex] [(H.subgroupOf K).FiniteIndex] : H.FiniteIndex

Finite index composes along a chain of subgroups. If K has finite index in G and H has finite index in K -- that is, the copy H.subgroupOf K of H inside K has finite index -- then H has finite index in G. This is the converse of Subgroup.instFiniteIndex_subgroupOf, which restricts a finite index in G to one in K; neither direction is an instance, because the intermediate subgroup K cannot be recovered from the goal H.FiniteIndex.

theorem AddSubgroup.finiteIndex_of_finiteIndex_addSubgroupOf {G : Type u_1} [AddGroup G] (H K : AddSubgroup G) [K.FiniteIndex] [(H.addSubgroupOf K).FiniteIndex] : H.FiniteIndex

Finite index composes along a chain of additive subgroups. If K has finite index in G and H has finite index in K -- that is, the copy H.addSubgroupOf K of H inside K has finite index -- then H has finite index in G.

theorem Subgroup.finiteIndex_inf_comap {G : Type u_1} {N : Type u_2} [Group G] [Group N] (H : Subgroup G) [H.FiniteIndex] (K : Subgroup N) (f : G →* N) [K.IsFiniteRelIndex (map f H)] : (H ⊓ comap f K).FiniteIndex

Pulling back a subgroup of finite relative index. If H has finite index in G and K has finite index relative to f(H), then H ⊓ f⁻¹(K) has finite index in G: its index in H is the relative index of K in f(H).

theorem Subgroup.finiteIndex_of_map_eq {G : Type u_1} {N : Type u_2} [Group G] [Group N] (H : Subgroup G) [H.FiniteIndex] (f : G →* N) (hf : Function.Surjective ⇑f) {K : Subgroup N} (h : map f H = K) : K.FiniteIndex

The image of a finite-index subgroup under a surjective homomorphism has finite index.

theorem AddSubgroup.finiteIndex_of_map_eq {G : Type u_1} {N : Type u_2} [AddGroup G] [AddGroup N] (H : AddSubgroup G) [H.FiniteIndex] (f : G →+ N) (hf : Function.Surjective ⇑f) {K : AddSubgroup N} (h : map f H = K) : K.FiniteIndex

The image of a finite-index additive subgroup under a surjective homomorphism has finite index.

def Subgroup.withCenter {G : Type u_1} [Group G] (Γ : Subgroup G) : Subgroup G

Γ with the centre of the ambient group adjoined. For Γ ≤ SL(2, ℤ) the centre is {±I}, which acts trivially on ℍ; it is the cosets of Γ·{±I} — not those of Γ itself — that name the distinct translates of 𝒟 tiling a Γ fundamental domain, since q and -q would otherwise be counted as two cosets carrying the same translate. The two subgroups agree exactly when -I ∈ Γ.

Equations

• Γ.withCenter = Γ ⊔ Subgroup.center G

theorem Subgroup.withCenter_def {G : Type u_1} [Group G] (Γ : Subgroup G) : Γ.withCenter = Γ ⊔ center G

Unfolding: Γ.withCenter is the supremum of Γ with the centre.

theorem Subgroup.le_withCenter {G : Type u_1} [Group G] (Γ : Subgroup G) : Γ ≤ Γ.withCenter

Γ sits inside Γ with the centre adjoined.

theorem Subgroup.center_le_withCenter {G : Type u_1} [Group G] (Γ : Subgroup G) : center G ≤ Γ.withCenter

The centre sits inside Γ with the centre adjoined — the other half of the supremum.

@[simp]

theorem Subgroup.withCenter_le_iff {G : Type u_1} [Group G] {Γ H : Subgroup G} : Γ.withCenter ≤ H ↔ Γ ≤ H ∧ center G ≤ H

The universal property of withCenter: a subgroup contains Γ·Z(G) exactly when it contains both Γ and the centre.

theorem Subgroup.mem_withCenter_iff {G : Type u_1} [Group G] {Γ : Subgroup G} {g : G} : g ∈ Γ.withCenter ↔ ∃ γ ∈ Γ, ∃ c ∈ center G, γ * c = g

Characteristic membership for withCenter: an element of Γ·Z(G) is one of Γ times a central one.

@[simp]

theorem Subgroup.withCenter_eq_self_iff {G : Type u_1} [Group G] {Γ : Subgroup G} : Γ.withCenter = Γ ↔ center G ≤ Γ

Adjoining the centre changes nothing exactly when the centre is already inside Γ — the other half of the dichotomy Subgroup.withCenter describes.

instance Subgroup.instFiniteIndexWithCenter {G : Type u_1} [Group G] (Γ : Subgroup G) [Γ.FiniteIndex] : Γ.withCenter.FiniteIndex

theorem Subgroup.relIndex_sup_eq_two {G : Type u_1} [Group G] {Γ : Subgroup G} {a : G} (N : Subgroup G) (hnorm : Γ ≤ normalizer ↑N) (ha : a ∈ N) (haΓ : a ∉ Γ) (hN : ∀ c ∈ N, c = 1 ∨ c = a) : Γ.relIndex (Γ ⊔ N) = 2

A two-element subgroup normalised by Γ and not already inside it has relative index 2. If every element of N is 1 or a, and a ∉ Γ, then Γ ⊔ N splits into the two cosets Γ and Γ * a.

Only normalisation by Γ is asked for, not normality of N in the whole group, so a two-element subgroup normalised by Γ alone is covered. A globally normal N is the special case Subgroup.le_normalizer_of_normal.

Stated for an arbitrary N rather than for the centre, because the centre is often larger than two elements — in GL (Fin 2) ℝ it is every scalar — while the two-element subgroup one actually wants there is Subgroup.zpowers (-1). A caller supplies whichever N is in hand.

a is not assumed to be an involution; it follows from the hypotheses that it is one.

Generalises Mathlib's Subgroup.relindex_adjoinNegOne_eq_two (Mathlib/NumberTheory/ModularForms/ArithmeticSubgroups.lean) from 𝒢 ≤ GL n R with a = -1 to an arbitrary group.

theorem Subgroup.index_eq_two_mul_index_sup {G : Type u_1} [Group G] {Γ : Subgroup G} {a : G} (N : Subgroup G) (hnorm : Γ ≤ normalizer ↑N) (ha : a ∈ N) (haΓ : a ∉ Γ) (hN : ∀ c ∈ N, c = 1 ∨ c = a) : Γ.index = 2 * (Γ ⊔ N).index

The index doubles on adjoining a two-element subgroup normalised by Γ and not inside it. The counting form of Subgroup.relIndex_sup_eq_two.

theorem Subgroup.relIndex_withCenter_eq_two {G : Type u_1} [Group G] {Γ : Subgroup G} {a : G} (ha : a ∈ center G) (haΓ : a ∉ Γ) (hcenter : ∀ c ∈ center G, c = 1 ∨ c = a) : Γ.relIndex Γ.withCenter = 2

When the centre is {1, a} and a ∉ Γ, Γ has relative index exactly 2 in Γ.withCenter. The centre reading of Subgroup.relIndex_sup_eq_two. This is the branch in which the two subgroups genuinely differ; they coincide exactly when the centre already lies inside Γ.

For Γ ≤ SL(2, ℤ) the centre is {±I} and a = -I, so this is the quantitative form of the dichotomy recorded on Subgroup.withCenter: cosets of Γ count each translate of 𝒟 twice unless -I ∈ Γ already.

theorem Subgroup.index_eq_two_mul_index_withCenter {G : Type u_1} [Group G] {Γ : Subgroup G} {a : G} (ha : a ∈ center G) (haΓ : a ∉ Γ) (hcenter : ∀ c ∈ center G, c = 1 ∨ c = a) : Γ.index = 2 * Γ.withCenter.index

When the centre is {1, a} and a ∉ Γ, the index of Γ is twice that of Γ.withCenter. The counting form of Subgroup.relIndex_withCenter_eq_two: it is Γ.withCenter, not Γ, whose cosets index the distinct translates, so a count over Γ-cosets is twice the geometric one.

theorem TauCeti.index_eq_of_natCard_eq_mul {G : Type u_1} [Group G] {H : Subgroup G} {c d : ℕ} (hpos : 0 < c) (hH : Nat.card ↥H = c) (hG : Nat.card G = c * d) : H.index = d

Cancel a known nonzero subgroup order from the order-index formula. If H has order c and its ambient group has order c * d, with c > 0, then H has index d.

theorem TauCeti.isUnit_natCard_subgroup {k : Type u_1} {G : Type u_2} [Semiring k] [Group G] (S : Subgroup G) (hG : IsUnit ↑(Nat.card G)) : IsUnit ↑(Nat.card ↥S)

If the order of a finite group is invertible in k, then so is the order of any subgroup, because the two differ by the index.