# Adjunctions between large precategories

Content created by Fredrik Bakke, Egbert Rijke, Jonathan Prieto-Cubides and Elisabeth Stenholm.

Created on 2022-03-11.

module category-theory.adjunctions-large-precategories where

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

open import foundation.action-on-identifications-functions
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 precategories. 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-Precategory αC βC)
(D : Large-Precategory αD βD)
(F : functor-Large-Precategory γF C D)
(G : functor-Large-Precategory γG D C)
where

{l1 l2 : Level} (X : obj-Large-Precategory C l1)
(Y : obj-Large-Precategory D l2) →
hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y ≃
hom-Large-Precategory C X (obj-functor-Large-Precategory G Y)

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

record is-adjoint-pair-Large-Precategory : UUω
where
field

(H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
(X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) →
hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y →
hom-Large-Precategory C X (obj-functor-Large-Precategory G Y)
map-equiv-is-adjoint-pair-Large-Precategory H X Y =
map-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)

(H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
(X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) →
hom-Large-Precategory C X (obj-functor-Large-Precategory G Y) ≃
hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y
inv-equiv-is-adjoint-pair-Large-Precategory H X Y =
inv-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)

(H : is-adjoint-pair-Large-Precategory) {l1 l2 : Level}
(X : obj-Large-Precategory C l1) (Y : obj-Large-Precategory D l2) →
hom-Large-Precategory C X (obj-functor-Large-Precategory G Y) →
hom-Large-Precategory D (obj-functor-Large-Precategory F X) Y
map-inv-equiv-is-adjoint-pair-Large-Precategory H X Y =
map-inv-equiv (equiv-is-adjoint-pair-Large-Precategory H X Y)

( H : is-adjoint-pair-Large-Precategory)
{ l1 l2 l3 l4 : Level}
{ X1 : obj-Large-Precategory C l1}
{ X2 : obj-Large-Precategory C l2}
{ Y1 : obj-Large-Precategory D l3}
{ Y2 : obj-Large-Precategory D l4}
( f : hom-Large-Precategory C X2 X1)
( g : hom-Large-Precategory D Y1 Y2) →
coherence-square-maps
( map-inv-equiv-is-adjoint-pair-Large-Precategory H X1 Y1)
( λ h →
comp-hom-Large-Precategory C
( comp-hom-Large-Precategory C (hom-functor-Large-Precategory G g) h)
( f))
( λ h →
comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D g h)
( hom-functor-Large-Precategory F f))
( map-inv-equiv-is-adjoint-pair-Large-Precategory H X2 Y2)
H {X1 = X1} {X2} {Y1} {Y2} f g =
horizontal-inv-equiv-coherence-square-maps
( equiv-is-adjoint-pair-Large-Precategory H X1 Y1)
( λ h →
comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D g h)
( hom-functor-Large-Precategory F f))
( λ h →
comp-hom-Large-Precategory C
( comp-hom-Large-Precategory C
( hom-functor-Large-Precategory G g)
( h))
( f))
( equiv-is-adjoint-pair-Large-Precategory H X2 Y2)
( naturality-equiv-is-adjoint-pair-Large-Precategory H f g)


### The predicate of being a left adjoint

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

is-adjoint-pair-Large-Precategory C D F G


### The predicate of being a right adjoint

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

is-adjoint-pair-Large-Precategory C D F G


### Adjunctions of large precategories

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

record Adjunction-Large-Precategory : UUω where
field
functor-Large-Precategory γ C D
functor-Large-Precategory δ D C

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

{l : Level} → obj-Large-Precategory C l → obj-Large-Precategory D (γ l)
obj-functor-Large-Precategory

{l1 l2 : Level}
{X : obj-Large-Precategory C l1}
{Y : obj-Large-Precategory C l2} →
hom-Large-Precategory C X Y →
hom-Large-Precategory D
hom-functor-Large-Precategory

{l1 : Level} (X : obj-Large-Precategory C l1) →
( id-hom-Large-Precategory C {X = X}) ＝
id-hom-Large-Precategory D
preserves-id-functor-Large-Precategory

{l1 : Level} → obj-Large-Precategory D l1 → obj-Large-Precategory C (δ l1)
obj-functor-Large-Precategory

{l1 l2 : Level}
{X : obj-Large-Precategory D l1}
{Y : obj-Large-Precategory D l2} →
hom-Large-Precategory D X Y →
hom-Large-Precategory C
hom-functor-Large-Precategory

{l : Level}
(Y : obj-Large-Precategory D l) →
( id-hom-Large-Precategory D {X = Y}) ＝
id-hom-Large-Precategory C
preserves-id-functor-Large-Precategory

{l1 l2 : Level}
(X : obj-Large-Precategory C l1)
(Y : obj-Large-Precategory D l2) →
hom-Large-Precategory D
( Y) ≃
hom-Large-Precategory C
( X)

{l1 l2 : Level}
(X : obj-Large-Precategory C l1)
(Y : obj-Large-Precategory D l2) →
hom-Large-Precategory D
( Y) →
hom-Large-Precategory C
( X)

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

