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/direct_sum): graded algebras #8783

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat(algebra/direct_sum): graded algebras #8783

wants to merge 15 commits into from

Conversation

eric-wieser
Copy link
Member

@eric-wieser eric-wieser commented Aug 20, 2021 •
edited

This provides a direct_sum.galgebra structure on top of the existing direct_sum.gmonoid structure.
This typeclass is used to provide an algebra R (⨁ i, A i) instance.

This also renames and improves the stateement of direct_sum.module.ext to direct_sum.linear_map_ext and adds direect_sum.ring_hom_ext and direct_sum.alg_hom_ext to match.

Open in Gitpod

@eric-wieser eric-wieser added the WIP Work in progress label Aug 20, 2021
@jcommelin
Copy link
Member

A couple of months ago @kbuzzard and you played with this a lot. So I'm pinging Kevin here. I think he had some ideas in the end about how to set things up.

@eric-wieser
Copy link
Member Author

eric-wieser commented Aug 21, 2021 •
edited

I think the stuff Kevin and I were talking about was mainly how to actually work with the ring structure on direct_sum in a convenient way, specifically when the summands are submodules.

This doesn't attempt to answer that question, and simply extends the existing logic for semirings to algebras too.

That said, I'm on vacation for the next week anyway, and this is probably of interest to Kevin even if it's not the same as what we looked at before.

kbuzzard
kbuzzard approved these changes Aug 25, 2021
View reviewed changes
Copy link
Member

@kbuzzard kbuzzard left a comment

Choose a reason for hiding this comment

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

Developing the theory of Proj of a graded ring will be a good test for this stuff.

src/algebra/direct_sum_graded_algebra.lean Outdated Show resolved Hide resolved
src/algebra/direct_sum_graded_algebra.lean Outdated Show resolved Hide resolved
src/algebra/direct_sum_graded_algebra.lean Outdated Show resolved Hide resolved
src/algebra/direct_sum_graded_algebra.lean Outdated
(carriers : ι → submodule R B)
(one_mem : (1 : B) ∈ carriers 0)
(mul_mem : ∀ ⦃i j⦄ (gi : carriers i) (gj : carriers j), (gi * gj : B) ∈ carriers (i + j)) :
by haveI : gmonoid (λ i, carriers i) := gmonoid.of_submodules carriers one_mem mul_mem; exact
Copy link
Member

Choose a reason for hiding this comment

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

Should this be a letI? If so, I'm slightly surprised that haveI didn't give you problems later on.

Copy link
Member Author

Choose a reason for hiding this comment

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

The nice thing about haveI is that it ends up inlined into the arguments rather than producing a let expression; so haveI is surprisingly the better choice here!

src/algebra/direct_sum_graded_algebra.lean Outdated Show resolved Hide resolved
@eric-wieser eric-wieser added awaiting-author A reviewer has asked the author a question or requested changes and removed WIP Work in progress labels Aug 26, 2021
@eric-wieser eric-wieser 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 Aug 28, 2021
eric-wieser
eric-wieser commented Aug 28, 2021
View reviewed changes
Copy link
Member Author

@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 the docstring @kbuzzard; I've updated with a algebra.direct_sum_galgebra instance so as to show that add_monoid_algebra A ι ≃ₐ[R] ⨁ i : ι, A

@eric-wieser eric-wieser force-pushed the eric-wieser/direct_sum_graded.algebra branch from 733b58a to 95c26db Compare August 29, 2021 12:52
@eric-wieser eric-wieser force-pushed the eric-wieser/direct_sum_graded.algebra branch from 95c26db to 5558fe8 Compare August 29, 2021 12:56
@eric-wieser eric-wieser mentioned this pull request Aug 29, 2021
Open
2 tasks
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 29, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Aug 30, 2021
@eric-wieser
Copy link
Member Author

Oops, hadn't noticed this had trivial conflicts

jcommelin
jcommelin approved these changes Aug 30, 2021
View reviewed changes
Copy link
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.

Thanks 🎉

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Aug 30, 2021
bors bot pushed a commit that referenced this pull request Aug 30, 2021
@eric-wieser
feat(algebra/direct_sum): graded algebras (#8783)
cc360db 
This provides a `direct_sum.galgebra` structure on top of the existing `direct_sum.gmonoid` structure.
This typeclass is used to provide an `algebra R (⨁ i, A i)` instance.

This also renames and improves the stateement of `direct_sum.module.ext` to `direct_sum.linear_map_ext` and adds `direect_sum.ring_hom_ext` and `direct_sum.alg_hom_ext` to match.
@github-actions github-actions bot removed the awaiting-review The author would like community review of the PR label Aug 30, 2021
@bors
Copy link

bors bot commented Aug 30, 2021

Build failed:

@eric-wieser
Copy link
Member Author

bors r+

1 similar comment
@eric-wieser
Copy link
Member Author

bors r+

bors bot pushed a commit that referenced this pull request Aug 30, 2021
@eric-wieser
feat(algebra/direct_sum): graded algebras (#8783)
98466d2 
This provides a `direct_sum.galgebra` structure on top of the existing `direct_sum.gmonoid` structure.
This typeclass is used to provide an `algebra R (⨁ i, A i)` instance.

This also renames and improves the stateement of `direct_sum.module.ext` to `direct_sum.linear_map_ext` and adds `direect_sum.ring_hom_ext` and `direct_sum.alg_hom_ext` to match.
@bors
Copy link

bors bot commented Aug 30, 2021

Already running a review

@bors
Copy link

bors bot commented Aug 30, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(algebra/direct_sum): graded algebras [Merged by Bors] - feat(algebra/direct_sum): graded algebras Aug 30, 2021
@bors bors bot closed this Aug 30, 2021
@bors bors bot deleted the eric-wieser/direct_sum_graded.algebra branch August 30, 2021 14:05
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

@kbuzzard kbuzzard kbuzzard approved these changes

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
Graded modules, rings, and algebras
  
Done
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

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