[Merged by Bors] - feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure #6053

eric-wieser · 2021-02-05T10:00:00Z

To quote the module docstring

This module provides a set of heterogenous typeclasses for defining a multiplicative structure
over ⨁ i, A i such that (*) : A i → A j → A (i + j); that is to say, A forms an
additively-graded ring. The typeclasses are:

direct_sum.ghas_one A

direct_sum.ghas_mul A

direct_sum.gmonoid A

direct_sum.gcomm_monoid A

Respectively, these imbue the direct sum ⨁ i, A i with:

has_one

mul_zero_class, distrib

semiring, ring

comm_semiring, comm_ring

Additionally, this module provides helper functions to construct gmonoid and gcomm_monoid
instances for:

A : ι → submonoid S: direct_sum.ghas_one.of_submonoids, direct_sum.ghas_mul.of_submonoids,
direct_sum.gmonoid.of_submonoids, direct_sum.gcomm_monoid.of_submonoids

A : ι → submonoid S: direct_sum.ghas_one.of_subgroups, direct_sum.ghas_mul.of_subgroups,
direct_sum.gmonoid.of_subgroups, direct_sum.gcomm_monoid.of_subgroups

If the A i are disjoint, these provide a gradation of ⨆ i, A i, and the mapping
⨁ i, A i →+ ⨆ i, A i can be obtained as
direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i).

This PR is an alternative to #5956

…ture

robertylewis

This looks reasonable but I think some of the proofs can use some golfing. I'm no expert here so I'd appreciate another review.

src/algebra/direct_sum_graded.lean

robertylewis · 2021-02-22T13:27:42Z

src/algebra/direct_sum_graded.lean

+end
+
+private lemma mul_assoc (a b c : ⨁ i, A i) : a * b * c = a * (b * c) :=
+begin


This proof looks really weird, did it come from tidy? Lots of simp onlys can be combined (and above too), same with rw/erws.

Nope, it was written by hand...

I think I found that sometimes simp only [x, y], simp only [z] would behave differently compared to simp only [x, y, z], since the former requires z to happen only after all x and y are done. I'll see if I can reduce this further though. Would you expect combining simp / erw / rw calls to speed up the proofs?

I don't think combing calls would be expected to speed up a proof at all significantly. If that were the concern, possibly simp_rw with a correctly ordered list would be superior.

But I don't think speed is what Rob was noticing here; just that it's mildly confusing to have them separate (just because a reader can look at it and think "hmm, it's strange these were done as separate tactic invocations, there must be some good reason for that" and then be left unable to guess a reason).

Something else that motivated it was to try and group together morally similar lemmas, so that the progression in tactic states looked reasonable - the depth of binders makes this proof really quite hard to keep track of.

Golfing attempts greatly appreciated, as usual!

I've replaced almost all the simp onlys with rw, and the proof is almost an order of magnitude faster.

Vierkantor

Found a few typos, otherwise looks good to me.

src/algebra/direct_sum_graded.lean

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

jcommelin · 2021-03-04T14:20:08Z

Somewhere some part of me feels a bit uneasy about the heterogeneous classes and potential DTT issues. But several eyes have now looked at this, and several brains haven't come up with a better strategy. So let's move forward and try this out.

If (not when) issues arise later, then we'll deal with them at that point.

bors merge

