[Merged by Bors] - feat(Algebra/DirectSum): getting a map between directsums by giving the map on components by xyzw12345 · Pull Request #22354 · leanprover-community/mathlib4

xyzw12345 · 2025-02-27T04:47:12Z

This PR defines the map obtained between DirectSums by giving the component-wise mapping. More specifically, it creates a homomorphism DirectSum.map f : (⨁ i, α i) →+ ⨁ i, β i from the component-wise map f : ∀(i : ι), α i →+ β i. We also proved some basic properties of this function. This construction is expected to be used in things related to graded rings.

The linear version of this map was added already in #20265.

#22279 depends on this PR.

github-actions · 2025-02-27T04:48:08Z

PR summary 28256e0bfc

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

Declarations diff

+ lmap_comp
+ lmap_eq_iff
+ lmap_eq_map
+ lmap_id
+ lmap_of
+ lmap_surjective
+ map
+ mapRange_surjective
+ map_apply
+ map_comp
+ map_eq_iff
+ map_id
+ map_injective
+ map_of
+ map_surjective
+ toAddMonoidHom_lmap

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

Mathlib/Algebra/DirectSum/Basic.lean

j-loreaux

Thanks! There are a few minor issues described below. Mainly just showing you the way we do things in Mathlib.

Mathlib/Algebra/DirectSum/Basic.lean

xyzw12345 · 2025-03-01T12:05:29Z

I've updated the linearMap version by now, and the definitions are renamed similarly to those appearing in DFinsupp section (so that it's probably easier to find?).

Mathlib/Algebra/DirectSum/Basic.lean

eric-wieser · 2025-03-01T12:36:43Z

and the definitions are renamed similarly to those appearing in DFinsupp section (so that it's probably easier to find?).

I think map is a better name; one of the key differences between DFinsupp and DirectSum is the deliberate choice to use different terminology (eg of vs single).

Perhaps map and lmap would be reasonable names?

xyzw12345 · 2025-03-01T12:37:14Z

OK, that makes sense as well.

Edit: I found that DirectSum.lmap actually existed in mathlib, so I just tried to imitate what is done there and added DFinsupp.mapRange_surjective as a iff version (following DFinsupp.mapRange_injective).

Mathlib/Algebra/DirectSum/Module.lean

Co-authored-by: Eric Wieser <efw@google.com>

j-loreaux

I'm happy with this now @eric-wieser, but I'll let you decide:

bors d=eric-wieser

mathlib-bors · 2025-03-02T21:44:50Z

✌️ 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.

Mathlib/Algebra/DirectSum/Module.lean

eric-wieser

bors d+

One very minor nit

mathlib-bors · 2025-03-04T14:19:39Z

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

xyzw12345 · 2025-03-05T02:59:04Z

bors r+

…he map on components (#22354) This PR defines the map obtained between `DirectSum`s by giving the component-wise mapping. More specifically, it creates a homomorphism `DirectSum.map f : (⨁ i, α i) →+ ⨁ i, β i` from the component-wise map `f : ∀(i : ι), α i →+ β i`. We also proved some basic properties of this function. This construction is expected to be used in things related to graded rings. The linear version of this map was added already in #20265. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

mathlib-bors · 2025-03-05T03:37:59Z

Pull request successfully merged into master.

Build succeeded:

…he map on components (#22354) This PR defines the map obtained between `DirectSum`s by giving the component-wise mapping. More specifically, it creates a homomorphism `DirectSum.map f : (⨁ i, α i) →+ ⨁ i, β i` from the component-wise map `f : ∀(i : ι), α i →+ β i`. We also proved some basic properties of this function. This construction is expected to be used in things related to graded rings. The linear version of this map was added already in #20265. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Update Basic.lean

8552730

github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Feb 27, 2025

github-actions bot added the t-algebra Algebra (groups, rings, fields, etc) label Feb 27, 2025

xyzw12345 mentioned this pull request Feb 27, 2025

feat(RingTheory/GradedAlgebra): homogeneous relation #22279

Closed

1 task

Paul-Lez self-requested a review February 27, 2025 11:24

eric-wieser reviewed Feb 27, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Basic.lean Outdated Show resolved Hide resolved

j-loreaux reviewed Feb 28, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/DirectSum/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/DirectSum/Basic.lean Outdated Show resolved Hide resolved

Mathlib/Algebra/DirectSum/Basic.lean Outdated Show resolved Hide resolved

j-loreaux added the awaiting-author A reviewer has asked the author a question or requested changes. label Feb 28, 2025

xyzw12345 added 2 commits March 1, 2025 19:41

update according to review comments

b1071d2

update linearMap version

8c15861

xyzw12345 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 1, 2025

golf

85d3857

eric-wieser reviewed Mar 1, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Basic.lean Outdated Show resolved Hide resolved

eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 1, 2025

xyzw12345 added 2 commits March 2, 2025 15:00

add new lemma

24aad9d

Update Module.lean

b895de4

xyzw12345 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Mar 2, 2025

xyzw12345 requested a review from eric-wieser March 2, 2025 10:35

eric-wieser reviewed Mar 2, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Module.lean Outdated Show resolved Hide resolved

xyzw12345 and others added 4 commits March 2, 2025 19:38

Update Mathlib/Algebra/DirectSum/Module.lean

badf4d5

Co-authored-by: Eric Wieser <efw@google.com>

golf

c403f2d

fix proof

cbea8ff

add back lmap_eq_map to match lof_eq_of

5decd70

j-loreaux reviewed Mar 2, 2025

View reviewed changes

ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 2, 2025

xyzw12345 requested a review from eric-wieser March 4, 2025 13:44

eric-wieser reviewed Mar 4, 2025

View reviewed changes

Mathlib/Algebra/DirectSum/Module.lean Outdated Show resolved Hide resolved

eric-wieser approved these changes Mar 4, 2025

View reviewed changes

Update Module.lean

28256e0

mathlib-bors bot changed the title ~~feat(Algebra/DirectSum): getting a map between directsums by giving the map on components~~ [Merged by Bors] - feat(Algebra/DirectSum): getting a map between directsums by giving the map on components Mar 5, 2025

mathlib-bors bot closed this Mar 5, 2025

mathlib-bors bot deleted the xyzw12345_DirectSum branch March 5, 2025 03:38

xyzw12345 mentioned this pull request Jul 20, 2025

feat(RingTheory/GradedAlgebra): homogeneous relation #27307

Open

Conversation

xyzw12345 commented Feb 27, 2025 • edited by eric-wieser Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Feb 27, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary 28256e0bfc

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

xyzw12345 commented Mar 1, 2025

Uh oh!

Uh oh!

eric-wieser commented Mar 1, 2025

Uh oh!

xyzw12345 commented Mar 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

j-loreaux left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 2, 2025

Uh oh!

Uh oh!

eric-wieser left a comment

Choose a reason for hiding this comment

Uh oh!

mathlib-bors bot commented Mar 4, 2025

Uh oh!

xyzw12345 commented Mar 5, 2025

Uh oh!

mathlib-bors bot commented Mar 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

xyzw12345 commented Feb 27, 2025 •

edited by eric-wieser

Loading

github-actions bot commented Feb 27, 2025 •

edited

Loading

xyzw12345 commented Mar 1, 2025 •

edited

Loading