mathlib documentation

category_theory.adjunction.mates

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₂} [category_theory.category C] [category_theory.category D] {E : Type u₃} {F : Type u₄} [category_theory.category E] [category_theory.category F] {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₂} [category_theory.category C] [category_theory.category D] {E : Type u₃} {F : Type u₄} [category_theory.category E] [category_theory.category F] {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) :
L₂.map (((category_theory.transfer_nat_trans adj₁ adj₂) f).app Y) adj₂.counit.app (H.obj Y) = f.app (R₁.obj Y) H.map (adj₁.counit.app Y)
theorem category_theory.unit_transfer_nat_trans {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {E : Type u₃} {F : Type u₄} [category_theory.category E] [category_theory.category F] {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) ((category_theory.transfer_nat_trans adj₁ 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₂} [category_theory.category C] [category_theory.category D] {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₂} [category_theory.category C] [category_theory.category D] {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) (X : D) :
L₂.map (((category_theory.transfer_nat_trans_self adj₁ adj₂) f).app X) adj₂.counit.app X = f.app (R₁.obj X) adj₁.counit.app X
theorem category_theory.unit_transfer_nat_trans_self {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) (X : C) :
adj₁.unit.app X ((category_theory.transfer_nat_trans_self adj₁ adj₂) f).app (L₁.obj X) = adj₂.unit.app X R₂.map (f.app X)
@[simp]
theorem category_theory.transfer_nat_trans_self_id {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {L₁ : C D} {R₁ : D C} (adj₁ : L₁ R₁) :
@[simp]
theorem category_theory.transfer_nat_trans_self_symm_id {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {L₁ : C D} {R₁ : D C} (adj₁ : L₁ R₁) :
theorem category_theory.transfer_nat_trans_self_comp {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {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₂} [category_theory.category C] [category_theory.category D] {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₂} [category_theory.category C] [category_theory.category D] {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₂} [category_theory.category C] [category_theory.category D] {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₂} [category_theory.category C] [category_theory.category D] {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) [category_theory.is_iso f] :

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

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

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.

theorem category_theory.transfer_nat_trans_self_of_iso {C : Type u₁} {D : Type u₂} [category_theory.category C] [category_theory.category D] {L₁ L₂ : C D} {R₁ R₂ : D C} (adj₁ : L₁ R₁) (adj₂ : L₂ R₂) (f : L₂ L₁) [category_theory.is_iso ((category_theory.transfer_nat_trans_self adj₁ 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.

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