# 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 category_theory.transfer_nat_trans {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} {G : C E} {H : D F} {L₁ : C D} {R₁ : D C} {L₂ : E F} {R₂ : F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) :
(G L₂ L₁ H) (R₁ G H 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.

Equations
theorem category_theory.transfer_nat_trans_counit {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} {G : C E} {H : D F} {L₁ : C D} {R₁ : D C} {L₂ : E F} {R₂ : F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : G L₂ L₁ H) (Y : D) :
theorem category_theory.unit_transfer_nat_trans {C : Type u₁} {D : Type u₂} {E : Type u₃} {F : Type u₄} {G : C E} {H : D F} {L₁ : C D} {R₁ : D C} {L₂ : E F} {R₂ : F E} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : G L₂ L₁ H) (X : C) :
G.map (adj₁.unit.app X) ( adj₂) f).app (L₁.obj X) = adj₂.unit.app (G.obj ((𝟭 C).obj X)) R₂.map (f.app ((𝟭 C).obj X))
def category_theory.transfer_nat_trans_self {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (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 transfer_nat_trans, 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 category_theory.transfer_nat_trans_self_iso. This is in contrast to the general case transfer_nat_trans which does not in general have this property.

Equations
theorem category_theory.transfer_nat_trans_self_counit {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) (X : D) :
theorem category_theory.unit_transfer_nat_trans_self {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) (X : C) :
@[simp]
theorem category_theory.transfer_nat_trans_self_id {C : Type u₁} {D : Type u₂} {L₁ : C D} {R₁ : D C} (adj₁ : L₁ R₁) :
adj₁) (𝟙 L₁) = 𝟙 R₁
@[simp]
theorem category_theory.transfer_nat_trans_self_symm_id {C : Type u₁} {D : Type u₂} {L₁ : C D} {R₁ : D C} (adj₁ : L₁ R₁) :
adj₁).symm) (𝟙 R₁) = 𝟙 L₁
theorem category_theory.transfer_nat_trans_self_comp {C : Type u₁} {D : Type u₂} {L₁ L₂ L₃ : C D} {R₁ R₂ R₃ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (f : L₂ L₁) (g : L₃ L₂) :
theorem category_theory.transfer_nat_trans_self_symm_comp {C : Type u₁} {D : Type u₂} {L₁ L₂ L₃ : C D} {R₁ R₂ R₃ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (adj₃ : L₃ R₃) (f : R₂ R₁) (g : R₃ R₂) :
theorem category_theory.transfer_nat_trans_self_comm {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) {f : L₂ L₁} {g : L₁ L₂} (gf : g f = 𝟙 L₁) :
theorem category_theory.transfer_nat_trans_self_symm_comm {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) {f : R₁ R₂} {g : R₂ R₁} (gf : g f = 𝟙 R₂) :
@[instance]
def category_theory.transfer_nat_trans_self_iso {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (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 transfer_nat_trans_self_of_iso.

Equations
@[instance]
def category_theory.transfer_nat_trans_self_symm_iso {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : R₁ R₂)  :

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

Equations
def category_theory.transfer_nat_trans_self_of_iso {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) [category_theory.is_iso ( adj₂) f)] :

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

Equations
def category_theory.transfer_nat_trans_self_symm_of_iso {C : Type u₁} {D : Type u₂} {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : R₁ R₂) [category_theory.is_iso ( adj₂).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 transfer_nat_trans_self_symm_iso.

Equations