{l1 l2 : Level}
(X : obj-Large-Precategory C l1)
(Y : obj-Large-Precategory D l2) →
hom-Large-Precategory C
( X)
hom-Large-Precategory D
( Y)

{l1 l2 : Level}
(X : obj-Large-Precategory C l1)
(Y : obj-Large-Precategory D l2) →
hom-Large-Precategory C
( X)
hom-Large-Precategory D
( Y)

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


### 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-Precategory αC βC) (D : Large-Precategory αD βD)
(FG : Adjunction-Large-Precategory γ δ C D)
where

family-of-morphisms-functor-Large-Precategory C C
( id-functor-Large-Precategory C)
( comp-functor-Large-Precategory C D C
( id-hom-Large-Precategory D)

naturality-family-of-morphisms-functor-Large-Precategory C C
( id-functor-Large-Precategory C)
( comp-functor-Large-Precategory C D C
naturality-unit-Adjunction-Large-Precategory {X = X} {Y} f =
inv
( ( inv
( left-unit-law-comp-hom-Large-Precategory C
( comp-hom-Large-Precategory C
( Y))
( f)))) ∙
( ap
( comp-hom-Large-Precategory' C
( comp-hom-Large-Precategory C
( Y))
( f)))
( inv
( C)
( D)
( FG)
( obj-left-adjoint-Adjunction-Large-Precategory C D FG Y)))) ∙
( inv
( associative-comp-hom-Large-Precategory C
( id-hom-Large-Precategory D))
C D FG Y
( id-hom-Large-Precategory D))
( f))) ∙
( inv
C D FG f
( id-hom-Large-Precategory D)
( id-hom-Large-Precategory D))) ∙
( ap
( ( associative-comp-hom-Large-Precategory D
( id-hom-Large-Precategory D)
( id-hom-Large-Precategory D)
( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ∙
( left-unit-law-comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D
( id-hom-Large-Precategory D)
( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙
( left-unit-law-comp-hom-Large-Precategory D
( hom-left-adjoint-Adjunction-Large-Precategory C D FG f)) ∙
( inv
( right-unit-law-comp-hom-Large-Precategory D
( hom-left-adjoint-Adjunction-Large-Precategory C D FG f))) ∙
( inv
( right-unit-law-comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D
( id-hom-Large-Precategory D)))) ∙
( ap
( comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D
( id-hom-Large-Precategory D)))
( inv
C D FG X)))) ∙
C D FG
( id-hom-Large-Precategory C)
( id-hom-Large-Precategory D)) ∙
( right-unit-law-comp-hom-Large-Precategory C
( comp-hom-Large-Precategory C
( X))))))

natural-transformation-Large-Precategory C C
( id-functor-Large-Precategory C)
( comp-functor-Large-Precategory C D C
hom-natural-transformation-Large-Precategory
naturality-natural-transformation-Large-Precategory


### 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-Precategory αC βC) (D : Large-Precategory αD βD)
(FG : Adjunction-Large-Precategory γ δ C D)
where

family-of-morphisms-functor-Large-Precategory D D
( comp-functor-Large-Precategory D C D
( id-functor-Large-Precategory D)
( Y)
( id-hom-Large-Precategory C)

naturality-family-of-morphisms-functor-Large-Precategory D D
( comp-functor-Large-Precategory D C D
( id-functor-Large-Precategory D)
naturality-counit-Adjunction-Large-Precategory {X = X} {Y = Y} f =
inv
( ( inv
( left-unit-law-comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D
( Y))
( hom-right-adjoint-Adjunction-Large-Precategory C D FG f))))) ∙
( inv
( associative-comp-hom-Large-Precategory D
( id-hom-Large-Precategory D)
( Y)
( id-hom-Large-Precategory C))
( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)))) ∙
( inv
( C)
( D)
( FG)
( id-hom-Large-Precategory D)
( id-hom-Large-Precategory C))) ∙
( ap
( Y))
( ( ap
( comp-hom-Large-Precategory' C
( ( right-unit-law-comp-hom-Large-Precategory C
( id-hom-Large-Precategory D))) ∙
C D FG Y))) ∙
( left-unit-law-comp-hom-Large-Precategory C
( hom-right-adjoint-Adjunction-Large-Precategory C D FG f)) ∙
( ( inv
( right-unit-law-comp-hom-Large-Precategory C
( hom-right-adjoint-Adjunction-Large-Precategory C D FG f))) ∙
( inv
( right-unit-law-comp-hom-Large-Precategory C
( comp-hom-Large-Precategory C
( id-hom-Large-Precategory C)))))) ∙
( FG)
( id-hom-Large-Precategory C)
( f)
( id-hom-Large-Precategory C)) ∙
( ap
( comp-hom-Large-Precategory
( D)
( comp-hom-Large-Precategory D f
( X))))
( C)
( D)
( FG)
( obj-right-adjoint-Adjunction-Large-Precategory C D FG X))) ∙
( right-unit-law-comp-hom-Large-Precategory D
( comp-hom-Large-Precategory D f
( X))))))

natural-transformation-Large-Precategory D D
( comp-functor-Large-Precategory D C D