[Merged by Bors] - feat(Algebra/Pi): add various `AlgEquiv`s and `RingEquiv`s by chrisflav · Pull Request #24520 · leanprover-community/mathlib4

chrisflav · 2025-05-01T16:25:55Z

Add

RingEquiv.sumArrowEquivProdArrow: ring version of Equiv.sumArrowEquivProdArrow.
AlgEquiv.sumArrowEquivProdArrow: algebra version of Equiv.sumArrowEquivProdArrow.
AlgEquiv.piCongrLeft': algebra version of Equiv.piCongrLeft.
AlgEquiv.piCongrLeft: algebra version of Equiv.piCongrLeft.
AlgEquiv.funUnique: algebra version of Equiv.funUnique.
AlgEquiv.prodCongr: algebra version of Equiv.prodCongr.

The four last ones already have ring versions.

github-actions · 2025-05-01T16:27:12Z

PR summary 824629269a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Algebra.Pi	706	707	+1 (+0.14%)

Import changes for all files

Files	Import difference
3 files `Mathlib.Algebra.Algebra.Pi` `Mathlib.RingTheory.Localization.Away.Basic` `Mathlib.RingTheory.Localization.Pi`	1

Declarations diff

+ funUnique
+ funUnique_apply
+ funUnique_symm_apply
+ piCongrLeft
+ piCongrLeft'
+ piCongrLeft'_apply
+ piCongrLeft'_symm_apply
+ piCongrLeft_apply
+ piCongrLeft_symm_apply
+ prodCongr
+ prodCongr_apply
+ prodCongr_symm_apply
+ sumArrowEquivProdArrow_symm_apply
+ sumArrowEquivProdArrow_symm_apply_inr
++ sumArrowEquivProdArrow
++ sumArrowEquivProdArrow_apply

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/Ring/Equiv.lean

Ruben-VandeVelde · 2025-05-02T12:07:25Z

Looking at the stats, I'm afraid I'm not really convinced by the import changes here, and even less convinced that they should happen in this PR

chrisflav · 2025-05-02T14:49:09Z

Looking at the stats, I'm afraid I'm not really convinced by the import changes here, and even less convinced that they should happen in this PR

I am not sure I understand: What do you suggest? Revert the last three commits and accept the +19% import bump? Or just split this PR?

eric-wieser · 2025-05-14T00:28:22Z

My vote would be to revert the move and accept the import shuffe; the import changes shallow out pretty quickly

mistarro · 2025-05-14T06:33:31Z

So is the inconsistency with having Ring.sumArrowEquivProdArrow in Mathlib.Algebra.Ring.Equiv and Algebra.sumArrowEquivProdArrow is in Mathlib.Algebra.Algebra.Pi ok? Maybe it might be moved the other way round?

This reverts commit dce0b53.

eric-wieser · 2025-05-24T17:19:57Z

Mathlib/Algebra/Ring/Equiv.lean

+@[simp]
+lemma sumArrowEquivProdArrow_symm_apply_inl (α β) (x : (α → R) × (β → R)) (a : α) :
+    (sumArrowEquivProdArrow R α β).symm x (Sum.inl a) = x.fst a := rfl
+
+@[simp]
+lemma sumArrowEquivProdArrow_symm_apply_inr (α β) (x : (α → R) × (β → R)) (b : β) :
+    (sumArrowEquivProdArrow R α β).symm x (Sum.inr b) = x.snd b := rfl


I think these should say

Suggested change

@[simp]

lemma sumArrowEquivProdArrow_symm_apply_inl (α β) (x : (α → R) × (β → R)) (a : α) :

(sumArrowEquivProdArrow R α β).symm x (Sum.inl a) = x.fst a := rfl

@[simp]

lemma sumArrowEquivProdArrow_symm_apply_inr (α β) (x : (α → R) × (β → R)) (b : β) :

(sumArrowEquivProdArrow R α β).symm x (Sum.inr b) = x.snd b := rfl

@[simp]

lemma sumArrowEquivProdArrow_apply (α β) (x) :

sumArrowEquivProdArrow R α β x = Equiv.sumArrowEquivProdArrow x := rfl

@[simp]

lemma sumArrowEquivProdArrow_symm_apply (α β) (x : (α → R) × (β → R)) (b : β) :

(sumArrowEquivProdArrow R α β).symm x = (Equiv.sumArrowEquivProdArrow).symm x := rfl

which should replace the simps above (unless it can generate exactly these for you)

(same for the other similar results)

Don't you then lose all ring hom simp lemmas on RingEquiv.sumArrowEquivProdArrow? Or do you suggest to add map_{add,mul,zero,one} lemmas for Equiv.sumArrowEquivProdArrow?

Those lemmas would apply before this one I think.

It does not seem so:

example (x y) : sumArrowEquivProdArrow α β R (x + y) = sumArrowEquivProdArrow α β R x + sumArrowEquivProdArrow α β R y := by simp

fails (and succeeds if I remove simp from the lemmas you suggest).

Does it work if you use simp 900 on the lemmas I suggested?

No, it only starts working with simp 100 (simp 101 is the first non-working one).

Strange, thanks for investigating! I can look into this further tomorrow

