# Mate of natural transformations #

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.

def CategoryTheory.transferNatTrans {C : Type u₁} {D : Type u₂} [] [] {E : Type u₃} {F : Type u₄} [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) :
() ()

Suppose we have a square of functors (where the top and bottom are adjunctions L₁ ⊣ R₁ and L₂ ⊣ R₂ respectively).

  C ↔ D
G ↓   ↓ H
E ↔ F


Then we have a bijection between natural transformations G ⋙ L₂ ⟶ L₁ ⋙ H and R₁ ⋙ G ⟶ H ⋙ R₂. This can be seen as a bijection of the 2-cells:

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


Note that if one of the transformations is an iso, it does not imply the other is an iso.

Instances For
theorem CategoryTheory.transferNatTrans_counit {C : Type u₁} {D : Type u₂} [] [] {E : Type u₃} {F : Type u₄} [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : ) (Y : D) :
theorem CategoryTheory.unit_transferNatTrans {C : Type u₁} {D : Type u₂} [] [] {E : Type u₃} {F : Type u₄} [] [] {G : } {H : } {L₁ : } {R₁ : } {L₂ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : ) (X : C) :
def CategoryTheory.transferNatTransSelf {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) :
(L₂ L₁) (R₁ R₂)

Given two adjunctions L₁ ⊣ R₁ and L₂ ⊣ R₂ both between categories C, D, there is a bijection between natural transformations L₂ ⟶ L₁ and natural transformations R₁ ⟶ R₂. This is defined as a special case of transferNatTrans, where the two "vertical" functors are identity. TODO: Generalise to when the two vertical functors are equivalences rather than being exactly 𝟭.

Furthermore, this bijection preserves (and reflects) isomorphisms, i.e. a transformation is an iso iff its image under the bijection is an iso, see eg CategoryTheory.transferNatTransSelf_iso. This is in contrast to the general case transferNatTrans which does not in general have this property.

Instances For
theorem CategoryTheory.transferNatTransSelf_counit {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) (X : D) :
CategoryTheory.CategoryStruct.comp (L₂.map ((↑() f).app X)) (adj₂.counit.app X) = CategoryTheory.CategoryStruct.comp (f.app (R₁.obj X)) (adj₁.counit.app X)
theorem CategoryTheory.unit_transferNatTransSelf {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) (X : C) :
CategoryTheory.CategoryStruct.comp (adj₁.unit.app X) ((↑() f).app (L₁.obj X)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app X) (R₂.map (f.app X))
@[simp]
theorem CategoryTheory.transferNatTransSelf_id {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {R₁ : } (adj₁ : L₁ R₁) :
@[simp]
theorem CategoryTheory.transferNatTransSelf_symm_id {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {R₁ : } (adj₁ : L₁ R₁) :
().symm () =
theorem CategoryTheory.transferNatTransSelf_comp {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {L₃ : } {R₁ : } {R₂ : } {R₃ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (f : L₂ L₁) (g : L₃ L₂) :
CategoryTheory.CategoryStruct.comp (↑() f) (↑() g) = ↑() ()
theorem CategoryTheory.transferNatTransSelf_adjunction_id {C : Type u₁} [] {L : } {R : } (adj : L R) (f : ) (X : C) :
theorem CategoryTheory.transferNatTransSelf_adjunction_id_symm {C : Type u₁} [] {L : } {R : } (adj : L R) (g : ) (X : C) :
theorem CategoryTheory.transferNatTransSelf_symm_comp {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {L₃ : } {R₁ : } {R₂ : } {R₃ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (f : R₂ R₁) (g : R₃ R₂) :
CategoryTheory.CategoryStruct.comp (().symm f) (().symm g) = ().symm ()
theorem CategoryTheory.transferNatTransSelf_comm {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) {f : L₂ L₁} {g : L₁ L₂} :
theorem CategoryTheory.transferNatTransSelf_symm_comm {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) {f : R₁ R₂} {g : R₂ R₁} :
CategoryTheory.CategoryStruct.comp (().symm f) (().symm g) =
instance CategoryTheory.transferNatTransSelf_iso {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) :

If f is an isomorphism, then the transferred natural transformation is an isomorphism. The converse is given in transferNatTransSelf_of_iso.

instance CategoryTheory.transferNatTransSelf_symm_iso {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : R₁ R₂) :
CategoryTheory.IsIso (().symm f)

If f is an isomorphism, then the un-transferred natural transformation is an isomorphism. The converse is given in transferNatTransSelf_symm_of_iso.

theorem CategoryTheory.transferNatTransSelf_of_iso {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) [CategoryTheory.IsIso (↑() f)] :

If f is a natural transformation whose transferred natural transformation is an isomorphism, then f is an isomorphism. The converse is given in transferNatTransSelf_iso.

theorem CategoryTheory.transferNatTransSelf_symm_of_iso {C : Type u₁} {D : Type u₂} [] [] {L₁ : } {L₂ : } {R₁ : } {R₂ : } (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : R₁ R₂) [CategoryTheory.IsIso (().symm f)] :

If f is a natural transformation whose un-transferred natural transformation is an isomorphism, then f is an isomorphism. The converse is given in transferNatTransSelf_symm_iso.