Documentation

Mathlib.GroupTheory.CosetCover

Lemma of B. H. Neumann on coverings of a group by cosets. #

Let the group $G$ be the union of finitely many, let us say $n$, left cosets of subgroups $C₁$, $C₂$, ..., $Cₙ$: $$ G = ⋃_{i = 1}^n C_i g_i. $$

A corollary of Subgroup.exists_finiteIndex_of_leftCoset_cover is:

This can be used to show that an algebraic extension of fields is determined by the set of all minimal polynomials (not proved here).

[1] [Neu54], Groups Covered By Permutable Subsets, Lemma 4.1 [2] https://mathoverflow.net/a/17398/3332 [3] http://alpha.math.uga.edu/~pete/Neumann54.pdf

theorem AddSubgroup.exists_leftTransversal_of_FiniteIndex {G : Type u_1} [AddGroup G] {D : AddSubgroup G} {H : AddSubgroup G} [D.FiniteIndex] (hD_le_H : D H) :
∃ (t : Finset H), t AddSubgroup.leftTransversals (D.addSubgroupOf H) gt, g +ᵥ D = H
theorem Subgroup.exists_leftTransversal_of_FiniteIndex {G : Type u_1} [Group G] {D : Subgroup G} {H : Subgroup G} [D.FiniteIndex] (hD_le_H : D H) :
∃ (t : Finset H), t Subgroup.leftTransversals (D.subgroupOf H) gt, g D = H
theorem AddSubgroup.leftCoset_cover_const_iff_surjOn {G : Type u_1} [AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ιG} :
is, g i +ᵥ H = Set.univ Set.SurjOn (fun (x : ι) => (g x)) (↑s) Set.univ
theorem Subgroup.leftCoset_cover_const_iff_surjOn {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ιG} :
is, g i H = Set.univ Set.SurjOn (fun (x : ι) => (g x)) (↑s) Set.univ
theorem AddSubgroup.finiteIndex_of_leftCoset_cover_const {G : Type u_1} [AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ιG} (hcovers : is, g i +ᵥ H = Set.univ) :
H.FiniteIndex
theorem Subgroup.finiteIndex_of_leftCoset_cover_const {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ιG} (hcovers : is, g i H = Set.univ) :
H.FiniteIndex

If H is a subgroup of G and G is the union of a finite family of left cosets of H then H has finite index.

