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β€²