module Cat.Functor.FullSubcategory {o h} {C : Precategory o h} where
Full subcategoriesπ
A full subcategory of some larger category is the category generated by some predicate on the objects of of You keep only those objects for which holds, and all the morphisms between them. An example is the category of abelian groups, as a full subcategory of groups: being abelian is a proposition (thereβs βat most one way for a group to be abelianβ).
We can interpret full subcategories, by analogy, as being the βinduced subgraphsβ of the categorical world: Keep only some of the vertices (objects), but all of the arrows (arrows) between them.
record Restrict-ob (P : C.Ob β Type β) : Type (o β β) where no-eta-equality constructor restrict field object : C.Ob witness : P object open Restrict-ob public Restrict : (P : C.Ob β Type β) β Precategory (o β β) h Restrict P .Ob = Restrict-ob P Restrict P .Hom A B = C.Hom (A .object) (B .object) Restrict P .Hom-set _ _ = C.Hom-set _ _ Restrict P .id = C.id Restrict P ._β_ = C._β_ Restrict P .idr = C.idr Restrict P .idl = C.idl Restrict P .assoc = C.assoc
Restrict-ob-path : β {P : C.Ob β Type β} β {x y : Restrict-ob P} β (p : x .object β‘ y .object) β PathP (Ξ» i β P (p i)) (x .witness) (y .witness) β x β‘ y Restrict-ob-path p q i .object = p i Restrict-ob-path p q i .witness = q i
A very important property of full subcategories (Restrict
ions) is that any
full subcategory of a univalent category is
univalent. The argument is roughly as follows: Since
is univalent, an isomorphism
gives us a path
so in particular if we know
and
then we have
But, since the morphisms in the full subcategory coincide with those of
any iso in the subcategory is an iso in
thus a path!
module _ (P : C.Ob β Type β) where import Cat.Reasoning (Restrict P) as R
We begin by translating between isomorphisms in the subcategory (called here) and in which can be done by destructuring and reassembling:
sub-isoβsuper-iso : β {A B : Restrict-ob P} β (A R.β B) β (A .object C.β B .object) sub-isoβsuper-iso x = C.make-iso x.to x.from x.invl x.invr where module x = R._β _ x super-isoβsub-iso : β {A B : Restrict-ob P} β (A .object C.β B .object) β (A R.β B) super-isoβsub-iso y = R.make-iso y.to y.from y.invl y.invr where module y = C._β _ y
module _ (P : C.Ob β Type β) (pprop : β x β is-prop (P x)) where import Cat.Reasoning (Restrict P) as R
We then prove that object-isomorphism pairs in the subcategory (i.e. inhabitants of coincide with those in the supercategory; Hence, since is by assumption univalent, so is
Restrict-is-category : is-category C β is-category (Restrict P) Restrict-is-category cids = Ξ» where .to-path im i .object β Univalent.isoβpath cids (sub-isoβsuper-iso P im) i .to-path {a = a} {b = b} im i .witness β is-propβpathp (Ξ» i β pprop (cids .to-path (sub-isoβsuper-iso P im) i)) (a .witness) (b .witness) i .to-path-over p β R.β -pathp _ _ Ξ» i β cids .to-path-over (sub-isoβsuper-iso P p) i .C.to
From full inclusionsπ
There is another way of representing full subcategories: By giving a full inclusion, i.e.Β a fully faithful functor Each full inclusion canonically determines a full subcategory of namely that consisting of the objects in merely in the image of
module _ {o' h'} {D : Precategory o' h'} {F : Functor D C} (ff : is-fully-faithful F) where open Functor F Full-inclusionβFull-subcat : Precategory _ _ Full-inclusionβFull-subcat = Restrict (Ξ» x β β[ d β Ob D ] (Fβ d C.β x))
This canonical full subcategory is weakly equivalent to meaning that it admits a fully faithful, essentially surjective functor from This functor is actually just again:
Ff-domainβFull-subcat : Functor D Full-inclusionβFull-subcat Ff-domainβFull-subcat .Functor.Fβ x = restrict (Fβ x) (inc (x , C.id-iso)) Ff-domainβFull-subcat .Functor.Fβ = Fβ Ff-domainβFull-subcat .Functor.F-id = F-id Ff-domainβFull-subcat .Functor.F-β = F-β is-fully-faithful-domainβFull-subcat : is-fully-faithful Ff-domainβFull-subcat is-fully-faithful-domainβFull-subcat = ff is-eso-domainβFull-subcat : is-eso Ff-domainβFull-subcat is-eso-domainβFull-subcat yo = β₯-β₯-map (Ξ» (preimg , isom) β preimg , super-isoβsub-iso _ isom) (yo .witness)
Up to weak equivalence, admitting a full inclusion is equivalent to being a full subcategory: Every full subcategory admits a full inclusion, given on objects by projecting the first component and on morphisms by the identity function.
module _ {P : C.Ob β Type β} where Forget-full-subcat : Functor (Restrict P) C Forget-full-subcat .Functor.Fβ = object Forget-full-subcat .Functor.Fβ f = f Forget-full-subcat .Functor.F-id = refl Forget-full-subcat .Functor.F-β f g i = f C.β g is-fully-faithful-Forget-full-subcat : is-fully-faithful Forget-full-subcat is-fully-faithful-Forget-full-subcat = id-equiv