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.
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.
Instances For
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.
Instances For
If f is an isomorphism, then the transferred natural transformation is an isomorphism.
The converse is given in transferNatTransSelf_of_iso.
Equations
- (_ : CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂) f)) = (_ : CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂) 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
- (_ : CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂).symm f)) = (_ : CategoryTheory.IsIso ((CategoryTheory.transferNatTransSelf adj₁ adj₂).symm 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.
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.