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

[Merged by Bors] - feat(group_theory/group_action/support): Support under an action #17055

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - feat(group_theory/group_action/support): Support under an action #17055

wants to merge 5 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies commented Oct 18, 2022 •
edited
Loading

Given an action of a group G on a type α, we say that a set s : set α supports an element a : α if, for all g, g fixes a if g fixes s pointwise.

From Con(NF)

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR t-algebra Algebra (groups, rings, fields etc) labels Oct 18, 2022
YaelDillies
YaelDillies commented Oct 18, 2022
View reviewed changes
src/group_theory/group_action/support.lean
[smul_comm_class G H β] [smul_comm_class G H α] {s t : set α} {b : β}

-- TODO: This should work without `smul_comm_class`
@[to_additive] lemma supports.smul (g : H) (h : supports G s b) : supports G (g • s) (g • b) :=
Copy link
Collaborator Author

Choose a reason for hiding this comment

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

This is the one lemma I care about and I can't afford smul_comm_class there. Thoughts? I can afford is_scalar_tower instead.

Copy link
Member

Choose a reason for hiding this comment

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

Can you explain the context you want this to hold in?

Copy link
Collaborator Author

@YaelDillies YaelDillies Oct 20, 2022 •
edited
Loading

Choose a reason for hiding this comment

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

The context is complicated, but the gist of it is that we have a subgroup of perm X acting on a decorated version of set X, and we can get everything down to perm X acting on set X if needed. The full story is here for the Lean code and there for the blueprint.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I tried a few things and couldn't find an obvious set of hypotheses that would make this true. If you assume is_scalar_tower, would that involve has_smul G H or has_smul H G (or both?)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Both IIRC

Copy link
Collaborator

Choose a reason for hiding this comment

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

I did a bit more experimenting and couldn't find any way to prove this without assuming smul_comm. Do you want to go ahead and PR this version, then later figure out a lemma that works for your usecase?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yeah, I see no point in waiting. The definition won't change.

@Vierkantor Vierkantor self-assigned this Dec 9, 2022
Vierkantor
Vierkantor reviewed Dec 13, 2022
View reviewed changes
src/group_theory/group_action/support.lean Outdated Show resolved Hide resolved
src/group_theory/group_action/support.lean Outdated Show resolved Hide resolved
src/group_theory/group_action/support.lean Show resolved Hide resolved
src/group_theory/group_action/support.lean
[smul_comm_class G H β] [smul_comm_class G H α] {s t : set α} {b : β}

-- TODO: This should work without `smul_comm_class`
@[to_additive] lemma supports.smul (g : H) (h : supports G s b) : supports G (g • s) (g • b) :=
Copy link
Collaborator

Choose a reason for hiding this comment

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

I tried a few things and couldn't find an obvious set of hypotheses that would make this true. If you assume is_scalar_tower, would that involve has_smul G H or has_smul H G (or both?)

@Vierkantor Vierkantor added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Dec 13, 2022
@YaelDillies @Vierkantor
better docstrings
aa7888c 
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 7, 2023
Vierkantor
Vierkantor approved these changes Jan 11, 2023
View reviewed changes
Copy link
Collaborator

@Vierkantor Vierkantor 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+

@bors
Copy link

bors bot commented Jan 11, 2023

✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Jan 11, 2023
@YaelDillies
Copy link
Collaborator Author

Generalisation later, hopefully. At least, the definition is stable.

bors merge

bors bot pushed a commit that referenced this pull request Jan 11, 2023
@YaelDillies
feat(group_theory/group_action/support): Support under an action (#17055
ffd020d 
)

Given an action of a group `G` on a type `α`, we say that a set `s : set α ` **supports** an element `a : α` if, for all `g`, `g` fixes `a` if `g` fixes `s` pointwise.
@bors
Copy link

bors bot commented Jan 11, 2023

Build failed (retrying...):

bors bot pushed a commit that referenced this pull request Jan 11, 2023
@YaelDillies
feat(group_theory/group_action/support): Support under an action (#17055
3cdfe10 
)

Given an action of a group `G` on a type `α`, we say that a set `s : set α ` **supports** an element `a : α` if, for all `g`, `g` fixes `a` if `g` fixes `s` pointwise.
@bors
Copy link

bors bot commented Jan 11, 2023

Build failed:

@YaelDillies
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Jan 12, 2023
@YaelDillies
feat(group_theory/group_action/support): Support under an action (#17055
36a3521 
)

Given an action of a group `G` on a type `α`, we say that a set `s : set α ` **supports** an element `a : α` if, for all `g`, `g` fixes `a` if `g` fixes `s` pointwise.
@bors
Copy link

bors bot commented Jan 12, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(group_theory/group_action/support): Support under an action [Merged by Bors] - feat(group_theory/group_action/support): Support under an action Jan 12, 2023
@bors bors bot closed this Jan 12, 2023
@bors bors bot deleted the mul_action_support branch January 12, 2023 02:58
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@Vierkantor Vierkantor Vierkantor approved these changes

Assignees

@Vierkantor Vierkantor

Labels
delegated The PR author may merge after reviewing final suggestions. t-algebra Algebra (groups, rings, fields etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@YaelDillies @eric-wieser @Vierkantor @leanprover-community-bot-assistant