feat(Algebra/DirectSum): equivalence between direct sum indexed by ι₁ and double sum indexed by ι₂ and fibres of f : ι₁ → ι₂

[TentativeConvert]

1. Add variant equivCongrLeft' of equivCongrLeft, and corresponding …_apply lemma.
2. Add …_of lemmas for both equivCongrLeft and equivCongrLeft'.
3. Add …of lemma for sigmaCurry, i.e. sigmaCurry_of.
4. Add sigmaFiberAddEquiv: the equivalence between a direct sum indexed by a type ι₁ and the double sum indexed by a type ι₂ and the fibres of a map f : ι₁ → ι₂. Add two …_apply lemmas and an …_of lemma.

---

This is supposed to be a first step towards merging the draft PR #39356.

re 1: Mathematically, I don't see why one version should be preferred over the other, but I found the existing equivCongrLeft more difficult to work with when the equivalence h : ι ≃ κ is naturally given in the opposite direction. (I could not avoid explicit type casts through the equality h.symm.symm = h when defining sigmaFiberAddEquiv in terms of equivCongrLeft.)

Very unsure about the name of equivCongrLeft'. (I see that the name equivCongrLeft was chosen in analogy with Equiv.piCongrLeft. Equiv.piCongrRight looks very different, so presumably equivCongrLeft' should not be called equivCongrRight.)

re 4: Very unsure about the naming of the two different …_apply lemmas; called them …_apply and …_apply' for now. The second (…_apply') cannot be a simp lemma as it would prevent the first (…_apply) from firing.

I've used Claude Opus for understanding error messages and git interaction, but everything is hand coded.

[github-actions]

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

[github-actions]

PR summary 3a427c0bae

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff (regex)

+ equivCongrLeft_of
+ sigmaCurry_of
+ sigmaFiberAddEquiv
+ sigmaFiberAddEquiv_apply
+ sigmaFiberAddEquiv_apply_apply
+ sigmaFiberAddEquiv_of

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 3a427c0).

• +6 new declarations
• −0 removed declarations

+DirectSum.equivCongrLeft_of
+DirectSum.sigmaCurry_of
+DirectSum.sigmaFiberAddEquiv
+DirectSum.sigmaFiberAddEquiv_apply
+DirectSum.sigmaFiberAddEquiv_apply_apply
+DirectSum.sigmaFiberAddEquiv_of

---

No changes to strong technical debt.

No changes to weak technical debt.

Current commit 3a427c0bae
Reference commit 4a73a604a6

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/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).

[github-actions]

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

[TentativeConvert]

-awaiting-author

[themathqueen]

why are you doing by exact lemmaname and not just := lemmaname? (here and throughout)

Suggested change

	equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x := by
	exact DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv _ _
	equivCongrLeft h (of β (h.symm k) x) = of (fun k ↦ β (h.symm k)) k x :=
	DFinsupp.comapDomain'_single (⇑h.symm) h.right_inv _ _

[TentativeConvert]

Only because I noticed this in other places in Mathlib. I get 800+ hits when searching for "by exact" in Mathlib, and I've just checked a few such occurrences at random to verify that they could be rephrased the way you suggest. And I don't see anything on this in the style guide.

Anyway, happy to switch from one to the other if you believe I should.

[themathqueen]

I think sometimes (in other parts of the library maybe) there are reasons to do so, but here I see no reason to do so

[TentativeConvert]

What about the proof of equivCongrLeft_apply right above? I did not write this. It uses by exact, even though that seems completely unnecessary. If I remove by exact from the proof of equivCongrLeft_of, should I also remove it from the proof of equivCongrLeft_apply?

[themathqueen]

remove them from everywhere :)

[joneugster]

Indeed, by exact e should (preferrably) be avoided unless it's necessary. Note that by exact e and e are not identical: the former is a bit stronger and does some defeq-stuff.

However, I can't find anything about this in any convention, so before library-wide (automated) cleanups happen, it should probably be written down in the style guide.

[TentativeConvert]

-awaiting-author

[themathqueen]

I think this is fine, thanks! Not entirely sure about the name sigmaFiberAddEquiv, but can't think of a better name, so I'll let someone else review this too.

[joneugster]

I see @themathqueen already did extensive reviewing, thanks! And thank you for the PR! I suggest,

maintainer merge

[joneugster]

Indeed, by exact e should (preferrably) be avoided unless it's necessary. Note that by exact e and e are not identical: the former is a bit stronger and does some defeq-stuff.

However, I can't find anything about this in any convention, so before library-wide (automated) cleanups happen, it should probably be written down in the style guide.

[github-actions]

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