Content created by Egbert Rijke and Fredrik Bakke.

Created on 2023-10-17.

module category-theory.adjunctions-large-categories where

Imports
open import category-theory.adjunctions-large-precategories
open import category-theory.functors-large-categories
open import category-theory.large-categories
open import category-theory.natural-transformations-functors-large-categories

open import foundation.commuting-squares-of-maps
open import foundation.equivalences
open import foundation.identity-types
open import foundation.universe-levels


## Idea

Let C and D be two large categories. Two functors F : C → D and G : D → C constitute an adjoint pair if

• for each pair of objects X in C and Y in D, there is an equivalence ϕ X Y : hom (F X) Y ≃ hom X (G Y) such that
• for every pair of morhpisms f : X₂ → X₁ and g : Y₁ → Y₂ the following square commutes:
                       ϕ X₁ Y₁
hom (F X₁) Y₁ --------> hom X₁ (G Y₁)
|                       |
g ∘ - ∘ F f |                       | G g ∘ - ∘ f
|                       |
∨                       ∨
hom (F X₂) Y₂ --------> hom X₂ (G Y₂)
ϕ X₂ Y₂


In this case we say that F is left adjoint to G and G is right adjoint to F, and write this as F ⊣ G.

Note: The direction of the equivalence ϕ X Y is chosen in such a way that it often coincides with the direction of the natural map. For example, in the abelianization adjunction, the natural candidate for an equivalence is given by precomposition

  - ∘ η : hom (abelianization-Group G) A → hom G (group-Ab A)


by the unit of the adjunction.

## Definition

### The predicate of being an adjoint pair of functors

module _
{αC αD γF γG : Level → Level}
{βC βD : Level → Level → Level}
(C : Large-Category αC βC)
(D : Large-Category αD βD)
(F : functor-Large-Category γF C D)
(G : functor-Large-Category γG D C)
where

( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)
( G)

( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)
( G)

( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)
( G)

(H : is-adjoint-pair-Large-Category) {l1 l2 : Level}
(X : obj-Large-Category C l1) (Y : obj-Large-Category D l2) →
hom-Large-Category D (obj-functor-Large-Category C D F X) Y →
hom-Large-Category C X (obj-functor-Large-Category D C G Y)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)
( G)

(H : is-adjoint-pair-Large-Category) {l1 l2 : Level}
(X : obj-Large-Category C l1) (Y : obj-Large-Category D l2) →
hom-Large-Category C X (obj-functor-Large-Category D C G Y) ≃
hom-Large-Category D (obj-functor-Large-Category C D F X) Y
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)
( G)

(H : is-adjoint-pair-Large-Category) {l1 l2 : Level}
(X : obj-Large-Category C l1) (Y : obj-Large-Category D l2) →
hom-Large-Category C X (obj-functor-Large-Category D C G Y) →
hom-Large-Category D (obj-functor-Large-Category C D F X) Y
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)
( G)

{ l1 l2 l3 l4 : Level}
{ X1 : obj-Large-Category C l1}
{ X2 : obj-Large-Category C l2}
{ Y1 : obj-Large-Category D l3}
{ Y2 : obj-Large-Category D l4}
( f : hom-Large-Category C X2 X1)
( g : hom-Large-Category D Y1 Y2) →
coherence-square-maps
( λ h →
comp-hom-Large-Category C
( comp-hom-Large-Category C (hom-functor-Large-Category D C G g) h)
( f))
( λ h →
comp-hom-Large-Category D
( comp-hom-Large-Category D g h)
( hom-functor-Large-Category C D F f))
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)
( G)


### The predicate of being a left adjoint

module _
{αC αD γF γG : Level → Level}
{βC βD : Level → Level → Level}
{C : Large-Category αC βC}
{D : Large-Category αD βD}
(G : functor-Large-Category γG D C)
(F : functor-Large-Category γF C D)
where



### The predicate of being a right adjoint

module _
{αC αD γF γG : Level → Level}
{βC βD : Level → Level → Level}
{C : Large-Category αC βC}
{D : Large-Category αD βD}
(F : functor-Large-Category γF C D)
(G : functor-Large-Category γG D C)
where



