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

Wide subcategoriesπŸ”—

A wide subcategory Dβ†ͺC\mathcal{D} \hookrightarrow \mathcal{C} is specified by a predicate PP on the morphisms of C\mathcal{C}, rather than one on the objects. Since PP is nontrivial, we must take care that the result actually form a category: PP must contain the identities and be closed under composition.

To start, we package up all the data required to define a wide subcategory up into a record.

record Wide-subcat (β„“ : Level) : Type (o βŠ” h βŠ” lsuc β„“) where
    P      : βˆ€ {x y} β†’ C.Hom x y β†’ Type β„“
    P-prop : βˆ€ {x y} (f : C.Hom x y) β†’ is-prop (P f)

    P-id : βˆ€ {x} β†’ P ( {x})
    P-∘  : βˆ€ {x y z} {f : C.Hom y z} {g : C.Hom x y}
         β†’ P f β†’ P g β†’ P (f C.∘ g)

open Wide-subcat

Morphisms of wide subcategories are defined as morphisms in C\mathcal{C} where PP holds.

record Wide-hom (sub : Wide-subcat β„“) (x y : C.Ob) : Type (h βŠ” β„“) where
  constructor wide
    hom : C.Hom x y
    witness : sub .P hom

We can then use this data to construct a category.

Wide : Wide-subcat β„“ β†’ Precategory o (h βŠ” β„“)
Wide sub .Ob = C.Ob
Wide sub .Hom         = Wide-hom sub
Wide sub .Hom-set _ _ = Wide-hom-is-set

Wide sub .id .hom     =
Wide sub .id .witness = sub .P-id

Wide sub ._∘_ f g .hom     = f .hom C.∘ g .hom
Wide sub ._∘_ f g .witness = sub .P-∘ (f .witness) (g .witness)

Wide sub .idr _ = Wide-hom-path $ C.idr _
Wide sub .idl _ = Wide-hom-path $ C.idl _
Wide sub .assoc _ _ _ = Wide-hom-path $ C.assoc _ _ _

From split essentially surjective inclusionsπŸ”—

There is another way of representing wide subcategories: By giving a pseudomonic split essentially surjection F:D↠CF : \mathcal{D} \twoheadrightarrow \mathcal{C}.

We construct the wide subcategory by restricting to the morphisms in C\mathcal{C} that lie in the image of FF. Since FF is a faithful functor, this is indeed a proposition.

  Split-eso-inclusion→Wide-subcat : Precategory _ _
  Split-eso-inclusion→Wide-subcat = Wide sub where
    sub : Wide-subcat (h βŠ” h')
    sub .P {x = x} {y = y} f =
      Σ[ g ∈ D.Hom (eso x .fst) (eso y .fst) ]
      ( y C.∘ F₁ g C.∘ eso.from x ≑ f)
    sub .P-prop {x} {y} f (g , p) (g' , q) =
      Ξ£-prop-path (Ξ» _ β†’ C.Hom-set _ _ _ _) $
      is-pseudomonic.faithful pseudomonic   $
      C.isoβ†’epic (eso x .snd C.Iso⁻¹) _ _   $
      C.isoβ†’monic (eso y .snd) _ _ (p βˆ™ sym q)
    sub .P-id {x} =
      ( , apβ‚‚ C._∘_ refl (C.eliml F-id) βˆ™ C.invl (eso x .snd))
    sub .P-∘ {x} {y} {z} {f} {g} (f' , p) (g' , q) =
      f' D.∘ g' , ( z C.∘ F₁ (f' D.∘ g') C.∘ eso.from x                                    β‰‘βŸ¨ C.push-inner (F-∘ f' g') βŸ©β‰‘
        ( z C.∘ F₁ f') C.∘ (F₁ g' C.∘ eso.from x)                               β‰‘βŸ¨ C.insert-inner (eso.invr y) βŸ©β‰‘
        (( z C.∘ F₁ f') C.∘ eso.from y) C.∘ ( y C.∘ F₁ g' C.∘ eso.from x) β‰‘βŸ¨ apβ‚‚ C._∘_ (sym (C.assoc _ _ _) βˆ™ p) q βŸ©β‰‘
        f C.∘ g ∎)

This canonical wide subcategory is equivalent to D\mathcal{D}.

  Wide-subcat→Split-eso-domain : Functor (Split-eso-inclusion→Wide-subcat) D
  Wide-subcat→Split-eso-domain .Functor.F₀ x = eso x .fst
  Wide-subcatβ†’Split-eso-domain .Functor.F₁ f = f .witness .fst
  Wide-subcat→Split-eso-domain .Functor.F-id = refl
  Wide-subcatβ†’Split-eso-domain .Functor.F-∘ _ _ = refl

  is-fully-faithful-Wide-subcat→domain : is-fully-faithful Wide-subcat→Split-eso-domain
  is-fully-faithful-Wide-subcat→domain = is-iso→is-equiv $ iso
    (Ξ» f β†’ wide ( _ C.∘ F₁ f C.∘ eso.from _) (f , refl))
    (Ξ» _ β†’ refl)
    (Ξ» f β†’ Wide-hom-path (f .witness .snd))

  is-eso-Wide-subcat→domain : is-split-eso Wide-subcat→Split-eso-domain
  is-eso-Wide-subcat→domain x =
    F₀ x , pseudomonic→essentially-injective pseudomonic (eso (F₀ x) .snd)

We did cheat a bit earlier when defining wide subcategories: our predicate isn’t required to respect isomorphisms! This means that we could form a β€œsubcategory” that kills off all the isomorphisms, which allows us to distinguish between isomorphic objects. Therefore, wide subcategories are not invariant under equivalence of categories.

This in turn means that the forgetful functor from a wide subcategory is not pseudomonic! To ensure that it is, we need to require that the predicate holds on all isomorphisms. Arguably this is something that should be part of the definition of a wide subcategory, but it isn’t strictly required, so we opt to leave it as a side condition.

  Forget-wide-subcat : Functor (Wide sub) C
  Forget-wide-subcat .Functor.Fβ‚€ x = x
  Forget-wide-subcat .Functor.F₁ f = f .hom
  Forget-wide-subcat .Functor.F-id = refl
  Forget-wide-subcat .Functor.F-∘ _ _ = refl

  is-faithful-Forget-wide-subcat : is-faithful Forget-wide-subcat
  is-faithful-Forget-wide-subcat = Wide-hom-path

    : (P-invert : βˆ€ {x y} {f : C.Hom x y} β†’ f β†’ sub .P f)
    β†’ is-pseudomonic Forget-wide-subcat
  is-pseudomonic-Forget-wide-subcat P-invert .is-pseudomonic.faithful =
  is-pseudomonic-Forget-wide-subcat P-invert .is-pseudomonic.isos-full f =
    pure $
        (wide (P-invert (C.iso→invertible f)))
        (wide f.from (P-invert (C.isoβ†’invertible (f C.Iso⁻¹))))
        (Wide-hom-path f.invl)
        (Wide-hom-path f.invr) ,
      C.β‰…-pathp refl refl refl
    where module f = C._β‰…_ f

  is-split-eso-Forget-wide-subcat : is-split-eso Forget-wide-subcat
  is-split-eso-Forget-wide-subcat y = y ,