feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann)

[AntoineChambert-Loir]

Lemma of B. H. Neumann on covering a group by finitely many cosets of subgroups.

---

Zulip

[bustercopley]

Thanks for the review, @alreadydone. I'll have a go at the corollary you stated, but probably nothing stronger for now.

[bustercopley]

[Edited] Do you have any opinion on where Subspace.biUnion_ne_univ_of_lt_top (signature below) should go? For my part I think it's ok here in GroupTheory.CosetCover, as a corollary.

Alternatives:

• LinearAlgebra.Basis.VectorSpace (for the Module.Free instance, but this is currently a small and focused module)
• Algebra.CharP.ExpChar (suggested by #find_home but doesn't sound good)

variable {k E ι : Type*} [DivisionRing k] [Infinite k] [AddCommGroup E] [Module k E]
    {s : Finset (Subspace k E)} (hs : ∀ p ∈ s, p < ⊤)

theorem Subspace.biUnion_ne_univ_of_lt_top :
    ⋃ p ∈ s, (p : Set E) ≠ Set.univ := by
  sorry

[AntoineChambert-Loir]

I believe it sits nicely here. (Moreover, putting it elsewhere would require to add an import to that file.)

[alreadydone]

Thanks! Here are some slight golf and a rephrase of the vector space result:

theorem Subspace.exists_eq_top_of_biUnion_eq_univ (hcovers : ⋃ p ∈ s, (p : Set E) = Set.univ) :
    ∃ p ∈ s, p = ⊤

I also changed p < ⊤ in the assumptions to p ≠ ⊤ for the same reason that people prefers n ≠ 0 in the assumptions but 0 < n in the conclusions for n : ℕ.

I'm not completely sure what should be the canonical spelling regarding finiteness. We've chosen to use Finset but users may apply it to a finite type (Finite) or a finite set (Set.Finite). However it's not too hard to convert between them and the current choice is reasonable, and I don't think we should provide three versions of every result.

The main result Subgroup.one_le_sum_inv_index_of_leftCoset_cover in this PR can be strengthened to say that if the sum of 1/index equals 1, then the finite-index cosets must be pairwise disjoint. This could be used to show that #K+1 proper vector subspaces are necessary to cover a vector space over a finite field K. (In finite dimension one can also use counting. The argument in Clark's paper uses the irredundant result which may not be of enough general interest; but I think it's worth adding the results saying #K+1 vector spaces or #K affine subspaces are necessary to cover a finite-dimensional vector space, in some later PR.

[bustercopley]

Here are some slight golf and a rephrase of the vector space result

Thank you, I pushed those.

[AntoineChambert-Loir]

The pr is very close to proving disjointness of cosets when the density equals one. It might however be necessary to refactor the intermediate construction to transfer more properties than is presently done. (Density is unchanged, nor is disjointness)

For vector spaces over finite fields, I am wondering whether proofs in the Chevalley-Warning/Combinatorial Nullstellensatz style aren't easier. (Does Mathlib have the latter?)

[bustercopley]

The pr is very close to proving disjointness of cosets when the density equals one. It might however be necessary to refactor the intermediate construction to transfer more properties than is presently done. (Density is unchanged, nor is disjointness)

Here is a commit that includes the density and disjointness in the transfer. I haven't tried to use it to prove disjointness of cosets when the density equals one. (The commit also introduces a structure LeftCosetCover. It might be a bit too heavyweight.)

For vector spaces over finite fields, I am wondering whether proofs in the Chevalley-Warning/Combinatorial Nullstellensatz style aren't easier. (Does Mathlib have the latter?)

Can you trick me into believing it's not as difficult as it sounds? :smile:

[AntoineChambert-Loir]

OMG! I was in the middle of proving disjointness. Probably if I pull your commit, it'll be done.

[AntoineChambert-Loir]

I can assure you, it is not as difficult as it sounds. In fact, for subspaces of vector spaces, it would have been easier to use this machine than Neumann's lemma (but I didn't know that lemma and found it fun!).

[bustercopley]

I can assure you, it is not as difficult as it sounds. In fact, for subspaces of vector spaces, it would have been easier to use this machine than Neumann's lemma (but I didn't know that lemma and found it fun!).

I was quite taken with it too! (Thanks again for the suggestion, @alreadydone.)

[bustercopley]

I had no success refactoring the unwieldy auxiliary lemma Subgroup.leftCoset_cover_filter_FiniteIndex_aux, I'm afraid.

[AntoineChambert-Loir]

I'll try something this afternoon once I've finished that urgent stack of grading.

[github-actions[bot]]

PR summary c455742c01

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.GroupTheory.CosetCover	1062

---

Declarations diff

+ Finite.preimage' + Submodule.exists_finiteIndex_of_cover + Subspace.biUnion_ne_univ_of_ne_top + Subspace.exists_eq_top_of_biUnion_eq_univ + exists_finiteIndex_of_leftCoset_cover + exists_finiteIndex_of_leftCoset_cover_aux + exists_index_le_card_of_leftCoset_cover + exists_leftTransversal_of_FiniteIndex + finiteIndex_iInf + finiteIndex_iInf' + finiteIndex_of_leftCoset_cover_const + index_le_of_leftCoset_cover_const + instFiniteIndex_subgroupOf + leftCoset_cover_const_iff_surjOn + leftCoset_cover_filter_FiniteIndex + leftCoset_cover_filter_FiniteIndex_aux + one_le_sum_inv_index_of_leftCoset_cover + pairwiseDisjoint_leftCoset_cover_const_of_index_eq + pairwiseDisjoint_leftCoset_cover_of_sum_inv_index_eq_one ++ finite_iff

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

[faenuccio]

I have removed the awaiting-review label according to the decision explained here https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Changes.20to.20the.20.23queue/near/450176907

[riccardobrasca]

Thanks!

bors merge

[mathlib-bors[bot]]

Build failed:

• Build

[riccardobrasca]

As usual something changed in mathlib, please merge master and fix the error. Thanks!

bors d+

[mathlib-bors[bot]]

:v: AntoineChambert-Loir can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[AntoineChambert-Loir]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style