module Cat.Functor.Subcategory where

Subcategories🔗

A subcategory $D ↪ C$ is specified by a predicate $P : C \to Prop$ on objects, and a predicate $Q : P (x) \to P (y) \to C (x, y) \to Prop$ on morphisms between objects within $P$ that is closed under identities and composites.

To start, we package up all the data required to define a subcategory up into a record. Note that we omit the requirement that the predicate on objects is a proposition; this tends to be ill-behaved unless the $C$ is univalent.

  record Subcat (o' ℓ' : Level) : Type (o ⊔ ℓ ⊔ lsuc o' ⊔ lsuc ℓ') where
    no-eta-equality
    field
      is-ob : Ob → Type o'
      is-hom : ∀ {x y} (f : Hom x y) → is-ob x → is-ob y → Type ℓ'
      is-hom-prop
        : ∀ {x y} (f : Hom x y) (px : is-ob x) (py : is-ob y)
        → is-prop (is-hom f px py)
      is-hom-id : ∀ {x} → (px : is-ob x) → is-hom id px px
      is-hom-∘
        : ∀ {x y z} {f : Hom y z} {g : Hom x y}
        → {px : is-ob x} {py : is-ob y} {pz : is-ob z}
        → is-hom f py pz → is-hom g px py
        → is-hom (f ∘ g) px pz

Morphisms of wide subcategories are defined as morphisms in $C$ where $Q$ holds.

module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} (subcat : Subcat C o' ℓ') where
  open Cat.Reasoning C
  open Subcat subcat

  record Subcat-hom (x y : Σ[ ob ∈ Ob ] (is-ob ob)) : Type (ℓ ⊔ ℓ') where
    no-eta-equality
    constructor sub-hom
    field
      hom : Hom (x .fst) (y .fst)
      witness : subcat .is-hom hom (x .snd) (y .snd)

open Subcat-hom

We can then use this data to construct a category.

  Subcategory : Precategory (o ⊔ o') (ℓ ⊔ ℓ')
  Subcategory .Precategory.Ob = ∫ₚ subcat
  Subcategory .Precategory.Hom = Subcat-hom subcat
  Subcategory .Precategory.Hom-set _ _ = hlevel 2
  Subcategory .Precategory.id .hom = id
  Subcategory .Precategory.id .witness = is-hom-id _
  Subcategory .Precategory._∘_ f g .hom = f .hom ∘ g .hom
  Subcategory .Precategory._∘_ f g .witness = is-hom-∘ (f .witness) (g .witness)
  Subcategory .Precategory.idr f = ext (idr _)
  Subcategory .Precategory.idl f = ext (idl _)
  Subcategory .Precategory.assoc f g h = ext (assoc _ _ _)

From pseudomonic functors🔗

There is another way of representing subcategories: By giving a faithful functor $F : D ↠ C .$

We construct a subcategory from a faithful functor $F$ by restricting to the objects in the essential image of $F,$ and restricting the morphisms to those that lie in the image of $F .$

  Faithful-subcat : Subcat D (o ⊔ ℓ') (ℓ ⊔ ℓ')
  Faithful-subcat .Subcat.is-ob x = Essential-fibre F x
  Faithful-subcat .Subcat.is-hom f (y , y-es) (z , z-es) =
    Σ[ g ∈ C.Hom y z ] (D.to z-es D.∘ F₁ g D.∘ D.from y-es ≡ f)
  Faithful-subcat .Subcat.is-hom-prop f (y , y-es) (z , z-es) (g , p) (h , q) =
    Σ-prop-path! $
    faithful $
    D.iso→epic (y-es D.Iso⁻¹) _ _ $
    D.iso→monic z-es _ _ $
    p ∙ sym q
  Faithful-subcat .Subcat.is-hom-id (y , y-es) =
    C.id , ap₂ D._∘_ refl (D.eliml F-id) ∙ D.invl y-es
  Faithful-subcat .Subcat.is-hom-∘
    {f = f} {g = g} {x , x-es} {y , y-es} {z , z-es} (h , p) (i , q) =
    (h C.∘ i) ,
    D.push-inner (F-∘ h i)
    ·· D.insert-inner (D.invr y-es)
    ·· ap₂ D._∘_ (sym (D.assoc _ _ _) ∙ p) q

There is an equivalence between canonical subcategory associated with $F$ and $C .$

  Faithful-subcat-domain : Functor (Subcategory Faithful-subcat) C
  Faithful-subcat-domain .Functor.F₀ (x , x-es) = x-es .fst
  Faithful-subcat-domain .Functor.F₁ f = f .witness .fst
  Faithful-subcat-domain .Functor.F-id = refl
  Faithful-subcat-domain .Functor.F-∘ _ _ = refl

  Faithful-subcat-domain-is-ff : is-fully-faithful Faithful-subcat-domain
  Faithful-subcat-domain-is-ff {x = x , x' , x-es} {y = y , y' , y-es} =
    is-iso→is-equiv $ iso
    (λ f → sub-hom (D.to y-es D.∘ F₁ f D.∘ D.from x-es) (f , refl))
    (λ _ → refl)
    (λ f → ext (f .witness .snd))

  Faithful-subcat-domain-is-split-eso : is-split-eso Faithful-subcat-domain
  Faithful-subcat-domain-is-split-eso x =
    (F₀ x , x , D.id-iso) , C.id-iso

There is a faithful functor from a subcategory on $C$ to $C .$

  Forget-subcat : Functor (Subcategory S) C
  Forget-subcat .Functor.F₀ (x , _) = x
  Forget-subcat .Functor.F₁ f = f .hom
  Forget-subcat .Functor.F-id = refl
  Forget-subcat .Functor.F-∘ _ _ = refl

  is-faithful-Forget-subcat : is-faithful Forget-subcat
  is-faithful-Forget-subcat = ext

Furthermore, if the subcategory contains all of the isomorphisms of $C,$ then the forgetful functor is pseudomonic.

  is-pseudomonic-Forget-subcat
    : (∀ {x y} {f : Hom x y} {px : x ∈ S} {py : y ∈ S}
       → is-invertible f → S .is-hom f px py)
    → is-pseudomonic Forget-subcat
  is-pseudomonic-Forget-subcat invert .is-pseudomonic.faithful =
    is-faithful-Forget-subcat
  is-pseudomonic-Forget-subcat invert .is-pseudomonic.isos-full f =
    pure $ Sub.make-iso
      (sub-hom (f .to)   (invert (iso→invertible f)))
      (sub-hom (f .from) (invert (iso→invertible (f Iso⁻¹))))
      (ext (f .invl))
      (ext (f .invr)) , trivial!

Univalent subcategories🔗

Let $C$ be a univalent category. A subcategory of $C$ is univalent when the predicate on objects is a proposition.

  subcat-iso→iso : ∀ {x y : Σ[ x ∈ Ob ] (x ∈ S)} → x Sub.≅ y → x .fst ≅ y .fst
  subcat-iso→iso f = make-iso (Sub.to f .hom) (Sub.from f .hom)
    (ap hom (Sub.invl f)) (ap hom (Sub.invr f))

  subcat-is-category
    : is-category C
    → (∀ x → is-prop (x ∈ S))
    → is-category (Subcategory S)
  subcat-is-category cat ob-prop .to-path {a , pa} {b , pb} f =
    Σ-prop-path ob-prop (cat .to-path (subcat-iso→iso f))
  subcat-is-category cat ob-prop .to-path-over p =
    Sub.≅-pathp refl _ $
    Subcat-hom-pathp refl _ $
    apd (λ _ → to) (cat .to-path-over (subcat-iso→iso p))