module _
{αC αD : Level → Level}
{βC βD : Level → Level → Level}
(γ δ : Level → Level)
(C : Large-Category αC βC)
(D : Large-Category αD βD)
where

( large-precategory-Large-Category C)
( large-precategory-Large-Category D)

module _
{αC αD : Level → Level}
{βC βD : Level → Level → Level}
{γ δ : Level → Level}
(C : Large-Category αC βC)
(D : Large-Category αD βD)
(F : Adjunction-Large-Category γ δ C D)
where

functor-Large-Category γ C D

functor-Large-Category δ D C

{l : Level} → obj-Large-Category C l → obj-Large-Category D (γ l)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l1 l2 : Level}
{X : obj-Large-Category C l1}
{Y : obj-Large-Category C l2} →
hom-Large-Category C X Y →
hom-Large-Category D
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l1 : Level}
(X : obj-Large-Category C l1) →
( id-hom-Large-Category C {X = X}) ＝
id-hom-Large-Category D
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l1 : Level} → obj-Large-Category D l1 → obj-Large-Category C (δ l1)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l1 l2 : Level}
{X : obj-Large-Category D l1}
{Y : obj-Large-Category D l2} →
hom-Large-Category D X Y →
hom-Large-Category C
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l : Level}
(Y : obj-Large-Category D l) →
( id-hom-Large-Category D {X = Y}) ＝
id-hom-Large-Category C
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l1 l2 : Level}
(X : obj-Large-Category C l1)
(Y : obj-Large-Category D l2) →
hom-Large-Category D
( Y) →
hom-Large-Category C
( X)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l1 l2 : Level}
(X : obj-Large-Category C l1)
(Y : obj-Large-Category D l2) →
hom-Large-Category C
( X)
hom-Large-Category D
( Y)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l1 l2 : Level}
(X : obj-Large-Category C l1)
(Y : obj-Large-Category D l2) →
hom-Large-Category C
( X)
hom-Large-Category D
( Y)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

{l1 l2 l3 l4 : Level}
{X1 : obj-Large-Category C l1}
{X2 : obj-Large-Category C l2}
{Y1 : obj-Large-Category D l3}
{Y2 : obj-Large-Category D l4}
(f : hom-Large-Category C X2 X1)
(g : hom-Large-Category D Y1 Y2) →
coherence-square-maps
( λ h →
comp-hom-Large-Category C
( comp-hom-Large-Category C
( h))
( f))
( λ h →
comp-hom-Large-Category D
( comp-hom-Large-Category D g h)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)


### The unit of an adjunction

Given an adjoint pair F ⊣ G, we construct a natural transformation η : id → G ∘ F called the unit of the adjunction.

module _
{αC αD : Level → Level} {βC βD : Level → Level → Level} {γ δ : Level → Level}
(C : Large-Category αC βC) (D : Large-Category αD βD)
(F : Adjunction-Large-Category γ δ C D)
where

family-of-morphisms-functor-Large-Category C C
( id-functor-Large-Category C)
( comp-functor-Large-Category C D C
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

naturality-family-of-morphisms-functor-Large-Category C C
( id-functor-Large-Category C)
( comp-functor-Large-Category C D C
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

natural-transformation-Large-Category C C
( id-functor-Large-Category C)
( comp-functor-Large-Category C D C
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)


### The counit of an adjunction

Given an adjoint pair F ⊣ G, we construct a natural transformation ε : F ∘ G → id called the counit of the adjunction.

module _
{αC αD : Level → Level} {βC βD : Level → Level → Level} {γ δ : Level → Level}
(C : Large-Category αC βC) (D : Large-Category αD βD)
(F : Adjunction-Large-Category γ δ C D)
where

family-of-morphisms-functor-Large-Category D D
( comp-functor-Large-Category D C D
( id-functor-Large-Category D)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)

naturality-family-of-morphisms-functor-Large-Category D D
( comp-functor-Large-Category D C D
( id-functor-Large-Category D)
( large-precategory-Large-Category C)
( large-precategory-Large-Category D)
( F)