module Cat.Functor.Subcategory where
Subcategories🔗
A subcategory is specified by a predicate on objects, and a predicate on morphisms between objects within that is closed under identities and composites.
To start, we package up all the data required to define a subcategory up into a record. Note that we omit the requirement that the predicate on objects is a proposition; this tends to be ill-behaved unless the is univalent.
record Subcat (o' ℓ' : Level) : Type (o ⊔ ℓ ⊔ lsuc o' ⊔ lsuc ℓ') where no-eta-equality field is-ob : Ob → Type o' is-hom : ∀ {x y} (f : Hom x y) → is-ob x → is-ob y → Type ℓ' is-hom-prop : ∀ {x y} (f : Hom x y) (px : is-ob x) (py : is-ob y) → is-prop (is-hom f px py) is-hom-id : ∀ {x} → (px : is-ob x) → is-hom id px px is-hom-∘ : ∀ {x y z} {f : Hom y z} {g : Hom x y} → {px : is-ob x} {py : is-ob y} {pz : is-ob z} → is-hom f py pz → is-hom g px py → is-hom (f ∘ g) px pz
Morphisms of wide subcategories are defined as morphisms in where holds.
module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} (subcat : Subcat C o' ℓ') where open Cat.Reasoning C open Subcat subcat record Subcat-hom (x y : Σ[ ob ∈ Ob ] (is-ob ob)) : Type (ℓ ⊔ ℓ') where no-eta-equality constructor sub-hom field hom : Hom (x .fst) (y .fst) witness : subcat .is-hom hom (x .snd) (y .snd) open Subcat-hom
module _ {o ℓ} {C : Precategory o ℓ} where private module C = Precategory C instance Membership-subcat-ob : ∀ {o' ℓ'} → Membership C.Ob (Subcat C o' ℓ') _ Membership-subcat-ob = record { _∈_ = λ o S → o ∈ S .Subcat.is-ob } module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} {S : Subcat C o' ℓ'} where open Cat.Reasoning C open Subcat S Subcat-hom-pathp : {x x' y y' : Σ[ ob ∈ C ] (ob ∈ S)} → {f : Subcat-hom S x y} {g : Subcat-hom S x' y'} → (p : x ≡ x') (q : y ≡ y') → PathP (λ i → Hom (p i .fst) (q i .fst)) (f .hom) (g .hom) → PathP (λ i → Subcat-hom S (p i) (q i)) f g Subcat-hom-pathp p q r i .hom = r i Subcat-hom-pathp {f = f} {g = g} p q r i .witness = is-prop→pathp (λ i → is-hom-prop (r i) (p i .snd) (q i .snd)) (f .witness) (g .witness) i instance Extensional-subcat-hom : ∀ {ℓr x y} ⦃ sa : Extensional (Hom (x .fst) (y .fst)) ℓr ⦄ → Extensional (Subcat-hom S x y) ℓr Extensional-subcat-hom ⦃ sa ⦄ = injection→extensional! (Subcat-hom-pathp refl refl) sa Funlike-Subcat-hom : ∀ {ℓ ℓ'} {A : Type ℓ} {B : A → Type ℓ'} {x y} → ⦃ _ : Funlike (Hom (x .fst) (y .fst)) A B ⦄ → Funlike (Subcat-hom S x y) A B Funlike-Subcat-hom ⦃ i ⦄ = record { _#_ = λ f x → apply (f .hom) x } H-Level-Subcat-hom : ∀ {x y n} → H-Level (Subcat-hom S x y) (2 + n) H-Level-Subcat-hom = basic-instance 2 $ Iso→is-hlevel 2 eqv $ Σ-is-hlevel 2 (Hom-set _ _) λ _ → is-hlevel-suc 1 (is-hom-prop _ _ _) where unquoteDecl eqv = declare-record-iso eqv (quote Subcat-hom)
We can then use this data to construct a category.
module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} (subcat : Subcat C o' ℓ') where open Cat.Reasoning C open Subcat subcat
Subcategory : Precategory (o ⊔ o') (ℓ ⊔ ℓ') Subcategory .Precategory.Ob = ∫ₚ subcat Subcategory .Precategory.Hom = Subcat-hom subcat Subcategory .Precategory.Hom-set _ _ = hlevel 2 Subcategory .Precategory.id .hom = id Subcategory .Precategory.id .witness = is-hom-id _ Subcategory .Precategory._∘_ f g .hom = f .hom ∘ g .hom Subcategory .Precategory._∘_ f g .witness = is-hom-∘ (f .witness) (g .witness) Subcategory .Precategory.idr f = ext (idr _) Subcategory .Precategory.idl f = ext (idl _) Subcategory .Precategory.assoc f g h = ext (assoc _ _ _)
From pseudomonic functors🔗
There is another way of representing subcategories: By giving a faithful functor
module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} {D : Precategory o' ℓ'} {F : Functor C D} (faithful : is-faithful F) where open Functor F private module C = Cat.Reasoning C module D = Cat.Reasoning D
We construct a subcategory from a faithful functor by restricting to the objects in the essential image of and restricting the morphisms to those that lie in the image of
Faithful-subcat : Subcat D (o ⊔ ℓ') (ℓ ⊔ ℓ') Faithful-subcat .Subcat.is-ob x = Essential-fibre F x Faithful-subcat .Subcat.is-hom f (y , y-es) (z , z-es) = Σ[ g ∈ C.Hom y z ] (D.to z-es D.∘ F₁ g D.∘ D.from y-es ≡ f) Faithful-subcat .Subcat.is-hom-prop f (y , y-es) (z , z-es) (g , p) (h , q) = Σ-prop-path! $ faithful $ D.iso→epic (y-es D.Iso⁻¹) _ _ $ D.iso→monic z-es _ _ $ p ∙ sym q Faithful-subcat .Subcat.is-hom-id (y , y-es) = C.id , ap₂ D._∘_ refl (D.eliml F-id) ∙ D.invl y-es Faithful-subcat .Subcat.is-hom-∘ {f = f} {g = g} {x , x-es} {y , y-es} {z , z-es} (h , p) (i , q) = (h C.∘ i) , D.push-inner (F-∘ h i) ·· D.insert-inner (D.invr y-es) ·· ap₂ D._∘_ (sym (D.assoc _ _ _) ∙ p) q
There is an equivalence between canonical subcategory associated with and
Faithful-subcat-domain : Functor (Subcategory Faithful-subcat) C Faithful-subcat-domain .Functor.F₀ (x , x-es) = x-es .fst Faithful-subcat-domain .Functor.F₁ f = f .witness .fst Faithful-subcat-domain .Functor.F-id = refl Faithful-subcat-domain .Functor.F-∘ _ _ = refl Faithful-subcat-domain-is-ff : is-fully-faithful Faithful-subcat-domain Faithful-subcat-domain-is-ff {x = x , x' , x-es} {y = y , y' , y-es} = is-iso→is-equiv $ iso (λ f → sub-hom (D.to y-es D.∘ F₁ f D.∘ D.from x-es) (f , refl)) (λ _ → refl) (λ f → ext (f .witness .snd)) Faithful-subcat-domain-is-split-eso : is-split-eso Faithful-subcat-domain Faithful-subcat-domain-is-split-eso x = (F₀ x , x , D.id-iso) , C.id-iso
There is a faithful functor from a subcategory on to
module _ {o o' ℓ ℓ'} {C : Precategory o ℓ} {S : Subcat C o' ℓ'} where open Cat.Reasoning C private module Sub = Cat.Reasoning (Subcategory S) open Subcat S
Forget-subcat : Functor (Subcategory S) C Forget-subcat .Functor.F₀ (x , _) = x Forget-subcat .Functor.F₁ f = f .hom Forget-subcat .Functor.F-id = refl Forget-subcat .Functor.F-∘ _ _ = refl is-faithful-Forget-subcat : is-faithful Forget-subcat is-faithful-Forget-subcat = ext
Furthermore, if the subcategory contains all of the isomorphisms of then the forgetful functor is pseudomonic.
is-pseudomonic-Forget-subcat : (∀ {x y} {f : Hom x y} {px : x ∈ S} {py : y ∈ S} → is-invertible f → S .is-hom f px py) → is-pseudomonic Forget-subcat is-pseudomonic-Forget-subcat invert .is-pseudomonic.faithful = is-faithful-Forget-subcat is-pseudomonic-Forget-subcat invert .is-pseudomonic.isos-full f = pure $ Sub.make-iso (sub-hom (f .to) (invert (iso→invertible f))) (sub-hom (f .from) (invert (iso→invertible (f Iso⁻¹)))) (ext (f .invl)) (ext (f .invr)) , trivial!
Univalent subcategories🔗
Let be a univalent category. A subcategory of is univalent when the predicate on objects is a proposition.
subcat-iso→iso : ∀ {x y : Σ[ x ∈ Ob ] (x ∈ S)} → x Sub.≅ y → x .fst ≅ y .fst subcat-iso→iso f = make-iso (Sub.to f .hom) (Sub.from f .hom) (ap hom (Sub.invl f)) (ap hom (Sub.invr f)) subcat-is-category : is-category C → (∀ x → is-prop (x ∈ S)) → is-category (Subcategory S) subcat-is-category cat ob-prop .to-path {a , pa} {b , pb} f = Σ-prop-path ob-prop (cat .to-path (subcat-iso→iso f)) subcat-is-category cat ob-prop .to-path-over p = Sub.≅-pathp refl _ $ Subcat-hom-pathp refl _ $ apd (λ _ → to) (cat .to-path-over (subcat-iso→iso p))