Skip to content

[Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): order iso between blocks and subgroups#13995

Closed
AntoineChambert-Loir wants to merge 4 commits intomasterfrom
ACL/IwBlocks_Equiv2
Closed

[Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): order iso between blocks and subgroups#13995
AntoineChambert-Loir wants to merge 4 commits intomasterfrom
ACL/IwBlocks_Equiv2

Conversation

@AntoineChambert-Loir
Copy link
Copy Markdown
Collaborator

@AntoineChambert-Loir AntoineChambert-Loir commented Jun 20, 2024

This PR proves the order isomorphism between blocks containing a point and subgroups containing its stabilizer.

This is a new branch to correct the bad merge of #12050
Open in Gitpod

@AntoineChambert-Loir AntoineChambert-Loir mentioned this pull request Jun 20, 2024
Closed
2 tasks
@github-actions
Copy link
Copy Markdown

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

PR summary e4c484914c

Import changes

No significant changes to the import graph

Declarations diff

+ IsBlock.of_orbit
+ IsBlock.orbit_stabilizer_eq
+ IsBlock.stabilizer_le
+ block_stabilizerOrderIso
+ stabilizer_orbit_eq

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

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

This was referenced Jun 20, 2024
Closed
Closed
Closed
Closed
tb65536
tb65536 reviewed Jun 25, 2024
View reviewed changes
@AntoineChambert-Loir @tb65536
Update Mathlib/GroupTheory/GroupAction/Blocks.lean
c6ce67a 
Co-authored-by: Thomas Browning <tb65536@users.noreply.github.com>
tb65536
tb65536 reviewed Jun 25, 2024
View reviewed changes
tb65536
tb65536 reviewed Jun 25, 2024
View reviewed changes
tb65536
tb65536 approved these changes Jul 1, 2024
View reviewed changes
Mathlib/GroupTheory/GroupAction/Blocks.lean
right_inv := fun ⟨H, hH⟩ =>
(id (propext Subtype.mk_eq_mk)).mpr (stabilizer_orbit_eq hH)
map_rel_iff' := by
rintro ⟨B, ha, hB⟩; rintro ⟨B', ha', hB'⟩
Copy link
Copy Markdown
Contributor

@tb65536 tb65536 Jul 1, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does this work?

Suggested change
rintro ⟨B, ha, hB⟩; rintro ⟨B', ha', hB'⟩
rintro ⟨B, ha, hB⟩ ⟨B', ha', hB'⟩

jcommelin
jcommelin reviewed Jul 5, 2024
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@ghost ghost added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jul 5, 2024
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 5, 2024

✌️ 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
Copy link
Copy Markdown
Collaborator Author

AntoineChambert-Loir commented Jul 11, 2024

bors r+

mathlib-bors bot pushed a commit that referenced this pull request Jul 11, 2024
@AntoineChambert-Loir
feat(GroupTheory/GroupAction/Blocks): order iso between blocks and su…
34c81a7 
…bgroups (#13995)

This PR proves the order isomorphism between blocks containing a point and subgroups containing its stabilizer.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 11, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(GroupTheory/GroupAction/Blocks): order iso between blocks and subgroups [Merged by Bors] - feat(GroupTheory/GroupAction/Blocks): order iso between blocks and subgroups Jul 11, 2024
@mathlib-bors mathlib-bors bot closed this Jul 11, 2024
@mathlib-bors mathlib-bors bot deleted the ACL/IwBlocks_Equiv2 branch July 11, 2024 11:09
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin left review comments

@tb65536 tb65536 tb65536 approved these changes

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer).

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@AntoineChambert-Loir @jcommelin @tb65536