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(algebra/lie/basic): generalise the definition of lie_algebra.derived_series #5794

Closed
wants to merge 7 commits into from
Closed

[Merged by Bors] - feat(algebra/lie/basic): generalise the definition of lie_algebra.derived_series #5794

wants to merge 7 commits into from

Conversation

ocfnash
Copy link
Collaborator

@ocfnash ocfnash commented Jan 18, 2021 •
edited

This generalisation will make it easier to relate properties of the derived
series of a Lie algebra and the derived series of its ideals (regarded as Lie
algebras in their own right).

The key definition is lie_algebra.derived_series_of_ideal and the key result is lie_ideal.derived_series_eq_bot_iff.

@github-actions github-actions bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 18, 2021
@ocfnash ocfnash added WIP Work in progress blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Jan 18, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 18, 2021
@ocfnash ocfnash mentioned this pull request Jan 18, 2021
Closed
@github-actions github-actions bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Jan 18, 2021
@ocfnash ocfnash force-pushed the lie_derived_series_generalise branch from a6bce33 to 8c927b3 Compare January 18, 2021 14:38
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Jan 18, 2021
@ocfnash
feat(algebra/lie/basic): generalise the definition of `lie_algebra.de…
240c7b5 
…rived_series`

This generalisation will make it easier to relate properties of the derived
series of a Lie algebra and the derived series of its ideals (regarded as Lie
algebras in their own right).
@ocfnash
Implement remainder of @eric-wieser's suggestions from #5778
57cb8ca 
These suggestions were added after the referenced PR was already in
the queue for bors so they are being implemented here instead.
@ocfnash ocfnash force-pushed the lie_derived_series_generalise branch from 3e99dae to 57cb8ca Compare January 18, 2021 15:09
@ocfnash ocfnash added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Jan 18, 2021
eric-wieser
eric-wieser reviewed Jan 18, 2021
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

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

Thanks for following up on my comments from the previous PR, all those changes look good. I don't know enough about lie algebras to comment on the actual content of the PR :)

@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Jan 19, 2021
bors bot pushed a commit that referenced this pull request Jan 19, 2021
@ocfnash
feat(algebra/lie/basic): generalise the definition of `lie_algebra.de…
90763c4 
…rived_series` (#5794)

This generalisation will make it easier to relate properties of the derived
series of a Lie algebra and the derived series of its ideals (regarded as Lie
algebras in their own right).

The key definition is `lie_algebra.derived_series_of_ideal` and the key result is `lie_ideal.derived_series_eq_bot_iff`.
@bors
Copy link

bors bot commented Jan 19, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/lie/basic): generalise the definition of lie_algebra.derived_series [Merged by Bors] - feat(algebra/lie/basic): generalise the definition of lie_algebra.derived_series Jan 19, 2021
@bors bors bot closed this Jan 19, 2021
@bors bors bot deleted the lie_derived_series_generalise branch January 19, 2021 16:30
This was referenced Jan 27, 2021
Closed
Closed
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

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@ocfnash @jcommelin @eric-wieser