open import Cat.Instances.Shape.Terminal
open import Cat.Diagram.Colimit.Base
open import Cat.Functor.Properties
open import Cat.Functor.Kan.Nerve
open import Cat.Instances.Comma
open import Cat.Prelude

import Cat.Functor.Reasoning as Fr

module Cat.Functor.Dense where


# Dense subcategoriesπ

A $\kappa$-small subcategory $\mathcal{C} \sube \mathcal{D}$ of a locally $\kappa$-small category $\mathcal{D}$ (hence a fully faithful functor $F : \mathcal{C} \hookrightarrow \mathcal{D}$) is called dense if objects of $\mathcal{D}$ are generated under colimits by those of $\mathcal{C}$, in a certain canonical way. In particular, any functor $F$ and object $d : \mathcal{D}$ can be put into a diagram

$J : (F \searrow d) \xrightarrow{\mathrm{pr}} C \xrightarrow{F} D\text{,}$

where $(F \searrow d) \to C$ is the projection functor from the corresponding comma category, in such a way that the object $d$ is the nadir of a cocone over $J$.

module
_ {o β} {C : Precategory β β} {D : Precategory o β} (F : Functor C D)
where
open Functor
open βObj
open βHom
open _=>_

private
module C = Precategory C
module D = Precategory D
module F = Fr F

  dense-cocone : β d β F Fβ Dom F (const! d) => Const d
dense-cocone d .Ξ· x = x .map
dense-cocone d .is-natural _ _ f = f .sq

is-dense : Type _
is-dense = β d β is-colimit {J = F β d} (F Fβ Dom _ _) d (dense-cocone d)


The functor $F$ is called dense if this cocone is colimiting for every $d : \mathcal{D}$. The importance of density is that, for a dense functor $F$, the induced nerve functor is fully faithful.

  is-denseβnerve-is-ff : is-dense β is-fully-faithful (Nerve F)
is-denseβnerve-is-ff is-dense = is-isoβis-equiv $iso inv invr invl where module is-dense d = is-colimit (is-dense d) inv : β {x y} β (Nerve F .Fβ x => Nerve F .Fβ y) β D.Hom x y inv nt = is-dense.universal _ (Ξ» j β nt .Ξ· _ (j .map)) Ξ» f β sym (nt .is-natural _ _ _$β _) β ap (nt .Ξ· _) (f .sq β D.idl _)

invr : β {x y} (f : Nerve F .Fβ x => Nerve F .Fβ y) β Nerve F .Fβ (inv f) β‘ f
invr f = ext Ξ» x i β is-dense.factors _ {j = βobj i} _ _

invl : β {x y} (f : D.Hom x y) β inv (Nerve F .Fβ f) β‘ f
invl f = sym $is-dense.unique _ _ _ f (Ξ» _ β refl)  Another way of putting this is that probes by a dense subcategory are enough to tell morphisms (and so objects) in the ambient category apart.  denseβseparating : is-dense β {X Y : D.Ob} {f g : D.Hom X Y} β (β {Z} (h : D.Hom (F.β Z) X) β f D.β h β‘ g D.β h) β f β‘ g denseβseparating dense h = fully-faithfulβfaithful {F = Nerve F} (is-denseβnerve-is-ff dense)$
ext Ξ» x g β h g