[Merged by Bors] - feat (Category Theory): redefine and extend mates

[emilyriehl]

The mates bijection between natural transformations inhabiting a certain dual pairs of squares (the duality in the sense of a parallel pair of adjunctions) can be defined in a more direct way: using pasting composition on 2-cells.

This pull request:
(i) proposes a new definition of Mates to replace and rename the existing transferNatTrans
(ii) proposes a new definition of Conjugates to replace and rename the existing transferNatTransSelf
(iii) proves that the mates correspondence commutes with horizontal and vertical composition of squares, as well as some coherences relating mates to conjugates
(iv) updates the files that depends on this, involving two new proofs about exponentiation in cartesian closed categories

---

I have now refactored the rest of the library, so this pull request is ready for review.

I'd appreciate feedback on two aspects of the longer coherence proofs:

(i) Can this be done without calling "ext"? I originally tried to prove this using theorems about pasting composite of natural transformations but got stuck because I couldn't rewrite along equalities of functors of the form 1 >>> F = F. It's somewhat unaesthetic, though, to prove this by passing to components.

(ii) The long proofs involve lots of slice_rhs calls. This feels fairly readable to me, but I'm curious if there is a better way.

[github-actions]

PR summary a20fcb5384

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Adjunction.Mates	332	354	+22 (+6.63%)
Mathlib.CategoryTheory.Closed.Monoidal	420	421	+1 (+0.24%)
Mathlib.CategoryTheory.Closed.Cartesian	534	535	+1 (+0.19%)
Mathlib.CategoryTheory.Closed.Functor	535	536	+1 (+0.19%)

Import changes for all files

Files	Import difference
7 files Mathlib.CategoryTheory.Closed.FunctorCategory Mathlib.CategoryTheory.Closed.Ideal Mathlib.CategoryTheory.Closed.Functor Mathlib.CategoryTheory.Closed.Types Mathlib.CategoryTheory.Closed.Monoidal Mathlib.CategoryTheory.Closed.Zero Mathlib.CategoryTheory.Closed.Cartesian	1
Mathlib.CategoryTheory.Adjunction.Mates	22

---

Declarations diff

+ conjugateEquiv
+ conjugateEquiv_adjunction_id
+ conjugateEquiv_adjunction_id_symm
+ conjugateEquiv_comm
+ conjugateEquiv_comp
+ conjugateEquiv_counit
+ conjugateEquiv_counit_symm
+ conjugateEquiv_id
+ conjugateEquiv_iso
+ conjugateEquiv_mateEquiv_vcomp
+ conjugateEquiv_of_iso
+ conjugateEquiv_symm_comm
+ conjugateEquiv_symm_comp
+ conjugateEquiv_symm_id
+ conjugateEquiv_symm_iso
+ conjugateEquiv_symm_of_iso
+ conjugateIsoEquiv
+ iterated_mateEquiv_conjugateEquiv
+ iterated_mateEquiv_conjugateEquiv_symm
+ leftAdjointConjugateSquare.vcomp
+ leftAdjointSquare.comp
+ leftAdjointSquare.comp_hvcomp
+ leftAdjointSquare.comp_vhcomp
+ leftAdjointSquare.hcomp
+ leftAdjointSquare.vcomp
+ leftAdjointSquareConjugate.vcomp
+ mateEquiv
+ mateEquiv_conjugateEquiv_vcomp
+ mateEquiv_counit
+ mateEquiv_counit_symm
+ mateEquiv_hcomp
+ mateEquiv_square
+ mateEquiv_vcomp
+ prodComparison_comp
+ rightAdjointConjugateSquare.vcomp
+ rightAdjointSquare.comp
+ rightAdjointSquare.comp_hvcomp
+ rightAdjointSquare.comp_vhcomp
+ rightAdjointSquare.hcomp
+ rightAdjointSquare.vcomp
+ rightAdjointSquareConjugate.vcomp
+ unit_conjugateEquiv
+ unit_conjugateEquiv_symm
+ unit_mateEquiv
+ unit_mateEquiv_symm
- transferNatTransSelf_adjunction_id
- transferNatTransSelf_adjunction_id_symm
- transferNatTransSelf_comm
- transferNatTransSelf_comp
- transferNatTransSelf_counit
- transferNatTransSelf_id
- transferNatTransSelf_iso
- transferNatTransSelf_of_iso
- transferNatTransSelf_symm_comm
- transferNatTransSelf_symm_comp
- transferNatTransSelf_symm_id
- transferNatTransSelf_symm_iso
- transferNatTransSelf_symm_of_iso
- transferNatTrans_counit
- unit_transferNatTrans
- unit_transferNatTransSelf

You can run this locally as follows

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

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

[b-mehta]

Thanks for this PR! Your definition certainly looks more readable, and you've proved it's equal to the old one so I'm convinced it's a good change.

Make sure to follow the lint style suggestions (more guidelines are here: https://leanprover-community.github.io/contribute/style.html).

If no-one beats me to it, I'll try to review your actual proofs in more detail soon. I think in most cases it's probably easiest to do ext and pass to components, although I agree it's not ideal.
One thing that may help you is the reassoc_of% command, which can make rewriting an equality of morphisms inside a long chain quite a bit easier - it essentially lets you ignore associativity.

[emilyriehl]

This is now ready for review (as far as I can tell).

[emilyriehl]

Note there is one (non-trivial) new definition in the latest version: conjugateIsoEquiv. I had to mark it non-computable since it uses asIso; can this be avoided?

This was included to use in applications such as the following:

namespace Over
universe v u
variable {C : Type u} [Category.{v} C]

/-- The conjugate isomorphism between pullback functors. -/
def pullbackCompIso [HasPullbacks C] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) :
    baseChange (f ≫ g) ≅ baseChange g ⋙ baseChange f :=
  conjugateIsoEquiv (mapAdjunction (f ≫ g)) ((mapAdjunction f).comp (mapAdjunction g)) (mapCompIso f g)

Here mapCompIso has type

mapCompIso {X Y Z : C}(f : X ⟶ Y)(g : Y ⟶ Z) : Over.map f ⋙ Over.map g ≅ Over.map (f ≫ g)

For testing you could replace it with (mathComp f g).symm but I'm using a different isomorphism extracted from an equality between functors because it has better computational properties.

[dagurtomas]

I just made a small suggestion about slice syntax

[emilyriehl]

@jcommelin after our discussion today I realized I need to add deprecated alias tags. Should this be done for all the renamed theorems or just for the renamed definitions?

[jcommelin]

@emilyriehl Concerning "deprecated": We don't have any strict rules yet. It's good practice to add these, because it will help projects that depend on mathlib when they migrate to a newer version. But if we estimate that these declarations aren't really used outside mathlib, then we might skip the process.
Otoh, I guess some of this stuff is being used in the Poly project, so the next mathlib bump in that project would benefit from having deprecated aliases in place.

[emilyriehl]

@jcommelin just added for the two key definitions. We're already using this version of mates in poly so that's all set.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Build failed:

• Build

[jcommelin]

bors r+

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style