module Cat.Displayed.Adjoint where

Displayed adjunctionsπŸ”—

Following the general theme of defining displayed structure over 1-categorical structure, we can define a notion of displayed adjoint functors.

Let E,F\mathcal{E}, \mathcal{F} be categories displayed over A,B\mathcal{A}, \mathcal{B}, resp. Furthermore, let L:Aβ†’BL : \mathcal{A} \to \mathcal{B} and R:Bβ†’BR : \mathcal{B} \to \mathcal{B} be a pair of adjoint functors. We say 2 displayed functors Lβ€²,Rβ€²L', R' over LL and RR resp. are displayed adjoint functors if we have displayed natural transformations Ξ·β€²:Idβ†’Rβ€²βˆ˜Lβ€²\eta' : \mathrm{Id} \to R' \circ L' and Ξ΅β€²:Lβ€²βˆ˜Rβ€²β†’Id\varepsilon' : L' \circ R' \to \mathrm{Id} displayed over the unit and counit of the adjunction in the base that satisfy the usual triangle identities.

  record _⊣[_]_
    (L' : Displayed-functor β„° β„± L)
    (adj : L ⊣ R)
    (R' : Displayed-functor β„± β„° R )
    : Type lvl where
    no-eta-equality
    open _⊣_ adj
    field
      unit' : Id' =[ unit ]=> R' F∘' L'
      counit' : L' F∘' R' =[ counit ]=> Id'

    module unit' = _=[_]=>_ unit'
    module counit' = _=[_]=>_ counit' renaming (Ξ·' to Ξ΅')

    field
      zig' : βˆ€ {x} {x' : β„°.Ob[ x ]}
          β†’ (counit'.Ξ΅' (L' .Fβ‚€' x') β„±.∘' L' .F₁' (unit'.Ξ·' x')) β„±.≑[ zig ] β„±.id'
      zag' : βˆ€ {x} {x' : β„±.Ob[ x ]}
          β†’ (R' .F₁' (counit'.Ξ΅' x') β„°.∘' unit'.Ξ·' (R' .Fβ‚€' x')) β„°.≑[ zag ] β„°.id'

Fibred adjunctionsπŸ”—

Let E\mathcal{E} and F\mathcal{F} be categories displayed over some B\mathcal{B}. We say that a pair of vertical fibred functors L:E→FL : \mathcal{E} \to \mathcal{F}, R:F→cFR : \mathcal{F} \to cF are fibred adjoint functors if they are displayed adjoint functors, and the unit and counit are vertical natural transformations.

  record _βŠ£β†“_
    (L : Vertical-fibred-functor β„° β„±)
    (R : Vertical-fibred-functor β„± β„°)
    : Type lvl where
    no-eta-equality
    field
      unit' : IdVf =>f↓ R Vf∘ L
      counit' : L Vf∘ R =>f↓ IdVf

    module unit' = _=>↓_ unit'
    module counit' = _=>↓_ counit' renaming (Ξ·' to Ξ΅')

    field
      zig' : βˆ€ {x} {x' : β„°.Ob[ x ]}
           β†’ counit'.Ξ΅' (L .Fβ‚€' x') β„±.∘' L .F₁' (unit'.Ξ·' x') β„±.≑[ idl id ] β„±.id'
      zag' : βˆ€ {x} {x' : β„±.Ob[ x ]}
           β†’ R .F₁' (counit'.Ξ΅' x') β„°.∘' unit'.Ξ·' (R .Fβ‚€' x') β„°.≑[ idl id ] β„°.id'