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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} {F : Type u₄} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F} {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F} {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) : (CategoryTheory.Functor.comp G L₂ ⟶ CategoryTheory.Functor.comp L₁ H) ≃ (CategoryTheory.Functor.comp R₁ G ⟶ CategoryTheory.Functor.comp 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

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.transferNatTrans_counit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} {F : Type u₄} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F} {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F} {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : CategoryTheory.Functor.comp G L₂ ⟶ CategoryTheory.Functor.comp L₁ H) (Y : D) : CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.transferNatTrans adj₁ adj₂) f).app Y)) (adj₂.counit.app (H.obj Y)) = CategoryTheory.CategoryStruct.comp (f.app (R₁.obj Y)) (H.map (adj₁.counit.app Y))

theorem CategoryTheory.unit_transferNatTrans {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {E : Type u₃} {F : Type u₄} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.Category.{v₄, u₄} F] {G : CategoryTheory.Functor C E} {H : CategoryTheory.Functor D F} {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {L₂ : CategoryTheory.Functor E F} {R₂ : CategoryTheory.Functor F E} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : CategoryTheory.Functor.comp G L₂ ⟶ CategoryTheory.Functor.comp L₁ H) (X : C) : CategoryTheory.CategoryStruct.comp (G.map (adj₁.unit.app X)) (((CategoryTheory.transferNatTrans adj₁ adj₂) f).app (L₁.obj X)) = CategoryTheory.CategoryStruct.comp (adj₂.unit.app (G.obj ((CategoryTheory.Functor.id C).obj X))) (R₂.map (f.app ((CategoryTheory.Functor.id C).obj X)))

def CategoryTheory.transferNatTransSelf {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor 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 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.

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.transferNatTransSelf_counit {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : L₂ ⟶ L₁) (X : D) : CategoryTheory.CategoryStruct.comp (L₂.map (((CategoryTheory.transferNatTransSelf adj₁ adj₂) 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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : L₂ ⟶ L₁) (X : C) : CategoryTheory.CategoryStruct.comp (adj₁.unit.app X) (((CategoryTheory.transferNatTransSelf adj₁ adj₂) 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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) : (CategoryTheory.transferNatTransSelf adj₁ adj₁) (CategoryTheory.CategoryStruct.id L₁) = CategoryTheory.CategoryStruct.id R₁

@[simp]

theorem CategoryTheory.transferNatTransSelf_symm_id {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) : (CategoryTheory.transferNatTransSelf adj₁ adj₁).symm (CategoryTheory.CategoryStruct.id R₁) = CategoryTheory.CategoryStruct.id L₁

theorem CategoryTheory.transferNatTransSelf_comp {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {L₃ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} {R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (f : L₂ ⟶ L₁) (g : L₃ ⟶ L₂) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.transferNatTransSelf adj₁ adj₂) f) ((CategoryTheory.transferNatTransSelf adj₂ adj₃) g) = (CategoryTheory.transferNatTransSelf adj₁ adj₃) (CategoryTheory.CategoryStruct.comp g f)

theorem CategoryTheory.transferNatTransSelf_adjunction_id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {L : CategoryTheory.Functor C C} {R : CategoryTheory.Functor C C} (adj : L ⊣ R) (f : CategoryTheory.Functor.id C ⟶ L) (X : C) : ((CategoryTheory.transferNatTransSelf adj CategoryTheory.Adjunction.id) f).app X = CategoryTheory.CategoryStruct.comp (f.app (R.obj X)) (adj.counit.app X)

theorem CategoryTheory.transferNatTransSelf_adjunction_id_symm {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {L : CategoryTheory.Functor C C} {R : CategoryTheory.Functor C C} (adj : L ⊣ R) (g : R ⟶ CategoryTheory.Functor.id C) (X : C) : ((CategoryTheory.transferNatTransSelf adj CategoryTheory.Adjunction.id).symm g).app X = CategoryTheory.CategoryStruct.comp (adj.unit.app X) (g.app (L.obj X))

theorem CategoryTheory.transferNatTransSelf_symm_comp {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {L₃ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} {R₃ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (adj₃ : L₃ ⊣ R₃) (f : R₂ ⟶ R₁) (g : R₃ ⟶ R₂) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.transferNatTransSelf adj₂ adj₁).symm f) ((CategoryTheory.transferNatTransSelf adj₃ adj₂).symm g) = (CategoryTheory.transferNatTransSelf adj₃ adj₁).symm (CategoryTheory.CategoryStruct.comp g f)

theorem CategoryTheory.transferNatTransSelf_comm {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) {f : L₂ ⟶ L₁} {g : L₁ ⟶ L₂} (gf : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id L₁) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.transferNatTransSelf adj₁ adj₂) f) ((CategoryTheory.transferNatTransSelf adj₂ adj₁) g) = CategoryTheory.CategoryStruct.id R₁

theorem CategoryTheory.transferNatTransSelf_symm_comm {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) {f : R₁ ⟶ R₂} {g : R₂ ⟶ R₁} (gf : CategoryTheory.CategoryStruct.comp g f = CategoryTheory.CategoryStruct.id R₂) : CategoryTheory.CategoryStruct.comp ((CategoryTheory.transferNatTransSelf adj₁ adj₂).symm f) ((CategoryTheory.transferNatTransSelf adj₂ adj₁).symm g) = CategoryTheory.CategoryStruct.id L₂

instance CategoryTheory.transferNatTransSelf_iso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : L₂ ⟶ L₁) [CategoryTheory.IsIso f] : CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂) f)

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

Equations

• ⋯ = ⋯

instance CategoryTheory.transferNatTransSelf_symm_iso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : R₁ ⟶ R₂) [CategoryTheory.IsIso f] : CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂).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.

Equations

• ⋯ = ⋯

theorem CategoryTheory.transferNatTransSelf_of_iso {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : L₂ ⟶ L₁) [CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂) f)] : 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₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Category.{v₂, u₂} D] {L₁ : CategoryTheory.Functor C D} {L₂ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} {R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂) (f : R₁ ⟶ R₂) [CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂).symm f)] : CategoryTheory.IsIso 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.