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 -small subcategory of a locally -small category (hence a fully faithful functor ) is called dense if objects of are generated under colimits by those of , in a certain canonical way. In particular, any functor and object can be put into a diagram
where is the projection functor from the corresponding comma category, in such a way that the object is the nadir of a cocone over .
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 is called dense if this cocone is colimiting for every . The important of density is that, for a dense functor , 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