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] [Neumann-1954], Groups Covered By Permutable Subsets, Lemma 4.1 [2] https://mathoverflow.net/a/17398/3332 [3] http://alpha.math.uga.edu/~pete/Neumann54.pdf

source
šŸ“ coverage
theorem Subgroup.exists_leftTransversal_of_FiniteIndex {G : Type u_1} [Group G] {D H : Subgroup G} [D.FiniteIndex] (hD_le_H : D ā‰¤ H) :
āˆƒ (t : Finset ā†„H), IsComplement ā†‘t ā†‘(D.subgroupOf H) āˆ§ ā‹ƒ g āˆˆ t, ā†‘g ā€¢ ā†‘D = ā†‘H
source
šŸ“ coverage
theorem AddSubgroup.exists_leftTransversal_of_FiniteIndex {G : Type u_1} [AddGroup G] {D H : AddSubgroup G} [D.FiniteIndex] (hD_le_H : D ā‰¤ H) :
āˆƒ (t : Finset ā†„H), IsComplement ā†‘t ā†‘(D.addSubgroupOf H) āˆ§ ā‹ƒ g āˆˆ t, ā†‘g +įµ„ ā†‘D = ā†‘H
source
šŸ“ coverage
theorem Subgroup.leftCoset_cover_const_iff_surjOn {G : Type u_1} [Group G] {Ī¹ : Type u_2} {s : Finset Ī¹} {H : Subgroup G} {g : Ī¹ ā†’ G} :
ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘H = Set.univ ā†” Set.SurjOn (fun (x : Ī¹) => ā†‘(g x)) (ā†‘s) Set.univ
source
šŸ“ coverage
theorem AddSubgroup.leftCoset_cover_const_iff_surjOn {G : Type u_1} [AddGroup G] {Ī¹ : Type u_2} {s : Finset Ī¹} {H : AddSubgroup G} {g : Ī¹ ā†’ G} :
ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘H = Set.univ ā†” Set.SurjOn (fun (x : Ī¹) => ā†‘(g x)) (ā†‘s) Set.univ
source
šŸ“ coverage
theorem Subgroup.finiteIndex_of_leftCoset_cover_const {G : Type u_1} [Group G] {Ī¹ : Type u_2} {s : Finset Ī¹} {H : Subgroup G} {g : Ī¹ ā†’ G} (hcovers : ā‹ƒ i āˆˆ s, 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.

source
šŸ“ coverage
theorem AddSubgroup.finiteIndex_of_leftCoset_cover_const {G : Type u_1} [AddGroup G] {Ī¹ : Type u_2} {s : Finset Ī¹} {H : AddSubgroup G} {g : Ī¹ ā†’ G} (hcovers : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘H = Set.univ) :
H.FiniteIndex
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘H = Set.univ) :
H.index ā‰¤ s.card
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘H = Set.univ) :
H.index ā‰¤ s.card
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘H = Set.univ) (hind : H.index = s.card) :
(ā†‘s).PairwiseDisjoint fun (x : Ī¹) => g x ā€¢ ā†‘H
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘H = Set.univ) (hind : H.index = s.card) :
(ā†‘s).PairwiseDisjoint fun (x : Ī¹) => g x +įµ„ ā†‘H
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘(H i) = Set.univ) [DecidableEq (Subgroup G)] (j : Ī¹) (hj : j āˆˆ s) (hcovers' : ā‹ƒ i āˆˆ {x āˆˆ s | H x = H j}, g i ā€¢ ā†‘(H i) ā‰  Set.univ) :
āˆƒ i āˆˆ s, H i ā‰  H j āˆ§ (H i).FiniteIndex
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘(H i) = Set.univ) [DecidableEq (AddSubgroup G)] (j : Ī¹) (hj : j āˆˆ s) (hcovers' : ā‹ƒ i āˆˆ {x āˆˆ s | H x = H j}, g i +įµ„ ā†‘(H i) ā‰  Set.univ) :
āˆƒ i āˆˆ s, H i ā‰  H j āˆ§ (H i).FiniteIndex
source
šŸ“ coverage
theorem Subgroup.exists_finiteIndex_of_leftCoset_cover {G : Type u_1} [Group G] {Ī¹ : Type u_2} {H : Ī¹ ā†’ Subgroup G} {g : Ī¹ ā†’ G} {s : Finset Ī¹} (hcovers : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘(H i) = Set.univ) :
āˆƒ k āˆˆ s, (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.

source
šŸ“ coverage
theorem AddSubgroup.exists_finiteIndex_of_leftCoset_cover {G : Type u_1} [AddGroup G] {Ī¹ : Type u_2} {H : Ī¹ ā†’ AddSubgroup G} {g : Ī¹ ā†’ G} {s : Finset Ī¹} (hcovers : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘(H i) = Set.univ) :
āˆƒ k āˆˆ s, (H k).FiniteIndex
source
šŸ“ coverage
theorem Subgroup.leftCoset_cover_filter_FiniteIndex_aux {G : Type u_1} [Group G] {Ī¹ : Type u_2} {H : Ī¹ ā†’ Subgroup G} {g : Ī¹ ā†’ G} {s : Finset Ī¹} (hcovers : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘(H i) = Set.univ) [DecidablePred FiniteIndex] :
ā‹ƒ k āˆˆ {i āˆˆ s | (H i).FiniteIndex}, g k ā€¢ ā†‘(H k) = Set.univ āˆ§ 1 ā‰¤ āˆ‘ i āˆˆ s, (ā†‘(H i).index)ā»Ā¹ āˆ§ (āˆ‘ i āˆˆ s, (ā†‘(H i).index)ā»Ā¹ = 1 ā†’ (ā†‘({i āˆˆ s | (H i).FiniteIndex})).PairwiseDisjoint fun (i : Ī¹) => g i ā€¢ ā†‘(H i))
source
šŸ“ coverage
theorem AddSubgroup.leftCoset_cover_filter_FiniteIndex_aux {G : Type u_1} [AddGroup G] {Ī¹ : Type u_2} {H : Ī¹ ā†’ AddSubgroup G} {g : Ī¹ ā†’ G} {s : Finset Ī¹} (hcovers : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘(H i) = Set.univ) [DecidablePred FiniteIndex] :
ā‹ƒ k āˆˆ {i āˆˆ s | (H i).FiniteIndex}, g k +įµ„ ā†‘(H k) = Set.univ āˆ§ 1 ā‰¤ āˆ‘ i āˆˆ s, (ā†‘(H i).index)ā»Ā¹ āˆ§ (āˆ‘ i āˆˆ s, (ā†‘(H i).index)ā»Ā¹ = 1 ā†’ (ā†‘({i āˆˆ s | (H i).FiniteIndex})).PairwiseDisjoint fun (i : Ī¹) => g i +įµ„ ā†‘(H i))
source
šŸ“ coverage
theorem Subgroup.leftCoset_cover_filter_FiniteIndex {G : Type u_1} [Group G] {Ī¹ : Type u_2} {H : Ī¹ ā†’ Subgroup G} {g : Ī¹ ā†’ G} {s : Finset Ī¹} (hcovers : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘(H i) = Set.univ) [DecidablePred FiniteIndex] :
ā‹ƒ k āˆˆ {i āˆˆ s | (H i).FiniteIndex}, 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.

source
šŸ“ coverage
theorem AddSubgroup.leftCoset_cover_filter_FiniteIndex {G : Type u_1} [AddGroup G] {Ī¹ : Type u_2} {H : Ī¹ ā†’ AddSubgroup G} {g : Ī¹ ā†’ G} {s : Finset Ī¹} (hcovers : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘(H i) = Set.univ) [DecidablePred FiniteIndex] :
ā‹ƒ k āˆˆ {i āˆˆ s | (H i).FiniteIndex}, g k +įµ„ ā†‘(H k) = Set.univ
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘(H i) = Set.univ) :
1 ā‰¤ āˆ‘ i āˆˆ s, (ā†‘(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.

source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘(H i) = Set.univ) :
1 ā‰¤ āˆ‘ i āˆˆ s, (ā†‘(H i).index)ā»Ā¹
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘(H i) = Set.univ) [DecidablePred FiniteIndex] :
āˆ‘ i āˆˆ s, (ā†‘(H i).index)ā»Ā¹ = 1 ā†’ (ā†‘({i āˆˆ s | (H i).FiniteIndex})).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.

source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘(H i) = Set.univ) [DecidablePred FiniteIndex] :
āˆ‘ i āˆˆ s, (ā†‘(H i).index)ā»Ā¹ = 1 ā†’ (ā†‘({i āˆˆ s | (H i).FiniteIndex})).PairwiseDisjoint fun (i : Ī¹) => g i +įµ„ ā†‘(H i)
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i ā€¢ ā†‘(H i) = Set.univ) :
āˆƒ i āˆˆ s, (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.

source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, g i +įµ„ ā†‘(H i) = Set.univ) :
āˆƒ i āˆˆ s, (H i).FiniteIndex āˆ§ (H i).index ā‰¤ s.card
source
šŸ“ coverage
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 : ā‹ƒ i āˆˆ s, ā†‘(p i) = Set.univ) :
āˆƒ k āˆˆ s, (p k).toAddSubgroup.FiniteIndex
source
theorem Subspace.biUnion_ne_univ_of_top_notMem {k : Type u_1} {E : Type u_2} [DivisionRing k] [Infinite k] [AddCommGroup E] [Module k E] {s : Finset (Subspace k E)} (hs : āŠ¤ āˆ‰ s) :
ā‹ƒ p āˆˆ s, ā†‘p ā‰  Set.univ

A vector space over an infinite field cannot be a finite union of proper subspaces.

source
šŸ“ coverage
theorem Subspace.top_mem_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 : ā‹ƒ p āˆˆ s, ā†‘p = Set.univ) :
āŠ¤ āˆˆ s

A vector space over an infinite field cannot be a finite union of proper subspaces.

source
šŸ“ coverage
theorem Subspace.exists_eq_top_of_iUnion_eq_univ {k : Type u_1} {E : Type u_2} [DivisionRing k] [Infinite k] [AddCommGroup E] [Module k E] {Ī¹ : Sort u_3} [Finite Ī¹] {p : Ī¹ ā†’ Subspace k E} (hcovers : ā‹ƒ (i : Ī¹), ā†‘(p i) = Set.univ) :
āˆƒ (i : Ī¹), p i = āŠ¤