open import Cat.Diagram.Limit.Finite
open import Cat.Diagram.Terminal
open import Cat.Functor.Pullback
open import Cat.Functor.Adjoint
open import Cat.Instances.Slice
open import Cat.Functor.Base
open import Cat.Prelude

import Cat.Reasoning

module Cat.Functor.Slice where

Slicing functorsπŸ”—

Let F:Cβ†’DF : \mathcal{C} \to \mathcal{D} be a functor and X:CX : \mathcal{C} an object. By a standard tool in category theory (namely β€œwhacking an entire commutative diagram with a functor”), FF restricts to a functor F/X:C/Xβ†’D/F(X)F/X : \mathcal{C}/X \to \mathcal{D}/F(X). We call this β€œslicing” the functor FF. This module investigates some of the properties of sliced functors.

Sliced : βˆ€ {o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
       β†’ (F : Functor C D)
       β†’ (X : Precategory.Ob C)
       β†’ Functor (Slice C X) (Slice D (F .Fβ‚€ X))
Sliced F X .Fβ‚€ ob = cut (F .F₁ (ob .map))
Sliced F X .F₁ sh = shβ€² where
  shβ€² : /-Hom _ _
  shβ€² .map = F .F₁ (sh .map)
  shβ€² .commutes = sym (F .F-∘ _ _) βˆ™ ap (F .F₁) (sh .commutes)
Sliced F X .F-id = /-Hom-path (F .F-id)
Sliced F X .F-∘ f g = /-Hom-path (F .F-∘ _ _)

Faithful, fully faithfulπŸ”—

Slicing preserves faithfulness and fully-faithfulness. It does not preserve fullness: Even if, by fullness, we get a map f:xβ†’y∈Cf : x \to y \in \mathcal{C} from a map h:F(x)β†’F(y)∈D/F(X)h : F(x) \to F(y) \in \mathcal{D}/F(X), it does not necessarily restrict to a map in C/X\mathcal{C}/X. We’d have to show F(y)h=F(x)F(y)h=F(x) and h=F(f)h=F(f) implies yf=xyf=x, which is possible only if FF is faithful.

module _ {o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
         {F : Functor C D} {X : Precategory.Ob C} where
  private
    module D = Cat.Reasoning D

However, if FF is faithful, then so are any of its slices F/XF/X, and additionally, if FF is full, then the sliced functors are also fully faithful.

  Sliced-faithful : is-faithful F β†’ is-faithful (Sliced F X)
  Sliced-faithful faith p = /-Hom-path (faith (ap map p))

  Sliced-ff : is-fully-faithful F β†’ is-fully-faithful (Sliced F X)
  Sliced-ff eqv = is-iso→is-equiv isom where
    isom : is-iso _
    isom .is-iso.inv sh = record
      { map = equiv→inverse eqv (sh .map)
      ; commutes = ap fst $ is-contr→is-prop (eqv .is-eqv _)
        (_ , F .F-∘ _ _ βˆ™ apβ‚‚ D._∘_ refl (equivβ†’counit eqv _) βˆ™ sh .commutes) (_ , refl)
      }
    isom .is-iso.rinv x = /-Hom-path (equiv→counit eqv _)
    isom .is-iso.linv x = /-Hom-path (equiv→unit eqv _)

Left exactnessπŸ”—

If FF is lex (meaning it preserves pullbacks and the terminal object), then F/XF/X is lex as well. We note that it (by definition) preserves products, since products in C/X\mathcal{C}/X are equivalently pullbacks in C/X\mathcal{C}/X. Pullbacks are also immediately shown to be preserved, since a square in C/X\mathcal{C}/X is a pullback iff it is a pullback in C\mathcal{C}.

Sliced-lex
  : βˆ€ {o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
  β†’ {F : Functor C D} {X : Precategory.Ob C}
  β†’ is-lex F
  β†’ is-lex (Sliced F X)
Sliced-lex {C = C} {D = D} {F = F} {X = X} flex = lex where
  module D = Cat.Reasoning D
  module Dx = Cat.Reasoning (Slice D (F .Fβ‚€ X))
  module C = Cat.Reasoning C
  open is-lex
  lex : is-lex (Sliced F X)
  lex .pres-pullback = pullback-above→pullback-below
                     βŠ™ flex .pres-pullback
                     βŠ™ pullback-belowβ†’pullback-above

That the slice of lex functor preserves the terminal object is slightly more involved, but not by a lot. The gist of the argument is that we know what the terminal object is: It’s the identity map! So we can cheat: Since we know that TT is terminal, we know that Tβ‰…idT \cong {{\mathrm{id}}_{}} β€” but FF preserves this isomorphism, so we have F(T)β‰…F(id)F(T) \cong F({{\mathrm{id}}_{}}). But F(id)F({{\mathrm{id}}_{}}) is id{{\mathrm{id}}_{}} again, now in D\mathcal{D}, so F(T)F(T), being isomorphic to the terminal object, is itself terminal!

  lex .pres-⊀ {T = T} term =
    is-terminal-iso (Slice D (F .Fβ‚€ X))
      (subst (Dx._β‰… cut (F .F₁ (T .map))) (ap cut (F .F-id))
        (F-map-iso (Sliced F X)
          (⊀-unique (Slice C X)
            (record { has⊀ = Slice-terminal-object })
            (record { has⊀ = term }))))
      Slice-terminal-object

Sliced adjointsπŸ”—

A very important property of sliced functors is that, if L⊣RL \dashv R, then R/XR/X is also a right adjoint. The left adjoint isn’t quite L/XL/X, because the types there don’t match, nor is it L/R(x)L/R(x) β€” but it’s quite close. We can adjust that functor by postcomposition with the counit Ξ΅:LR(x)β†’x{\varepsilon}: LR(x) \to xA to get a functor left adjoint to R/XR/X.

Sliced-adjoints
  : βˆ€ {o β„“ oβ€² β„“β€²} {C : Precategory o β„“} {D : Precategory oβ€² β„“β€²}
  β†’ {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) {X : Precategory.Ob D}
  β†’ (Ξ£f (adj .counit .Ξ· _) F∘ Sliced L (R .Fβ‚€ X)) ⊣ Sliced R X
Sliced-adjoints {C = C} {D} {L} {R} adj {X} = adjβ€² where
  module adj = _⊣_ adj
  module L = Functor L
  module R = Functor R
  module C = Cat.Reasoning C
  module D = Cat.Reasoning D

  adjβ€² : (Ξ£f (adj .counit .Ξ· _) F∘ Sliced L (R .Fβ‚€ X)) ⊣ Sliced R X
  adjβ€² .unit .Ξ· x .map = adj.unit.Ξ· _
  adjβ€² .unit .is-natural x y f = /-Hom-path (adj.unit.is-natural _ _ _)
  adjβ€² .counit .Ξ· x .map = adj.counit.Ξ΅ _
  adjβ€² .counit .Ξ· x .commutes = sym (adj.counit.is-natural _ _ _)
  adjβ€² .counit .is-natural x y f = /-Hom-path (adj.counit.is-natural _ _ _)
  adjβ€² .zig = /-Hom-path adj.zig
  adjβ€² .zag = /-Hom-path adj.zag

80% of the adjunction transfers as-is (I didn’t quite count, but the percentage must be way up there β€” just look at the definition above!). The hard part is proving that the adjunction unit restricts to a map in slice categories, which we can compute:

  adjβ€² .unit .Ξ· x .commutes =
    R.₁ (adj.counit.Ξ΅ _ D.∘ L.₁ (x .map)) C.∘ adj.unit.Ξ· _         β‰‘βŸ¨ C.pushl (R.F-∘ _ _) βŸ©β‰‘
    R.₁ (adj.counit.Ξ΅ _) C.∘ R.₁ (L.₁ (x .map)) C.∘ adj.unit.Ξ· _   β‰‘Λ˜βŸ¨ ap (R.₁ _ C.∘_) (adj.unit.is-natural _ _ _) βŸ©β‰‘Λ˜
    R.₁ (adj.counit.Ξ΅ _) C.∘ adj.unit.Ξ· _ C.∘ x .map               β‰‘βŸ¨ C.cancell adj.zag βŸ©β‰‘
    x .map                                                         ∎