module Cat.Functor.Slice where

Slicing functorsπŸ”—

Let be a functor and an object. By a standard tool in category theory (namely β€œwhacking an entire commutative diagram with a functor”), restricts to a functor We call this β€œslicing” the functor This module investigates some of the properties of sliced functors.

Sliced : βˆ€ {o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'}
       β†’ (F : Functor C D) (X : ⌞ 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 = ext (F .F-id)
Sliced F X .F-∘ f g = ext (F .F-∘ _ _)

Faithful, fully faithfulπŸ”—

Slicing preserves faithfulness and fully-faithfulness. It does not preserve fullness: Even if, by fullness, we get a map from a map it does not necessarily restrict to a map in We’d have to show and implies which is possible only if is faithful.

module _ {o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'}
         {F : Functor C D} {X : ⌞ C ⌟} where
    module D = Cat.Reasoning D

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

  Sliced-faithful : is-faithful F β†’ is-faithful (Sliced F X)
  Sliced-faithful faith p = ext (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 = ext (equiv→counit eqv _)
    isom .is-iso.linv x = ext (equiv→unit eqv _)

Left exactnessπŸ”—

If is left exact (meaning it preserves pullbacks and the terminal object), then is lex as well. We note that it (by definition) preserves products, since products in are equivalently pullbacks in Pullbacks are also immediately shown to be preserved, since a square in is a pullback iff it is a pullback in

  : βˆ€ {o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'}
  β†’ {F : Functor C D} {X : ⌞ 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 is terminal, we know that β€” but preserves this isomorphism, so we have But is again, now in so 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) Slice-terminal-object (record { has⊀ = term }))))

Sliced adjointsπŸ”—

A very important property of sliced functors is that, if then is also a right adjoint. The left adjoint isn’t quite because the types there don’t match, nor is it β€” but it’s quite close. We can adjust that functor by postcomposition with the counit to get a functor left adjoint to

  : βˆ€ {o β„“ o' β„“'} {C : Precategory o β„“} {D : Precategory o' β„“'}
  β†’ {L : Functor C D} {R : Functor D C} (adj : L ⊣ R) {X : ⌞ 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.Ξ· _
  adj' .unit .is-natural x y f = ext ( _ _ _)

  adj' .counit .Ξ· x .map         = adj.Ξ΅ _
  adj' .counit .Ξ· x .commutes    = sym ( _ _ _)
  adj' .counit .is-natural x y f = ext ( _ _ _)

  adj' .zig = ext adj.zig
  adj' .zag = ext 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.Ξ΅ _ D.∘ L.₁ (x .map)) C.∘ adj.Ξ· _         β‰‘βŸ¨ C.pushl (R.F-∘ _ _) βŸ©β‰‘
    R.₁ (adj.Ξ΅ _) C.∘ R.₁ (L.₁ (x .map)) C.∘ adj.Ξ· _   β‰‘Λ˜βŸ¨ ap (R.₁ _ C.∘_) ( _ _ _) βŸ©β‰‘Λ˜
    R.₁ (adj.Ξ΅ _) C.∘ adj.Ξ· _ C.∘ x .map               β‰‘βŸ¨ C.cancell adj.zag βŸ©β‰‘
    x .map                                             ∎