module Cat.Restriction.Functor where

Restriction Functors๐Ÿ”—

A functor F:Cโ†’DF : \mathcal{C} \to \mathcal{D} between restriction categories is a restriction functor if F(fโ†“)=(Ff)โ†“F (f^{\downarrow}) = (F f)^{\downarrow}.

  : โˆ€ {oc โ„“c od โ„“d} {C : Precategory oc โ„“c} {D : Precategory od โ„“d}
  โ†’ (F : Functor C D)
  โ†’ (Cโ†“ : Restriction-category C)
  โ†’ (Dโ†“ : Restriction-category D)
  โ†’ Type _
is-restriction-functor {C = C} {D = D} F Cโ†“ Dโ†“ =
  โˆ€ {x y} (f : C.Hom x y) โ†’ F .Fโ‚ (f C.โ†“) โ‰ก (F .Fโ‚ f D.โ†“)
    module C = Cat.Restriction.Reasoning Cโ†“
    module D = Cat.Restriction.Reasoning Dโ†“

The identity functor is a restriction functor, and restriction functors are closed under composition.

  : โˆ€ {oc โ„“c} {C : Precategory oc โ„“c} {Cโ†“ : Restriction-category C}
  โ†’ is-restriction-functor Id Cโ†“ Cโ†“
Id-restriction f = refl

  : โˆ€ {oc โ„“c od โ„“d oe โ„“e}
  โ†’ {C : Precategory oc โ„“c} {D : Precategory od โ„“d} {E : Precategory oe โ„“e}
  โ†’ {Cโ†“ : Restriction-category C}
  โ†’ {Dโ†“ : Restriction-category D}
  โ†’ {Eโ†“ : Restriction-category E}
  โ†’ (F : Functor D E) (G : Functor C D)
  โ†’ is-restriction-functor F Dโ†“ Eโ†“ โ†’ is-restriction-functor G Cโ†“ Dโ†“
  โ†’ is-restriction-functor (F Fโˆ˜ G) Cโ†“ Eโ†“
Fโˆ˜-restriction F G Fโ†“ Gโ†“ f = ap (F .Fโ‚) (Gโ†“ f) โˆ™ Fโ†“ (G .Fโ‚ f)

Properties of Restriction Functors๐Ÿ”—

Let F:Cโ†’DF : \mathcal{C} \to \mathcal{D} be a restriction functor. Note that FF preserves total morphisms and restriction idempotents.

  F-total : โˆ€ {x y} {f : C.Hom x y} โ†’ f โ†’ (F .Fโ‚ f)
  F-total {f = f} f-total = sym (Fโ†“ f) ยทยท ap (F .Fโ‚) f-total ยทยท F .F-id

    : โˆ€ {x} {f : C.Hom x x}
    โ†’ f
    โ†’ (F .Fโ‚ f)
  F-restrict-idem {f = f} f-ridem =
    F .Fโ‚ f D.โ†“   โ‰กห˜โŸจ Fโ†“ f โŸฉโ‰กห˜
    F .Fโ‚ (f C.โ†“) โ‰กโŸจ ap (F .Fโ‚) f-ridem โŸฉโ‰ก
    F .Fโ‚ f โˆŽ

Furthermore, if gg refines ff, then F(g)F(g) refines F(f)F(f).

  F-โ‰ค : โˆ€ {x y} {f g : C.Hom x y} โ†’ f C.โ‰ค g โ†’ (F .Fโ‚ f) D.โ‰ค (F .Fโ‚ g)
  F-โ‰ค {f = f} {g = g} fโ‰คg =
    F .Fโ‚ g D.โˆ˜ F .Fโ‚ f D.โ†“   โ‰กโŸจ ap (F .Fโ‚ g D.โˆ˜_) (sym (Fโ†“ f)) โŸฉโ‰ก
    F .Fโ‚ g D.โˆ˜ F .Fโ‚ (f C.โ†“) โ‰กโŸจ sym (F .F-โˆ˜ g (f C.โ†“)) โŸฉโ‰ก
    F .Fโ‚ (g C.โˆ˜ f C.โ†“) โ‰กโŸจ ap (F .Fโ‚) fโ‰คg โŸฉโ‰ก
    F .Fโ‚ f โˆŽ

Restriction functors also preserve restricted isomorphisms.

    : โˆ€ {x y} {f : C.Hom x y} {g : C.Hom y x}
    โ†’ C.restricted-inverses f g
    โ†’ D.restricted-inverses (F .Fโ‚ f) (F .Fโ‚ g)
  F-restricted-inverses {f = f} {g = g} fg-inv = record
    { โ†“-invl =
      F .Fโ‚ f D.โˆ˜ F .Fโ‚ g โ‰กห˜โŸจ F .F-โˆ˜ f g โŸฉโ‰กห˜
      F .Fโ‚ (f C.โˆ˜ g)     โ‰กโŸจ ap (F .Fโ‚) fg-inv.โ†“-invl โŸฉโ‰ก
      F .Fโ‚ (g C.โ†“)       โ‰กโŸจ Fโ†“ g โŸฉโ‰ก
      F .Fโ‚ g D.โ†“         โˆŽ
    ; โ†“-invr =
      F .Fโ‚ g D.โˆ˜ F .Fโ‚ f โ‰กห˜โŸจ F .F-โˆ˜ g f โŸฉโ‰กห˜
      F .Fโ‚ (g C.โˆ˜ f)     โ‰กโŸจ ap (F .Fโ‚) fg-inv.โ†“-invr โŸฉโ‰ก
      F .Fโ‚ (f C.โ†“)       โ‰กโŸจ Fโ†“ f โŸฉโ‰ก
      F .Fโ‚ f D.โ†“         โˆŽ
    where module fg-inv = C.restricted-inverses fg-inv

    : โˆ€ {x y} {f : C.Hom x y}
    โ†’ f
    โ†’ (F .Fโ‚ f)
  F-restricted-invertible f-inv = record
    { โ†“-inv = F .Fโ‚ f-inv.โ†“-inv
    ; โ†“-inverses = F-restricted-inverses f-inv.โ†“-inverses
    where module f-inv = f-inv

  F-โ†“โ‰… : โˆ€ {x y} โ†’ x C.โ†“โ‰… y โ†’ F .Fโ‚€ x D.โ†“โ‰… F .Fโ‚€ y
  F-โ†“โ‰… f = record
    { โ†“-to = F .Fโ‚ f.โ†“-to
    ; โ†“-from = F .Fโ‚ f.โ†“-from
    ; โ†“-inverses = F-restricted-inverses f.โ†“-inverses
    where module f = C._โ†“โ‰…_ f