Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

feat(GroupTheory/GroupAction/Primitive) #12052

Open
wants to merge 148 commits into
base: master
Choose a base branch
from
Open

feat(GroupTheory/GroupAction/Primitive) #12052

wants to merge 148 commits into from
+727 −14

Conversation

AntoineChambert-Loir
Copy link
Collaborator

@AntoineChambert-Loir AntoineChambert-Loir commented Apr 10, 2024 •
edited
Loading

This PR defines the notion of a primitive action.

This concept is used to state the Iwasawa criterion for simplicity of #12048

Open in Gitpod

AntoineChambert-Loir and others added 30 commits April 6, 2024 01:04
@AntoineChambert-Loir
blocks of group actions
f2b4301
@AntoineChambert-Loir
Merge branch 'ACL/IwBlocks' into ACL/IwPrimitive
cf64231 
Second branch towards the iwasawa criterion
We import blocks.
@AntoineChambert-Loir
feat(Mathlib/GroupAction/Primitive): primitive actions
4590e6d
@AntoineChambert-Loir
adjust files blocks and primitive
8cf4bff
@AntoineChambert-Loir
cleanup blocks
8cdd62e
@AntoineChambert-Loir
mv pointwise to group action
85ed927
@AntoineChambert-Loir
update Mathlib.lean and a single import
5c2a690
@AntoineChambert-Loir
delete obsolete file
5fc97e4
@AntoineChambert-Loir
remove import, add docstring
0d6df8d
@AntoineChambert-Loir
adjust docstring
52b250a
@AntoineChambert-Loir
Merge branch 'ACL/IwBlocks' of https://github.com/leanprover-communit…
159414e 
…y/mathlib4 into ACL/IwBlocks
@AntoineChambert-Loir
add the pointwise file
8757c26
@AntoineChambert-Loir
cleanup blocks
e83f016
@AntoineChambert-Loir
adjust to calm linter
745ea01
@AntoineChambert-Loir
Merge branch 'ACL/IwBlocks' into ACL/IwBlocks_Equiv
82405e6
@AntoineChambert-Loir
change as suggested on Zulip
7ae244f
@AntoineChambert-Loir @github-actions
Update Mathlib/GroupTheory/GroupAction/Pointwise.lean
05bb01d 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@AntoineChambert-Loir @github-actions
Update Mathlib/GroupTheory/GroupAction/Pointwise.lean
c7bf04a 
Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>
@AntoineChambert-Loir
adjust
c956614
@AntoineChambert-Loir
adjust docstring
72043b0
@AntoineChambert-Loir
adjust docstring (lint100)
5c45358
@AntoineChambert-Loir
adjust namespace for preimage_smul_set[sl]
39609e7
@AntoineChambert-Loir
adjust Pointwise
483a13c
@AntoineChambert-Loir
Merge branch 'ACL/IwBlocks' into ACL/IwBlocks_Equiv
a7bd55e
@AntoineChambert-Loir
Merge branch 'ACL/IwBlocks' into ACL/IwBlocks_Finite
85f5ddd
@AntoineChambert-Loir
orderiso
5188ff6
@AntoineChambert-Loir
truncate Blocks.lean to basic definitions
4ae8aad
@AntoineChambert-Loir
adjust to pointwise
dc4ff20
@AntoineChambert-Loir
Merge branch 'ACL/IwBlocks_Equiv' into ACL/IwBlocks_Finite
09c3c00
@AntoineChambert-Loir
adjust and simplify
6949298
@AntoineChambert-Loir AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes label Nov 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Nov 25, 2024
@AntoineChambert-Loir @leanprover-community-mathlib4-bot
feat: additivize equivariance of morphisms of actions (#19171)
beb3168 
Additivize the definition of equivariant morphisms with respect to multiplicative actions.
The notation introduced is `X →ₑᵥ[φ] Y` for equivariant morphisms, and `X →ᵥ[M] Y` when the
underlying map is identity.

The goal is to be able to fully additivize the properties of blocks for actions and the definition
of primitive actions in #12052 



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Nov 25, 2024
@mathlib4-dependent-issues-bot
Copy link
Collaborator

mathlib4-dependent-issues-bot commented Nov 25, 2024 •
edited
Loading

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 25, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 25, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 28, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 30, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 2, 2024
@leanprover-community-bot-assistant leanprover-community-bot-assistant removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Dec 2, 2024
@YaelDillies
Copy link
Collaborator

Sorry for the delay reviewing. This PR is quite big and I am failing to justify why. Could you split it along something like

  1. Instance renaming
  2. Missing to_additive
  3. Maximal subgroups
  4. Primitive actions (stay in this PR, depend on 2 and 3)

@YaelDillies YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes label Jan 4, 2025
@AntoineChambert-Loir
Copy link
Collaborator Author

I cancelled step 1. (Master does this better.)

@AntoineChambert-Loir
Copy link
Collaborator Author

Step 2 is #20498

@AntoineChambert-Loir
Copy link
Collaborator Author

Step 3 is #20499

@AntoineChambert-Loir AntoineChambert-Loir removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 5, 2025
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jan 5, 2025
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 6, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@github-actions github-actions[bot] github-actions[bot] left review comments

@alreadydone alreadydone alreadydone left review comments

@urkud urkud urkud left review comments

Assignees

@faenuccio faenuccio

Labels
blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) t-algebra Algebra (groups, rings, fields, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
10 participants
@AntoineChambert-Loir @kim-em @tb65536 @mathlib4-dependent-issues-bot @YaelDillies @urkud @alreadydone @faenuccio @leanprover-community-bot-assistant @leanprover-community-mathlib4-bot