[Merged by Bors] - feat(algebra/direct_sum/decomposition): add decompositions into a direct sum #14626

eric-wieser · 2022-06-08T17:13:51Z

This is a constructive version of direct_sum.is_internal, and generalizes the existing graded_algebra.

The main user-facing changes are:

graded_algebra.decompose is now spelt direct_sum.decompose_alg_hom
The simp normal form of decomposition is now direct_sum.decompose.
graded_algebra.support 𝒜 x is now spelt (decompose 𝒜 x).support
left_inv and right_inv has swapped, now with meaning "the decomposition is the (left|right) inverse of the canonical map" rather than the other way around

To keep this from growing even larger, I've left graded_algebra.proj alone for a future refactor.

This replaces

feat(linear_algebra/decomposition): Define module decompositions and prove basic facts #8246

…ect sum This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`.

jjaassoonn · 2022-06-09T13:39:08Z

May be we should also define direct_sum.decomposition.support so that we don't need to write support twice for graded algebra and graded module

eric-wieser · 2022-06-09T14:21:29Z

I don't think there's much point in having direct_sum.decomposition.support x given it's longer than (direct_sum.decompose x).support which we already have. If we're going to have it, it needs a shorter name

jjaassoonn · 2022-06-09T15:24:12Z

I don't think there's much point in having direct_sum.decomposition.support x given it's longer than (direct_sum.decompose x).support which we already have. If we're going to have it, it needs a shorter name

In graded algebra, there are several lemmas about writing an element as sum of its projections. Same lemma applies to graded modules as well. So I think it makes sense to move these lemmas to direct_sum.decomposition where possible.

eric-wieser · 2022-06-09T16:05:44Z

given it's longer than (direct_sum.decompose x).support which we already have.

Hmm, this doesn't actually elaborate though.

eric-wieser · 2022-06-09T16:15:51Z

I've ended up just removing graded_algebra.support, and added an instance to resolve the elaboration issue.

src/algebra/direct_sum/decomposition.lean

src/algebra/monoid_algebra/grading.lean

Vierkantor

The technical aspects look good, any mathematical objections?

bors d=@jjaassoonn

bors · 2022-06-16T08:33:36Z

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

jjaassoonn · 2022-06-16T12:13:35Z

bors r+

jjaassoonn · 2022-06-16T12:16:10Z

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

bors r+

bors · 2022-06-16T12:16:11Z

Already running a review

…ect sum (#14626) This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`. The main user-facing changes are: * `graded_algebra.decompose` is now spelt `direct_sum.decompose_alg_hom` * The simp normal form of decomposition is now `direct_sum.decompose`. * `graded_algebra.support 𝒜 x` is now spelt `(decompose 𝒜 x).support` * `left_inv` and `right_inv` has swapped, now with meaning "the decomposition is the (left|right) inverse of the canonical map" rather than the other way around To keep this from growing even larger, I've left `graded_algebra.proj` alone for a future refactor. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

bors · 2022-06-16T12:52:00Z

Build failed (retrying...):

Run tests

…sum.decomposition

bors · 2022-06-16T12:59:18Z

Canceled.

Vierkantor · 2022-06-16T13:49:58Z

I don't think the failing test is your fault so:

bors r+

bors d+

bors · 2022-06-16T13:49:59Z

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

