[Merged by Bors] - feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann) #13047

AntoineChambert-Loir · 2024-05-20T02:33:43Z

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

Zulip

Mathlib/GroupTheory/Neumann.lean

docs/references.bib

Mathlib/GroupTheory/BHNeumann.lean

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Used once. It is nice, but it doesn't belong here and we can do without it.

Mathlib/GroupTheory/CosetCover.lean

github-actions · 2024-06-21T13:30:35Z

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>

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

jcommelin

Sorry, need to run after only a trivial comment.

Mathlib/GroupTheory/CosetCover.lean

faenuccio · 2024-07-09T19:11:50Z

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 · 2024-07-25T11:28:25Z

Mathlib/GroupTheory/CosetCover.lean

+    {s : Finset (Subspace k E)}
+
+/- A vector space over an infinite field cannot be a finite union of proper subspaces. -/
+theorem Subspace.biUnion_ne_univ_of_ne_top (hs : ∀ p ∈ s, p ≠ ⊤) :


Can this be generalized to free module over some class of rings?

It's false for Z² as a Z-module, by taking the pre images of the three mod-2 lines. Maybe if all residue fields are infinite...

OK, it's complicated. It doesn't matter.

It's a good question, obviously, and in some sense, Neumann's lemma gives some answers. If you have a finitely generated module, then every submodule is contained in a maximal one whose co-quotient is a residue field, hence is infinite if all residue fields are infinite.

But I have to admit that my way of proving the case of vector spaces is not via Neumann's lemma but via polynomials (over an infinite field, a nonzero polynomial does not vanish identically).

riccardobrasca · 2024-07-26T07:40:04Z

Thanks!

bors merge

#13047) Lemma of B. H. Neumann on covering a group by finitely many cosets of subgroups. Co-authored-by: Richard Copley <[email protected]> Co-authored-by: Junyan Xu <[email protected]> Co-authored-by: Richard Copley <[email protected]>

mathlib-bors · 2024-07-26T08:26:52Z

Build failed:

Build

riccardobrasca · 2024-07-26T08:28:19Z

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

bors d+

mathlib-bors · 2024-07-26T08:28:22Z

✌️ 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 · 2024-07-26T08:50:44Z

bors r+

#13047) Lemma of B. H. Neumann on covering a group by finitely many cosets of subgroups. Co-authored-by: Richard Copley <[email protected]> Co-authored-by: Junyan Xu <[email protected]> Co-authored-by: Richard Copley <[email protected]>

mathlib-bors · 2024-07-26T09:00:55Z

Pull request successfully merged into master.

Build succeeded:

initial commit

46cee95

github-actions bot reviewed May 20, 2024

View reviewed changes

Mathlib/GroupTheory/Neumann.lean Outdated Show resolved Hide resolved

AntoineChambert-Loir added 3 commits May 21, 2024 20:05

add comments

f555a84

merge with Richard Copley's file and almost conclude

3e20800

add bibtex

39cc81b

github-actions bot reviewed May 22, 2024

View reviewed changes

docs/references.bib Outdated Show resolved Hide resolved

AntoineChambert-Loir added 3 commits May 21, 2024 21:32

rename to BHNeumann, add BHNeymann in Mathlib.lean

879d52d

add docstring

5cdb58b

obey to reviewdog

8c94f62

github-actions bot reviewed May 22, 2024

View reviewed changes

docs/references.bib Outdated Show resolved Hide resolved

little golfs; linter fixes; comment fixes

f9479b8

bustercopley mentioned this pull request May 22, 2024

A lemma of B. H. Neumann. #13040

Closed

Last step

87cd127

github-actions bot reviewed May 22, 2024

View reviewed changes

bustercopley added 8 commits May 22, 2024 14:35

lint

3bf9897

renames

2be9ae1

golf

50cf0a2

golf

5872d97

reorganize and golf

a1bb3c2

variable declarations

53998f2

clear discharged hypotheses (via replace) to keep context tidier

0d4d5c1

golf 22 lines

4b3f3b7

bustercopley force-pushed the ACL/Neumann branch from 1132dad to 4b3f3b7 Compare May 24, 2024 22:11

simplify

ce82517

github-actions bot reviewed May 24, 2024

View reviewed changes

Mathlib/GroupTheory/BHNeumann.lean Outdated Show resolved Hide resolved

Mathlib/GroupTheory/BHNeumann.lean Outdated Show resolved Hide resolved

bustercopley and others added 5 commits May 26, 2024 10:27

Update Mathlib/GroupTheory/BHNeumann.lean

