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. $$

• Subgroup.exists_finiteIndex_of_leftCoset_cover at least one subgroup $C_i$ has finite index in $G$.

• Subgroup.leftCoset_cover_filter_FiniteIndex the cosets of subgroups of infinite index may be omitted from the covering.

• Subgroup.exists_index_le_card_of_leftCoset_cover : the index of (at least) one of these subgroups does not exceed $n$.

• Subgroup.one_le_sum_inv_index_of_leftCoset_cover : the sum of the inverses of the indexes of the $C_i$ is greater than or equal to 1.

• Subgroup.pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one If the sum of the inverses of the indexes of the subgroups $C_i$ is equal to 1, then the cosets of the subgroups of finite index are pairwise disjoint.

A corollary of Subgroup.exists_finiteIndex_of_leftCoset_cover is:

• Subspace.biUnion_ne_univ_of_ne_top : a vector space over an infinite field cannot be a finite union of proper subspaces.

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

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), ↑t ∈ Subgroup.leftTransversals ↑(D.subgroupOf H) ∧ ⋃ g ∈ t, ↑g • ↑D = ↑H

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), ↑t ∈ AddSubgroup.leftTransversals ↑(D.addSubgroupOf H) ∧ ⋃ g ∈ t, ↑g +ᵥ ↑D = ↑H

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

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

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.

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

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

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

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

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

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 ∈ Finset.filter (fun (x : ι) => H x = H j) s, g i • ↑(H i) ≠ Set.univ) : ∃ i ∈ s, H i ≠ H j ∧ (H i).FiniteIndex

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 ∈ Finset.filter (fun (x : ι) => H x = H j) s, g i +ᵥ ↑(H i) ≠ Set.univ) : ∃ i ∈ s, H i ≠ H j ∧ (H i).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 : ⋃ 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.

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

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 Subgroup.FiniteIndex] : ⋃ k ∈ Finset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k • ↑(H k) = Set.univ ∧ 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧ (∑ i ∈ s, (↑(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_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 AddSubgroup.FiniteIndex] : ⋃ k ∈ Finset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k +ᵥ ↑(H k) = Set.univ ∧ 1 ≤ ∑ i ∈ s, (↑(H i).index)⁻¹ ∧ (∑ i ∈ s, (↑(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 {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 Subgroup.FiniteIndex] : ⋃ k ∈ Finset.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.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 AddSubgroup.FiniteIndex] : ⋃ k ∈ Finset.filter (fun (i : ι) => (H i).FiniteIndex) s, g k +ᵥ ↑(H k) = Set.univ

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.

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)⁻¹

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 Subgroup.FiniteIndex] : ∑ i ∈ s, (↑(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.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 AddSubgroup.FiniteIndex] : ∑ i ∈ s, (↑(H i).index)⁻¹ = 1 → (↑(Finset.filter (fun (i : ι) => (H i).FiniteIndex) s)).PairwiseDisjoint fun (i : ι) => g i +ᵥ ↑(H i)

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.

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

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

theorem Subspace.biUnion_ne_univ_of_top_nmem {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

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

@[deprecated Subspace.biUnion_ne_univ_of_top_nmem]

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 : ⊤ ∉ s) : ⋃ p ∈ s, ↑p ≠ Set.univ

Alias of Subspace.biUnion_ne_univ_of_top_nmem.

@[deprecated Subspace.top_mem_of_biUnion_eq_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 : ⋃ p ∈ s, ↑p = Set.univ) : ⊤ ∈ s

Alias of Subspace.top_mem_of_biUnion_eq_univ.

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 = ⊤