module Cat.Functor.FullSubcategory {o h} {C : Precategory o h} where

Full subcategoriesπŸ”—

A full subcategory of some larger category is the category generated by some predicate on the objects of of You keep only those objects for which holds, and all the morphisms between them. An example is the category of abelian groups, as a full subcategory of groups: being abelian is a proposition (there’s β€œat most one way for a group to be abelian”).

We can interpret full subcategories, by analogy, as being the β€œinduced subgraphs” of the categorical world: Keep only some of the vertices (objects), but all of the arrows (arrows) between them.

record Restrict-ob (P : C.Ob β†’ Type β„“) : Type (o βŠ” β„“) where
  no-eta-equality
  constructor restrict
  field
    object  : C.Ob
    witness : P object

open Restrict-ob public

Restrict : (P : C.Ob β†’ Type β„“) β†’ Precategory (o βŠ” β„“) h
Restrict P .Ob = Restrict-ob P
Restrict P .Hom A B = C.Hom (A .object) (B .object)
Restrict P .Hom-set _ _ = C.Hom-set _ _
Restrict P .id    = C.id
Restrict P ._∘_   = C._∘_
Restrict P .idr   = C.idr
Restrict P .idl   = C.idl
Restrict P .assoc = C.assoc

A very important property of full subcategories (Restrictions) is that any full subcategory of a univalent category is univalent. The argument is roughly as follows: Since is univalent, an isomorphism gives us a path so in particular if we know and then we have But, since the morphisms in the full subcategory coincide with those of any iso in the subcategory is an iso in thus a path!

module _ (P : C.Ob β†’ Type β„“) where
  import Cat.Reasoning (Restrict P) as R

We begin by translating between isomorphisms in the subcategory (called here) and in which can be done by destructuring and reassembling:

  sub-isoβ†’super-iso : βˆ€ {A B : Restrict-ob P} β†’ (A R.β‰… B) β†’ (A .object C.β‰… B .object)
  sub-iso→super-iso x = C.make-iso x.to x.from x.invl x.invr
    where module x = R._β‰…_ x

  super-isoβ†’sub-iso : βˆ€ {A B : Restrict-ob P} β†’ (A .object C.β‰… B .object) β†’ (A R.β‰… B)
  super-iso→sub-iso y = R.make-iso y.to y.from y.invl y.invr
    where module y = C._β‰…_ y
module _ (P : C.Ob β†’ Type β„“) (pprop : βˆ€ x β†’ is-prop (P x))
  where
  import Cat.Reasoning (Restrict P) as R

We then prove that object-isomorphism pairs in the subcategory (i.e. inhabitants of coincide with those in the supercategory; Hence, since is by assumption univalent, so is

  Restrict-is-category : is-category C β†’ is-category (Restrict P)
  Restrict-is-category cids = Ξ» where
    .to-path im i .object → Univalent.iso→path cids (sub-iso→super-iso P im) i
    .to-path {a = a} {b = b} im i .witness → is-prop→pathp
      (λ i → pprop (cids .to-path (sub-iso→super-iso P im) i))
      (a .witness) (b .witness) i
    .to-path-over p → R.≅-pathp _ _ λ i → cids .to-path-over (sub-iso→super-iso P p) i .C.to

From full inclusionsπŸ”—

There is another way of representing full subcategories: By giving a full inclusion, i.e.Β a fully faithful functor Each full inclusion canonically determines a full subcategory of namely that consisting of the objects in merely in the image of

module _ {o' h'} {D : Precategory o' h'} {F : Functor D C} (ff : is-fully-faithful F) where
  open Functor F

  Full-inclusion→Full-subcat : Precategory _ _
  Full-inclusion→Full-subcat =
    Restrict (Ξ» x β†’ βˆƒ[ d ∈ Ob D ] (Fβ‚€ d C.β‰… x))

This canonical full subcategory is weakly equivalent to meaning that it admits a fully faithful, essentially surjective functor from This functor is actually just again:

  Ff-domain→Full-subcat : Functor D Full-inclusion→Full-subcat
  Ff-domain→Full-subcat .Functor.F₀ x = restrict (F₀ x) (inc (x , C.id-iso))
  Ff-domainβ†’Full-subcat .Functor.F₁ = F₁
  Ff-domain→Full-subcat .Functor.F-id = F-id
  Ff-domainβ†’Full-subcat .Functor.F-∘ = F-∘

  is-fully-faithful-domain→Full-subcat : is-fully-faithful Ff-domain→Full-subcat
  is-fully-faithful-domain→Full-subcat = ff

  is-eso-domain→Full-subcat : is-eso Ff-domain→Full-subcat
  is-eso-domain→Full-subcat yo =
    βˆ₯-βˆ₯-map (Ξ» (preimg , isom) β†’ preimg , super-isoβ†’sub-iso _ isom)
      (yo .witness)

Up to weak equivalence, admitting a full inclusion is equivalent to being a full subcategory: Every full subcategory admits a full inclusion, given on objects by projecting the first component and on morphisms by the identity function.

module _ {P : C.Ob β†’ Type β„“} where
  Forget-full-subcat : Functor (Restrict P) C
  Forget-full-subcat .Functor.Fβ‚€ = object
  Forget-full-subcat .Functor.F₁ f = f
  Forget-full-subcat .Functor.F-id = refl
  Forget-full-subcat .Functor.F-∘ f g i = f C.∘ g

  is-fully-faithful-Forget-full-subcat : is-fully-faithful Forget-full-subcat
  is-fully-faithful-Forget-full-subcat = id-equiv