effcd7b

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

Use Finset throughout

a085502

cleanup, mv some lemmas to mathlib files

b97ed75

reduce duplication

9b844e7

a bit of golfing and refactoring

e080877

bustercopley added 2 commits June 21, 2024 14:27

Delete lemma Subgroup.mem_leftCoset_iff

47e1518

Used once. It is nice, but it doesn't belong here and we can do without it.

Merge remote-tracking branch 'origin/master' into ACL/Neumann

d0a92d6

github-actions bot reviewed Jun 21, 2024

View reviewed changes

Mathlib/GroupTheory/CosetCover.lean Outdated Show resolved Hide resolved

Update Mathlib/GroupTheory/CosetCover.lean

1547794

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

jcommelin reviewed Jul 5, 2024

View reviewed changes

Mathlib/GroupTheory/CosetCover.lean Outdated Show resolved Hide resolved

kim-em removed the awaiting-review label Jul 9, 2024

add namespace as requested

d38def4

AntoineChambert-Loir added the awaiting-review-DONT-USE Read the "Changes to the #queue" announcement on Zulip label Jul 9, 2024

faenuccio removed the awaiting-review-DONT-USE Read the "Changes to the #queue" announcement on Zulip label Jul 9, 2024

riccardobrasca reviewed Jul 25, 2024

View reviewed changes

small simplifications

f4e84d2

github-actions bot added the ready-to-merge This PR has been sent to bors. label Jul 26, 2024

github-actions bot added the delegated label Jul 26, 2024

AntoineChambert-Loir added 2 commits July 26, 2024 10:31

Merge branch 'master' into ACL/Neumann

b0e196c

merge and adjust

c455742

mathlib-bors bot changed the title ~~feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann)~~ [Merged by Bors] - feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann) Jul 26, 2024

mathlib-bors bot closed this Jul 26, 2024

mathlib-bors bot deleted the ACL/Neumann branch July 26, 2024 09:00

adomani mentioned this pull request Aug 1, 2024

feat: MiM PR report #15355

Open

alreadydone mentioned this pull request Oct 29, 2024

[Merged by Bors] - feat(FieldTheory): minimal polynomials determine an algebraic extension (Isaacs 1980) #18412

Closed

2 tasks

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann) #13047

[Merged by Bors] - feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann) #13047

AntoineChambert-Loir commented May 20, 2024 •

edited by bustercopley

Loading

github-actions bot commented Jun 21, 2024 •

edited

Loading

Declarations diff

jcommelin left a comment

faenuccio commented Jul 9, 2024

riccardobrasca Jul 25, 2024

AntoineChambert-Loir Jul 25, 2024

riccardobrasca Jul 25, 2024

AntoineChambert-Loir Jul 25, 2024

AntoineChambert-Loir Jul 25, 2024

riccardobrasca commented Jul 26, 2024

mathlib-bors bot commented Jul 26, 2024

riccardobrasca commented Jul 26, 2024

mathlib-bors bot commented Jul 26, 2024

AntoineChambert-Loir commented Jul 26, 2024

mathlib-bors bot commented Jul 26, 2024

[Merged by Bors] - feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann) #13047

[Merged by Bors] - feat(GroupTheory): covering a group by cosets (Lemma of B. H. Neumann) #13047

Conversation

AntoineChambert-Loir commented May 20, 2024 • edited by bustercopley Loading

github-actions bot commented Jun 21, 2024 • edited Loading

PR summary c455742c01

Import changes for modified files

Declarations diff

jcommelin left a comment

Choose a reason for hiding this comment

faenuccio commented Jul 9, 2024

riccardobrasca Jul 25, 2024

Choose a reason for hiding this comment

AntoineChambert-Loir Jul 25, 2024

Choose a reason for hiding this comment

riccardobrasca Jul 25, 2024

Choose a reason for hiding this comment

AntoineChambert-Loir Jul 25, 2024

Choose a reason for hiding this comment

AntoineChambert-Loir Jul 25, 2024

Choose a reason for hiding this comment

riccardobrasca commented Jul 26, 2024

mathlib-bors bot commented Jul 26, 2024

riccardobrasca commented Jul 26, 2024

mathlib-bors bot commented Jul 26, 2024

AntoineChambert-Loir commented Jul 26, 2024

mathlib-bors bot commented Jul 26, 2024

AntoineChambert-Loir commented May 20, 2024 •

edited by bustercopley

Loading

github-actions bot commented Jun 21, 2024 •

edited

Loading