theorem AddSubgroup.index_le_of_leftCoset_cover_const {G : Type u_1} [AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ιG} (hcovers : is, g i +ᵥ H = Set.univ) :
H.index s.card
theorem Subgroup.index_le_of_leftCoset_cover_const {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ιG} (hcovers : is, g i H = Set.univ) :
H.index s.card
theorem AddSubgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq {G : Type u_1} [AddGroup G] {ι : Type u_2} {s : Finset ι} {H : AddSubgroup G} {g : ιG} (hcovers : is, g i +ᵥ H = Set.univ) (hind : H.index = s.card) :
(↑s).PairwiseDisjoint fun (x : ι) => g x +ᵥ H
theorem Subgroup.pairwiseDisjoint_leftCoset_cover_const_of_index_eq {G : Type u_1} [Group G] {ι : Type u_2} {s : Finset ι} {H : Subgroup G} {g : ιG} (hcovers : is, g i H = Set.univ) (hind : H.index = s.card) :
(↑s).PairwiseDisjoint fun (x : ι) => g x H
theorem AddSubgroup.exists_finiteIndex_of_leftCoset_cover_aux {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ιAddSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i +ᵥ (H i) = Set.univ) [DecidableEq (AddSubgroup G)] (j : ι) (hj : j s) (hcovers' : iFinset.filter (fun (x : ι) => H x = H j) s, g i +ᵥ (H i) Set.univ) :
is, H i H j (H i).FiniteIndex
theorem Subgroup.exists_finiteIndex_of_leftCoset_cover_aux {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i (H i) = Set.univ) [DecidableEq (Subgroup G)] (j : ι) (hj : j s) (hcovers' : iFinset.filter (fun (x : ι) => H x = H j) s, g i (H i) Set.univ) :
is, H i H j (H i).FiniteIndex
theorem AddSubgroup.exists_finiteIndex_of_leftCoset_cover {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ιAddSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i +ᵥ (H i) = Set.univ) :
ks, (H k).FiniteIndex
theorem Subgroup.exists_finiteIndex_of_leftCoset_cover {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i (H i) = Set.univ) :
ks, (H k).FiniteIndex

Let the group G be the union of finitely many left cosets g i • H i. Then at least one subgroup H i has finite index in G.

theorem AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ιAddSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i +ᵥ (H i) = Set.univ) [DecidablePred AddSubgroup.FiniteIndex] :
kFinset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k +ᵥ (H k) = Set.univ 1 is, (↑(H i).index)⁻¹ (is, (↑(H i).index)⁻¹ = 1(↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i +ᵥ (H i))
theorem Subgroup.leftCoset_cover_filter_FiniteIndex_aux {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i (H i) = Set.univ) [DecidablePred Subgroup.FiniteIndex] :
kFinset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k (H k) = Set.univ 1 is, (↑(H i).index)⁻¹ (is, (↑(H i).index)⁻¹ = 1(↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i (H i))
theorem AddSubgroup.leftCoset_cover_filter_FiniteIndex {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ιAddSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i +ᵥ (H i) = Set.univ) [DecidablePred AddSubgroup.FiniteIndex] :
kFinset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k +ᵥ (H k) = Set.univ
theorem Subgroup.leftCoset_cover_filter_FiniteIndex {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i (H i) = Set.univ) [DecidablePred Subgroup.FiniteIndex] :
kFinset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k (H k) = Set.univ

Let the group G be the union of finitely many left cosets g i • H i. Then the cosets of subgroups of infinite index may be omitted from the covering.

theorem AddSubgroup.one_le_sum_inv_index_of_leftCoset_cover {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ιAddSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i +ᵥ (H i) = Set.univ) :
1 is, (↑(H i).index)⁻¹
theorem Subgroup.one_le_sum_inv_index_of_leftCoset_cover {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i (H i) = Set.univ) :
1 is, (↑(H i).index)⁻¹

Let the group G be the union of finitely many left cosets g i • H i. Then the sum of the inverses of the indexes of the subgroups H i is greater than or equal to 1.

theorem AddSubgroup.pairwiseDisjoint_leftCoset_cover_of_sum_neg_index_eq_zero {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ιAddSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i +ᵥ (H i) = Set.univ) [DecidablePred AddSubgroup.FiniteIndex] :
is, (↑(H i).index)⁻¹ = 1(↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i +ᵥ (H i)
theorem Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i (H i) = Set.univ) [DecidablePred Subgroup.FiniteIndex] :
is, (↑(H i).index)⁻¹ = 1(↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i (H i)

Let the group G be the union of finitely many left cosets g i • H i. If the sum of the inverses of the indexes of the subgroups H i is equal to 1, then the cosets of the subgroups of finite index are pairwise disjoint.

theorem AddSubgroup.exists_index_le_card_of_leftCoset_cover {G : Type u_1} [AddGroup G] {ι : Type u_2} {H : ιAddSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i +ᵥ (H i) = Set.univ) :
is, (H i).FiniteIndex (H i).index s.card
theorem Subgroup.exists_index_le_card_of_leftCoset_cover {G : Type u_1} [Group G] {ι : Type u_2} {H : ιSubgroup G} {g : ιG} {s : Finset ι} (hcovers : is, g i (H i) = Set.univ) :
is, (H i).FiniteIndex (H i).index s.card

B. H. Neumann Lemma : If a finite family of cosets of subgroups covers the group, then at least one of these subgroups has index not exceeding the number of cosets.

theorem Submodule.exists_finiteIndex_of_cover {R : Type u_1} {M : Type u_2} {ι : Type u_3} [Ring R] [AddCommGroup M] [Module R M] {p : ιSubmodule R M} {s : Finset ι} (hcovers : is, (p i) = Set.univ) :
ks, (p k).toAddSubgroup.FiniteIndex
theorem Subspace.biUnion_ne_univ_of_ne_top {k : Type u_1} {E : Type u_2} [DivisionRing k] [Infinite k] [AddCommGroup E] [Module k E] {s : Finset (Subspace k E)} (hs : ps, p ) :
ps, p Set.univ
theorem Subspace.exists_eq_top_of_biUnion_eq_univ {k : Type u_1} {E : Type u_2} [DivisionRing k] [Infinite k] [AddCommGroup E] [Module k E] {s : Finset (Subspace k E)} (hcovers : ps, p = Set.univ) :
ps, p =