#25165 will help here I think. For now, can you set the priority to low - 1, with a comment saying that this is lower than map_add etc.? Then we can merge this without the other one.

Since #25165 was merged before this one, I switched all the low - 1 to low.

eric-wieser · 2025-05-24T17:21:08Z

Could you update the description to be explicit about what the new defs are, and how they relate to existing ones?

erdOne

The discussion above seems to be addressed already, and the PR has been stale for months so I'll

maintainer merge

github-actions · 2025-07-04T14:50:03Z

🚀 Pull request has been placed on the maintainer queue by erdOne.

riccardobrasca · 2025-07-05T04:42:58Z

Thanks!

bors merge

Add - `RingEquiv.sumArrowEquivProdArrow`: ring version of `Equiv.sumArrowEquivProdArrow`. - `AlgEquiv.sumArrowEquivProdArrow`: algebra version of `Equiv.sumArrowEquivProdArrow`. - `AlgEquiv.piCongrLeft'`: algebra version of `Equiv.piCongrLeft`. - `AlgEquiv.piCongrLeft`: algebra version of `Equiv.piCongrLeft`. - `AlgEquiv.funUnique`: algebra version of `Equiv.funUnique`. - `AlgEquiv.prodCongr`: algebra version of `Equiv.prodCongr`. The four last ones already have ring versions.

mathlib-bors · 2025-07-05T05:52:20Z

Pull request successfully merged into master.

Build succeeded:

CI Success

…r-community#24520) Add - `RingEquiv.sumArrowEquivProdArrow`: ring version of `Equiv.sumArrowEquivProdArrow`. - `AlgEquiv.sumArrowEquivProdArrow`: algebra version of `Equiv.sumArrowEquivProdArrow`. - `AlgEquiv.piCongrLeft'`: algebra version of `Equiv.piCongrLeft`. - `AlgEquiv.piCongrLeft`: algebra version of `Equiv.piCongrLeft`. - `AlgEquiv.funUnique`: algebra version of `Equiv.funUnique`. - `AlgEquiv.prodCongr`: algebra version of `Equiv.prodCongr`. The four last ones already have ring versions.

chrisflav added 2 commits May 1, 2025 18:02

alg equivs for products

ddc1850

add lemmas

dfdf25f

chrisflav added the t-algebra Algebra (groups, rings, fields, etc) label May 1, 2025

github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label May 1, 2025

reorganize

1c530d7

mistarro reviewed May 1, 2025

View reviewed changes

Mathlib/Algebra/Ring/Equiv.lean Outdated Show resolved Hide resolved

move around

dce0b53

github-actions bot removed the large-import Automatically added label for PRs with a significant increase in transitive imports label May 1, 2025

chrisflav added 2 commits May 1, 2025 21:54

reduce imports

43876c6

fix?

4ce75e0

chrisflav added 2 commits May 16, 2025 07:07

Revert "move around"

fde2c62

This reverts commit dce0b53.

Merge remote-tracking branch 'origin/master' into chrisflav-picongr

ed32b1a

grunweg assigned eric-wieser May 24, 2025

eric-wieser reviewed May 24, 2025

View reviewed changes

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

chrisflav changed the title ~~feat(Algebra/Pi): add AlgEquiv.prodCongr~~ feat(Algebra/Pi): add various AlgEquivs and RingEquivs May 24, 2025

chrisflav removed the awaiting-author A reviewer has asked the author a question or requested changes. label May 24, 2025

chrisflav added 2 commits May 24, 2025 20:59

small improvement

c272939

fix

7d3d116

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

review comment

2dd90e8

chrisflav added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels May 24, 2025

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 24, 2025

eric-wieser mentioned this pull request May 27, 2025

[Merged by Bors] - refactor: Use medium rather than low priority for hom lemmas #25165

Closed

switch to low

e4545a2

chrisflav requested a review from eric-wieser June 9, 2025 09:20

erdOne approved these changes Jul 4, 2025

View reviewed changes

ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Jul 4, 2025

ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Jul 5, 2025

mathlib-bors bot changed the title ~~feat(Algebra/Pi): add various AlgEquivs and RingEquivs~~ [Merged by Bors] - feat(Algebra/Pi): add various AlgEquivs and RingEquivs Jul 5, 2025

mathlib-bors bot closed this Jul 5, 2025

mathlib-bors bot deleted the chrisflav-picongr branch July 5, 2025 05:52

Conversation

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

Uh oh!

Uh oh!

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

Uh oh!

PR summary 824629269a

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Ruben-VandeVelde commented May 2, 2025

Uh oh!

chrisflav commented May 2, 2025

Uh oh!

eric-wieser commented May 14, 2025

Uh oh!

mistarro commented May 14, 2025

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

chrisflav May 24, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

eric-wieser commented May 24, 2025

Uh oh!

erdOne left a comment

Choose a reason for hiding this comment

Uh oh!

github-actions bot commented Jul 4, 2025

Uh oh!

riccardobrasca commented Jul 5, 2025

Uh oh!

mathlib-bors bot commented Jul 5, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

6 participants

chrisflav commented May 1, 2025 •

edited

Loading

github-actions bot commented May 1, 2025 •

edited

Loading

chrisflav May 24, 2025 •

edited

Loading