…ect sum (#14626) This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`. The main user-facing changes are: * `graded_algebra.decompose` is now spelt `direct_sum.decompose_alg_hom` * The simp normal form of decomposition is now `direct_sum.decompose`. * `graded_algebra.support 𝒜 x` is now spelt `(decompose 𝒜 x).support` * `left_inv` and `right_inv` has swapped, now with meaning "the decomposition is the (left|right) inverse of the canonical map" rather than the other way around To keep this from growing even larger, I've left `graded_algebra.proj` alone for a future refactor. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

bors · 2022-06-16T15:37:43Z

Canceled.

eric-wieser · 2022-06-16T15:51:35Z

Oh damn, I assumed the failing test was my fault so pushed a commit to speed up the slow proof

eric-wieser · 2022-06-16T15:52:06Z

bors r+

(since the test passes)

…ect sum (#14626) This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`. The main user-facing changes are: * `graded_algebra.decompose` is now spelt `direct_sum.decompose_alg_hom` * The simp normal form of decomposition is now `direct_sum.decompose`. * `graded_algebra.support 𝒜 x` is now spelt `(decompose 𝒜 x).support` * `left_inv` and `right_inv` has swapped, now with meaning "the decomposition is the (left|right) inverse of the canonical map" rather than the other way around To keep this from growing even larger, I've left `graded_algebra.proj` alone for a future refactor. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

bors · 2022-06-16T19:15:27Z

This PR was included in a batch that was canceled, it will be automatically retried

…ect sum (#14626) This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`. The main user-facing changes are: * `graded_algebra.decompose` is now spelt `direct_sum.decompose_alg_hom` * The simp normal form of decomposition is now `direct_sum.decompose`. * `graded_algebra.support 𝒜 x` is now spelt `(decompose 𝒜 x).support` * `left_inv` and `right_inv` has swapped, now with meaning "the decomposition is the (left|right) inverse of the canonical map" rather than the other way around To keep this from growing even larger, I've left `graded_algebra.proj` alone for a future refactor. Co-authored-by: Jujian Zhang <jujian.zhang1998@outlook.com>

bors · 2022-06-16T21:15:50Z

Pull request successfully merged into master.

Build succeeded:

@eric-wieser

By imitating the current `graded_algebra`, this pr builds `graded_module` over some `graded algebra` Co-authored-by: Eric Wieser @eric-wieser - [x] depends on: #14626 - [x] depends on: #15654 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

feat(algebra/direct_sum/decomposition): add decompositions into a dir…

b6f2bc9

…ect sum This is a constructive version of `direct_sum.is_internal`, and generalizes the existing `graded_algebra`.

eric-wieser requested a review from jjaassoonn June 8, 2022 17:13

eric-wieser added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels Jun 8, 2022

eric-wieser added this to In progress in Graded modules, rings, and algebras via automation Jun 8, 2022

This was referenced Jun 8, 2022

[Merged by Bors] - refactor(ring_theory/graded_algebra): use add_submonoid_class to generalize to graded rings #14583

Closed

[Merged by Bors] - feat(algebra/module/graded_module): define graded module #14582

Closed

fix

ba0c574

eric-wieser force-pushed the eric-wieser/direct_sum.decomposition branch from 99a374c to ba0c574 Compare June 8, 2022 17:27

eric-wieser added 2 commits June 8, 2022 18:15

lintfix

0af1d71

fix test

15a6372

github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label Jun 8, 2022

remove graded_algebra.support

1b9bc96

eric-wieser added 3 commits June 9, 2022 18:56

Fix lemma names

ebe4954

Fix

4f5d570

Fix build errors

82f500a

eric-wieser force-pushed the eric-wieser/direct_sum.decomposition branch from 3379dee to 82f500a Compare June 9, 2022 22:03

fix

4736ecb

eric-wieser requested a review from Vierkantor June 13, 2022 11:54

golf

450579d

Vierkantor reviewed Jun 15, 2022

View reviewed changes

src/algebra/direct_sum/decomposition.lean Outdated Show resolved Hide resolved

src/algebra/direct_sum/decomposition.lean Outdated Show resolved Hide resolved

src/algebra/direct_sum/decomposition.lean Show resolved Hide resolved

src/algebra/monoid_algebra/grading.lean Show resolved Hide resolved

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 Jun 15, 2022

expand docstring

7016b08

eric-wieser force-pushed the eric-wieser/direct_sum.decomposition branch from 310cf6e to 7016b08 Compare June 15, 2022 13:05

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 Jun 15, 2022

Vierkantor approved these changes Jun 16, 2022

View reviewed changes

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 Jun 16, 2022

Merge remote-tracking branch 'origin/master' into eric-wieser/direct_…

43486b8

…sum.decomposition

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 Jun 16, 2022

fix timeout and golf

fe0c699

bors bot changed the title ~~feat(algebra/direct_sum/decomposition): add decompositions into a direct sum~~ [Merged by Bors] - feat(algebra/direct_sum/decomposition): add decompositions into a direct sum Jun 16, 2022

bors bot closed this Jun 16, 2022

Graded modules, rings, and algebras automation moved this from In progress to Done Jun 16, 2022

bors bot deleted the eric-wieser/direct_sum.decomposition branch June 16, 2022 21:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(algebra/direct_sum/decomposition): add decompositions into a direct sum #14626

[Merged by Bors] - feat(algebra/direct_sum/decomposition): add decompositions into a direct sum #14626

eric-wieser commented Jun 8, 2022 •

edited

jjaassoonn commented Jun 9, 2022 •

edited

eric-wieser commented Jun 9, 2022 •

edited

jjaassoonn commented Jun 9, 2022

eric-wieser commented Jun 9, 2022

eric-wieser commented Jun 9, 2022

Vierkantor left a comment

bors bot commented Jun 16, 2022

jjaassoonn commented Jun 16, 2022

jjaassoonn commented Jun 16, 2022

bors bot commented Jun 16, 2022

bors bot commented Jun 16, 2022

bors bot commented Jun 16, 2022

Vierkantor commented Jun 16, 2022

bors bot commented Jun 16, 2022

bors bot commented Jun 16, 2022

eric-wieser commented Jun 16, 2022

eric-wieser commented Jun 16, 2022

bors bot commented Jun 16, 2022

bors bot commented Jun 16, 2022

[Merged by Bors] - feat(algebra/direct_sum/decomposition): add decompositions into a direct sum #14626

[Merged by Bors] - feat(algebra/direct_sum/decomposition): add decompositions into a direct sum #14626

Conversation

eric-wieser commented Jun 8, 2022 • edited

jjaassoonn commented Jun 9, 2022 • edited

eric-wieser commented Jun 9, 2022 • edited

jjaassoonn commented Jun 9, 2022

eric-wieser commented Jun 9, 2022

eric-wieser commented Jun 9, 2022

Vierkantor left a comment

Choose a reason for hiding this comment

bors bot commented Jun 16, 2022

jjaassoonn commented Jun 16, 2022

jjaassoonn commented Jun 16, 2022

bors bot commented Jun 16, 2022

bors bot commented Jun 16, 2022

bors bot commented Jun 16, 2022

Vierkantor commented Jun 16, 2022

bors bot commented Jun 16, 2022

bors bot commented Jun 16, 2022

eric-wieser commented Jun 16, 2022

eric-wieser commented Jun 16, 2022

bors bot commented Jun 16, 2022

bors bot commented Jun 16, 2022

eric-wieser commented Jun 8, 2022 •

edited

jjaassoonn commented Jun 9, 2022 •

edited

eric-wieser commented Jun 9, 2022 •

edited