Mate of natural transformations #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file establishes the bijection between the 2-cells

     L₁                  R₁
  C --→ D             C ←-- D
G ↓  ↗  ↓ H         G ↓  ↘  ↓ H
  E --→ F             E ←-- F
     L₂                  R₂

where L₁ ⊣ R₁ and L₂ ⊣ R₂, and shows that in the special case where G,H are identity then the bijection preserves and reflects isomorphisms (i.e. we have bijections (L₂ ⟶ L₁) ≃ (R₁ ⟶ R₂), and if either side is an iso then the other side is as well).

On its own, this bijection is not particularly useful but it includes a number of interesting cases as specializations.

For instance, this generalises the fact that adjunctions are unique (since if L₁ ≅ L₂ then we deduce R₁ ≅ R₂). Another example arises from considering the square representing that a functor H preserves products, in particular the morphism HA ⨯ H- ⟶ H(A ⨯ -). Then provided (A ⨯ -) and HA ⨯ - have left adjoints (for instance if the relevant categories are cartesian closed), the transferred natural transformation is the exponential comparison morphism: H(A ^ -) ⟶ HA ^ H-. Furthermore if H has a left adjoint L, this morphism is an isomorphism iff its mate L(HA ⨯ -) ⟶ A ⨯ L- is an isomorphism, see https://ncatlab.org/nlab/show/Frobenius+reciprocity#InCategoryTheory. This also relates to Grothendieck's yoga of six operations, though this is not spelled out in mathlib: https://ncatlab.org/nlab/show/six+operations.