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

import Cat.Functor.Reasoning as Fr
import Cat.Reasoning as Cr

module Cat.Functor.Dense where

Dense subcategoriesπŸ”—

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

J:(Fβ†˜d)β†’prCβ†’ΞΉD, J : (F \searrow d) {\xrightarrow{\mathrm{pr}}} C {\xrightarrow{\iota}} D\text{,}

where (ΞΉβ†˜d)β†’C(\iota \searrow d) \to C is the projection functor from the corresponding comma category, in such a way that the object dd is the nadir of a cocone over JJ.

  is-dense : Type _
  is-dense = βˆ€ d β†’ is-colimit {J = F β†˜ d} (F F∘ Dom _ _) $ Ξ» where
    .coapex     β†’ d
    .ψ x        β†’ x .map
    .commutes f β†’ f .sq βˆ™ D.idl _

The functor FF is called dense if this cocone is colimiting for every d:Dd : \mathcal{D}. The important of density is that, for a dense functor FF, 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-colim = is-iso→is-equiv $ iso inv invr invl where
    ntβ†’cone : βˆ€ {x y} β†’ (Nerve F .Fβ‚€ x => Nerve F .Fβ‚€ y) β†’ Cocone _
    nt→cone {x} {y} nt .coapex = y
    ntβ†’cone {x} {y} nt .ψ o = nt .Ξ· _ (o .map)
    nt→cone {x} {y} nt .commutes {γ} {δ} f =
      nt .Ξ· _ (Ξ΄ .map) D.∘ F.₁ (f .Ξ±)   β‰‘Λ˜βŸ¨ nt .is-natural _ _ _ $β‚š _ βŸ©β‰‘Λ˜
      nt .Ξ· _ ⌜ Ξ΄ .map D.∘ F.₁ (f .Ξ±) ⌝ β‰‘βŸ¨ ap! (f .sq βˆ™ D.idl _) βŸ©β‰‘
      nt .η _ (γ .map)                  ∎

    inv : βˆ€ {x y} β†’ (Nerve F .Fβ‚€ x => Nerve F .Fβ‚€ y) β†’ D.Hom x y
    inv {x} {y} nt = is-colim x (nt→cone nt) .centre .hom

    invr : βˆ€ {x y} (f : Nerve F .Fβ‚€ x => Nerve F .Fβ‚€ y) β†’ Nerve F .F₁ (inv f) ≑ f
    invr f = Nat-path Ξ» x β†’ funext Ξ» i β†’
      is-colim _ (nt→cone f) .centre .commutes record { map = i }

    invl : βˆ€ {x y} (f : D.Hom x y) β†’ inv (Nerve F .F₁ f) ≑ f
    invl f = ap hom $ is-colim _ (nt→cone _) .paths $ λ where
      .hom        β†’ f
      .commutes o β†’ 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) $
      Nat-path Ξ» x β†’ funext Ξ» g β†’ h g