…ture (#6053) To quote the module docstring > This module provides a set of heterogenous typeclasses for defining a multiplicative structure > over `⨁ i, A i` such that `(*) : A i → A j → A (i + j)`; that is to say, `A` forms an > additively-graded ring. The typeclasses are: > > * `direct_sum.ghas_one A` > * `direct_sum.ghas_mul A` > * `direct_sum.gmonoid A` > * `direct_sum.gcomm_monoid A` > > Respectively, these imbue the direct sum `⨁ i, A i` with: > > * `has_one` > * `mul_zero_class`, `distrib` > * `semiring`, `ring` > * `comm_semiring`, `comm_ring` > > Additionally, this module provides helper functions to construct `gmonoid` and `gcomm_monoid` > instances for: > > * `A : ι → submonoid S`: `direct_sum.ghas_one.of_submonoids`, `direct_sum.ghas_mul.of_submonoids`, > `direct_sum.gmonoid.of_submonoids`, `direct_sum.gcomm_monoid.of_submonoids` > * `A : ι → submonoid S`: `direct_sum.ghas_one.of_subgroups`, `direct_sum.ghas_mul.of_subgroups`, > `direct_sum.gmonoid.of_subgroups`, `direct_sum.gcomm_monoid.of_subgroups` > > If the `A i` are disjoint, these provide a gradation of `⨆ i, A i`, and the mapping > `⨁ i, A i →+ ⨆ i, A i` can be obtained as > `direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i)`.

bors · 2021-03-04T16:01:46Z

Pull request successfully merged into master.

Build succeeded:

…ture (#6053) To quote the module docstring > This module provides a set of heterogenous typeclasses for defining a multiplicative structure > over `⨁ i, A i` such that `(*) : A i → A j → A (i + j)`; that is to say, `A` forms an > additively-graded ring. The typeclasses are: > > * `direct_sum.ghas_one A` > * `direct_sum.ghas_mul A` > * `direct_sum.gmonoid A` > * `direct_sum.gcomm_monoid A` > > Respectively, these imbue the direct sum `⨁ i, A i` with: > > * `has_one` > * `mul_zero_class`, `distrib` > * `semiring`, `ring` > * `comm_semiring`, `comm_ring` > > Additionally, this module provides helper functions to construct `gmonoid` and `gcomm_monoid` > instances for: > > * `A : ι → submonoid S`: `direct_sum.ghas_one.of_submonoids`, `direct_sum.ghas_mul.of_submonoids`, > `direct_sum.gmonoid.of_submonoids`, `direct_sum.gcomm_monoid.of_submonoids` > * `A : ι → submonoid S`: `direct_sum.ghas_one.of_subgroups`, `direct_sum.ghas_mul.of_subgroups`, > `direct_sum.gmonoid.of_subgroups`, `direct_sum.gcomm_monoid.of_subgroups` > > If the `A i` are disjoint, these provide a gradation of `⨆ i, A i`, and the mapping > `⨁ i, A i →+ ⨆ i, A i` can be obtained as > `direct_sum.to_monoid (λ i, add_submonoid.inclusion $ le_supr A i)`.

eric-wieser mentioned this pull request Feb 5, 2021

feat(algebra/direct_sum): put a [comm_][semi]ring structure on direct sums of add_sub{group,monoid}s #5956

Closed

eric-wieser force-pushed the direct_sum_graded branch from 340a635 to 3809e02 Compare February 5, 2021 10:02

eric-wieser added the awaiting-review The author would like community review of the PR label Feb 5, 2021

feat(algebra/direct_sum_graded): endow direct_sum with a ring struc…

565de58

…ture

eric-wieser force-pushed the direct_sum_graded branch from 3809e02 to 565de58 Compare February 5, 2021 10:17

eric-wieser mentioned this pull request Feb 5, 2021

feat(algebra/graded_algebra): Define a dependent version of add_monoid_algebra #4812

Closed

feat(*): Add submodules too

e61b0f0

robertylewis reviewed Feb 22, 2021

View reviewed changes

robertylewis 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 Feb 22, 2021

Merge remote-tracking branch 'origin/master' into direct_sum_graded

f65a92a

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 Feb 22, 2021

Golf using Mario's idea of using sigma types in the typeclasses

618c3a8

eric-wieser force-pushed the direct_sum_graded branch from 9e88c22 to 618c3a8 Compare February 22, 2021 18:06

eric-wieser added 5 commits February 22, 2021 18:13

merge erw with rw

e06fd26

Speed up two proofs by a factor of 3

7ac2ccc

Tidy up helpers

e590665

Speed up, remove now-duplicate proof

f819082

Significantly speed up the proof

3f3a74d

eric-wieser requested a review from jcommelin February 23, 2021 16:08

eric-wieser added 2 commits February 23, 2021 16:23

Add a missing bit of API

851c2f1

simps, rename

1ccd353

Vierkantor approved these changes Mar 1, 2021

View reviewed changes

src/algebra/direct_sum_graded.lean Outdated Show resolved Hide resolved

src/algebra/direct_sum_graded.lean Outdated Show resolved Hide resolved

Apply suggestions from code review

932de7f

Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

Vierkantor requested a review from robertylewis March 1, 2021 16:07

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 Mar 4, 2021

bors bot changed the title ~~feat(algebra/direct_sum_graded): endow direct_sum with a ring structure~~ [Merged by Bors] - feat(algebra/direct_sum_graded): endow direct_sum with a ring structure Mar 4, 2021

bors bot closed this Mar 4, 2021

bors bot deleted the direct_sum_graded branch March 4, 2021 16:01

eric-wieser added this to Done in Graded modules, rings, and algebras Aug 31, 2021

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure #6053

[Merged by Bors] - feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure #6053

eric-wieser commented Feb 5, 2021 •

edited

Loading

robertylewis left a comment

robertylewis Feb 22, 2021

eric-wieser Feb 22, 2021

eric-wieser Feb 22, 2021 •

edited

Loading

semorrison Feb 22, 2021

eric-wieser Feb 22, 2021

eric-wieser Feb 23, 2021

Vierkantor left a comment

jcommelin commented Mar 4, 2021

bors bot commented Mar 4, 2021

[Merged by Bors] - feat(algebra/direct_sum_graded): endow direct_sum with a ring structure #6053

[Merged by Bors] - feat(algebra/direct_sum_graded): endow direct_sum with a ring structure #6053

Conversation

eric-wieser commented Feb 5, 2021 • edited Loading

robertylewis left a comment

Choose a reason for hiding this comment

robertylewis Feb 22, 2021

Choose a reason for hiding this comment

eric-wieser Feb 22, 2021

Choose a reason for hiding this comment

eric-wieser Feb 22, 2021 • edited Loading

Choose a reason for hiding this comment

semorrison Feb 22, 2021

Choose a reason for hiding this comment

eric-wieser Feb 22, 2021

Choose a reason for hiding this comment

eric-wieser Feb 23, 2021

Choose a reason for hiding this comment

Vierkantor left a comment

Choose a reason for hiding this comment

jcommelin commented Mar 4, 2021

bors bot commented Mar 4, 2021

[Merged by Bors] - feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure #6053

[Merged by Bors] - feat(algebra/direct_sum_graded): endow `direct_sum` with a ring structure #6053

eric-wieser commented Feb 5, 2021 •

edited

Loading

eric-wieser Feb 22, 2021 •

edited

Loading