[Merged by Bors] - chore: remove unnecessary uses of CategoryTheory.Equivalence.mk

[joelriou]

An equivalence of categories consists of a functor, an inverse, and unit and counit isomorphisms which satisfy the same compatibilities as for adjoint functors. However, certain equivalences are constructed via the constructor Equivalence.mk which does not assume these compatibilities: by changing the unit isomorphism, it is possible to satisfy the compatibility. When only the existence of an equivalence matters, we may certainly use Equivalence.mk (e.g. inside proofs). However, the more we develop the library, the more we may need to unfold the definitions of unit/counit isomorphisms (as it happened in #12728). Then, I would suggest that we refrain from using Equivalence.mk as much as possible. In this PR, most uses of Equivalence.mk are removed: in most cases, the compatibilities satisfied by adjunctions were easy to prove.

---

[github-actions]

PR summary cb45dbd899

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Sums.Basic	273	271	-2 (-0.73%)
Mathlib.CategoryTheory.Sums.Associator	274	272	-2 (-0.73%)
Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup	454	453	-1 (-0.22%)

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Sums.Associator Mathlib.CategoryTheory.Sums.Basic	-2
17 files Mathlib.Algebra.Homology.ShortComplex.Ab Mathlib.CategoryTheory.Preadditive.Yoneda.Projective Mathlib.Algebra.Category.Grp.EpiMono Mathlib.Algebra.Category.Grp.AB5 Mathlib.Topology.Category.Profinite.Nobeling Mathlib.Algebra.Category.Grp.Kernels Mathlib.Algebra.Homology.ShortComplex.ModuleCat Mathlib.Algebra.Category.Grp.EnoughInjectives Mathlib.CategoryTheory.Preadditive.Yoneda.Injective Mathlib.Algebra.Category.ModuleCat.Biproducts Mathlib.CategoryTheory.Abelian.Injective Mathlib.CategoryTheory.Abelian.Projective Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory Mathlib.Algebra.Category.ModuleCat.Free Mathlib.CategoryTheory.Triangulated.Yoneda Mathlib.Algebra.Homology.ConcreteCategory	-1

---

Declarations diff

+ isoMk
- from_toCostructuredArrow_eq
- to_fromCostructuredArrow_eq
-+-+ associativity
-+-+ equivalence
-+-+ swapEquiv

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.

[b-mehta]

I'm slightly surprised aesop_cat can't do this?

[joelriou]

No, it cannot.

[dagurtomas]

maintainer merge

[github-actions]

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

[mattrobball]

!bench

[leanprover-bot]

Here are the benchmark results for commit b3c0c79.
There were significant changes against commit b2af0a8:

  Benchmark                                            Metric         Change
  ==========================================================================
+ build                                                compilation     -5.4%
+ ~Mathlib.CategoryTheory.Comma.Basic                  instructions   -36.6%
+ ~Mathlib.CategoryTheory.Comma.StructuredArrow        instructions   -42.1%
+ ~Mathlib.CategoryTheory.Elements                     instructions   -35.5%
+ ~Mathlib.CategoryTheory.Functor.KanExtension.Basic   instructions   -47.6%
+ ~Mathlib.CategoryTheory.Limits.ConeCategory          instructions   -28.3%
+ ~Mathlib.CategoryTheory.Products.Associator          instructions   -53.8%
+ ~Mathlib.CategoryTheory.Products.Basic               instructions   -17.6%

[mattrobball]

Very nice.

[mattrobball]

bors delegate+

Thanks!

[mathlib-bors]

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

[joelriou]

Very nice.

Actually, I believe that at some point, some proofs of triangle compatibilities were removed because of performances issues. The situation looks better now :-)

[mattrobball]

When it passes CI, please merge

[joelriou]

Thanks!

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style