module Cat.Displayed.Instances.Subobjects {o ℓ} (B : Precategory o ℓ) where
The fibration of subobjects🔗
Given a base category we can define the displayed category of subobjects over This is, in essence, a restriction of the codomain fibration of but with our attention restricted to the monomorphisms rather than arbitrary maps
record Subobject (y : Ob) : Type (o ⊔ ℓ) where no-eta-equality field {dom} : Ob map : Hom dom y monic : is-monic map open Subobject public
To make formalisation smoother, we define our own version of
displayed morphisms in the subobject fibration, rather than reusing
those of the fundamental self-indexing. The reason for this is quite
technical: the type of maps in the self-indexing is only dependent (the
domains and) the morphisms being considered, meaning nothing
constrains the proofs that these are monomorphisms, causing unification
to fail at the determining the full Subobject
s involved.
record ≤-over {x y} (f : Hom x y) (a : Subobject x) (b : Subobject y) : Type ℓ where no-eta-equality field map : Hom (a .dom) (b .dom) com : f ∘ Subobject.map a ≡ Subobject.map b ∘ map open ≤-over public
We will denote the type of maps in the subobject fibration by since there is at most one such map: if satisfy then, since is a mono,
{-# INLINE Subobject.constructor #-} ≤-over-is-prop : ∀ {x y} {f : Hom x y} {a : Subobject x} {b : Subobject y} → (p q : ≤-over f a b) → p ≡ q ≤-over-is-prop {f = f} {a} {b} p q = path where maps : p .map ≡ q .map maps = b .monic (p .map) (q .map) (sym (p .com) ∙ q .com) path : p ≡ q path i .map = maps i path i .com = is-prop→pathp (λ i → Hom-set _ _ (f ∘ a .map) (b .map ∘ maps i)) (p .com) (q .com) i instance H-Level-≤-over : ∀ {x y} {f : Hom x y} {a : Subobject x} {b : Subobject y} {n} → H-Level (≤-over f a b) (suc n) H-Level-≤-over = prop-instance ≤-over-is-prop
Setting up the displayed category is now nothing more than routine verification: the identity map satisfies and commutative squares can be pasted together.
Subobjects : Displayed B (o ⊔ ℓ) ℓ Subobjects .Ob[_] y = Subobject y Subobjects .Hom[_] = ≤-over Subobjects .Hom[_]-set f a b = hlevel 2 Subobjects .id' .map = id Subobjects .id' .com = id-comm-sym Subobjects ._∘'_ α β .map = α .map ∘ β .map Subobjects ._∘'_ α β .com = pullr (β .com) ∙ extendl (α .com)
Subobjects .idr' _ = prop! Subobjects .idl' _ = prop! Subobjects .assoc' _ _ _ = prop! Subobjects .hom[_] p f .map = f .map Subobjects .hom[_] p f .com = ap₂ _∘_ (sym p) refl ∙ f .com Subobjects .coh[_] p f = prop! open reflects-cartesian-maps open Weak-cocartesian-lift open is-weak-cocartesian open Displayed-functor open is-fibred-functor open Cartesian-lift open is-cartesian open Pullback
The displayed category of subobjects comes with a forgetful vertical functor to the fundamental fibration of
Forget-subobjects : Vertical-functor Subobjects (Slices B) Forget-subobjects .F₀' m = cut (m .map) Forget-subobjects .F₁' f = record { map = f .map ; com = sym (f .com) } Forget-subobjects .F-id' = Slice-path refl Forget-subobjects .F-∘' = Slice-path refl
This functor is fully faithful, hence it reflects cartesian morphisms: a pullback square in determines a cartesian morphism in the subobject fibration. In fact, the uniqueness part follows automatically from the uniqueness of maps in the subobject fibration!
Forget-sub-full : ∀ {a b} {a' : Subobject a} {b' : Subobject b} {f : Hom a b} → Slice-hom B f (Forget-subobjects .F₀' a') (Forget-subobjects .F₀' b') → ≤-over f a' b' Forget-sub-full f' = record { map = f' .map ; com = sym (f' .com) } Forget-sub-reflects-cartesian : reflects-cartesian-maps Forget-subobjects Forget-sub-reflects-cartesian .reflects cart = record { universal = λ m m' → Forget-sub-full (cart .universal m (Forget-subobjects .F₁' m')) ; commutes = λ _ _ → prop! ; unique = λ _ _ → prop! }
pullback→cartesian-sub : ∀ {x y x' y'} {f : Hom x y} {f' : ≤-over f x' y'} → is-pullback B (x' .map) f (f' .map) (y' .map) → is-cartesian Subobjects f f' pullback→cartesian-sub pb = Forget-sub-reflects-cartesian .reflects (pullback→cartesian B pb)
As a fibration🔗
By exactly the same construction as for the fundamental self-indexing, if has pullbacks, the displayed category we have built is actually a fibration. The construction is slightly simpler now that we have no need to worry about uniqueness, but we can remind ourselves of the universal property:
On the first stage, we are given the data in black: we can complete an open span to a Cartesian square (in blue) by pulling back along this base change remains a monomorphism. Since a pullback square is cartesian, we are done.
-- The blue square: pullback-subobject : ∀ {X Y} (h : Hom X Y) (g : Subobject Y) → Subobject X pullback-subobject h g .dom = pb h (g .map) .apex pullback-subobject h g .map = pb h (g .map) .p₁ pullback-subobject h g .monic = mon where abstract mon : is-monic (pb h (g .map) .p₁) mon = is-monic→pullback-is-monic (g .monic) (rotate-pullback (pb h (g .map) .has-is-pb)) Subobject-fibration : Cartesian-fibration Subobjects Subobject-fibration f y' = l where it : Pullback _ _ _ it = pb (y' .map) f l : Cartesian-lift Subobjects f y' l .x' = pullback-subobject f y' l .lifting .map = pb f (y' .map) .p₂ l .lifting .com = pb f (y' .map) .square l .cartesian = Forget-sub-reflects-cartesian .reflects (pullback→cartesian B (pb _ _ .has-is-pb))
As a (weak) cocartesian fibration🔗
If has an image factorisation for every morphism, then its fibration of subobjects is a weak cocartesian fibration. By a general fact, if also has pullbacks, then is a cocartesian fibration.
Subobject-weak-opfibration : (∀ {x y} (f : Hom x y) → Image B f) → Weak-cocartesian-fibration Subobjects Subobject-weak-opfibration ims f x' = l where module im = Image B (ims (f ∘ x' .map))
To understand this result, we remind ourselves of the universal property of an image factorisation for It is the initial subobject through which factors. That is to say, if is another subobject, and for some map then Summarised diagrammatically, the universal property of an image factorisation looks like a kite:
Now compare this with the universal property required of a weak co-cartesian lift:
By smooshing the corner together (i.e., composing and we see that this is exactly the kite-shaped universal property of
l : Weak-cocartesian-lift Subobjects f x' l .y' .dom = im.Im l .y' .map = im.Im→codomain l .y' .monic = im.Im→codomain-is-M l .lifting .map = im.corestrict l .lifting .com = sym im.image-factors l .weak-cocartesian .universal {x' = y'} h .map = im.universal _ (y' .monic) (h .map) (sym (h .com)) l .weak-cocartesian .universal h .com = idl _ ∙ sym im.universal-factors l .weak-cocartesian .commutes g' = prop! l .weak-cocartesian .unique _ _ = prop!
The aforementioned general fact says that any cartesian and weak cocartesian fibration must actually be a full opfibration.
Subobject-opfibration : (∀ {x y} (f : Hom x y) → Image B f) → (pb : has-pullbacks B) → Cocartesian-fibration Subobjects Subobject-opfibration images pb = fibration+weak-opfibration→opfibration _ (with-pullbacks.Subobject-fibration pb) (Subobject-weak-opfibration images)
Subobjects over a base🔗
We define the category of subobjects of as a fibre of the subobject fibration.
Sub : Ob → Precategory (o ⊔ ℓ) ℓ Sub y = Fibre Subobjects y module Sub {y} = Cr (Sub y)
private variable y : Ob m n : Subobject y _≤ₘ_ : ∀ {y} (a b : Subobject y) → Type _ _≤ₘ_ = ≤-over id open Sub renaming (_≅_ to infix 7 _≅ₘ_) using () public infix 7 _≤ₘ_ ≤ₘ→monic : ∀ {y} {a b : Subobject y} → (f : a ≤ₘ b) → is-monic (f .map) ≤ₘ→monic {a = a} f g h α = a .monic g h $ a .map ∘ g ≡⟨ ap (_∘ g) (introl refl ∙ f .com) ∙ pullr refl ⟩≡ _ ∘ f .map ∘ g ≡⟨ ap₂ _∘_ refl α ⟩≡ _ ∘ f .map ∘ h ≡⟨ pulll (sym (f .com) ∙ idl _) ⟩≡ a .map ∘ h ∎ ≤ₘ→mono : ∀ {y} {a b : Subobject y} → a ≤ₘ b → a .dom ↪ b .dom ≤ₘ→mono f .mor = f .map ≤ₘ→mono {a = a} f .monic = ≤ₘ→monic f cutₛ : ∀ {x y} {f : Hom x y} → is-monic f → Subobject y cutₛ x .dom = _ cutₛ x .map = _ cutₛ x .monic = x Sub-antisym : m ≤ₘ n → n ≤ₘ m → m ≅ₘ n Sub-antisym f g = Sub.make-iso f g prop! prop!
There is an evident fully faithful functor from that forgets the property of being monic.
Sub→Slice : ∀ y → Functor (Sub y) (Slice B y) Sub→Slice y .Functor.F₀ m = cut (m .map) Sub→Slice y .Functor.F₁ f = record { map = f .map ; com = sym (f .com) ∙ idl _ } Sub→Slice y .Functor.F-id = ext refl Sub→Slice y .Functor.F-∘ _ _ = ext refl Sub→Slice-is-ff : ∀ y → is-fully-faithful (Sub→Slice y) Sub→Slice-is-ff y = is-iso→is-equiv λ where .is-iso.from m → record { map = m ./-Hom.map ; com = idl _ ∙ sym (m ./-Hom.com) } .is-iso.rinv m → ext refl .is-iso.linv m → prop!
Composing this with the forgetful functor we obtain a projection As both forgetful functors are conservative, so is the projection, which concretely means that we can construct isomorphisms in from isomorphisms in
Sub-cod : ∀ y → Functor (Sub y) B Sub-cod y = Forget/ F∘ Sub→Slice y Sub→Slice-conservative : ∀ y → is-conservative (Sub→Slice y) Sub→Slice-conservative y = is-ff→is-conservative {F = Sub→Slice y} (Sub→Slice-is-ff y) _ Sub-cod-conservative : ∀ y → is-conservative (Sub-cod y) Sub-cod-conservative y = F∘-is-conservative Forget/ (Sub→Slice y) Forget/-is-conservative (Sub→Slice-conservative y) invertible→≅ₘ : (f : m ≤ₘ n) → is-invertible (f .map) → m ≅ₘ n invertible→≅ₘ f inv = Sub.invertible→iso f (Sub-cod-conservative _ inv)
iso→≅ₘ : (is : m .dom ≅ n .dom) → m .map ≡ n .map ∘ is .to → m ≅ₘ n iso→≅ₘ is com = invertible→≅ₘ (record { map = is .to ; com = idl _ ∙ com }) (iso→invertible is) ≅ₘ→iso : m ≅ₘ n → m .dom ≅ n .dom ≅ₘ→iso p = F-map-iso (Sub-cod _) p Sub-path : ∀ {y} {a b : Subobject y} → (p : a .dom ≡ b .dom) → PathP (λ i → Hom (p i) y) (a .map) (b .map) → a ≡ b Sub-path p q i .dom = p i Sub-path p q i .map = q i Sub-path {a = a} {b = b} p q i .monic {c} = is-prop→pathp (λ i → Π-is-hlevel³ 1 λ (g h : Hom c (p i)) (_ : q i ∘ g ≡ q i ∘ h) → Hom-set _ _ g h) (a .monic) (b .monic) i
Fibrewise cartesian structure🔗
Finite products in are created by the projection to in other words, they are computed just like finite products in . We spell them out explicitly.
The greatest element (terminal object) in is given by the identity monomorphism
⊤ₘ : ∀ {y} → Subobject y ⊤ₘ .dom = _ ⊤ₘ .map = id ⊤ₘ .monic = id-monic opaque !ₘ : ∀ {y} {m : Subobject y} → m ≤ₘ ⊤ₘ !ₘ {m = m} = record { map = m .map ; com = refl } Sub-terminal : ∀ {y} → Terminal (Sub y) Sub-terminal .Terminal.top = ⊤ₘ Sub-terminal .Terminal.has⊤ m = contr !ₘ λ _ → prop!
Since products in slice categories are given by pullbacks, and pullbacks preserve monomorphisms, if has pullbacks, then has products, regardless of what is. Given two subobjects we write their product as and think of it as their intersection.
Sub-products : ∀ {y} → has-pullbacks B → has-products (Sub y) Sub-products {y} pb a b = prod where it = pb (a .map) (b .map) prod : Product (Sub y) a b prod .Product.apex .dom = it .apex prod .Product.apex .map = a .map ∘ it .p₁ prod .Product.apex .monic = ∘-is-monic (a .monic) (is-monic→pullback-is-monic (b .monic) (rotate-pullback (it .has-is-pb))) prod .Product.π₁ .map = it .p₁ prod .Product.π₁ .com = idl _ prod .Product.π₂ .map = it .p₂ prod .Product.π₂ .com = idl _ ∙ it .square prod .Product.has-is-product .is-product.⟨_,_⟩ q≤a q≤b .map = it .Pullback.universal {p₁' = q≤a .map} {p₂' = q≤b .map} (sym (q≤a .com) ∙ q≤b .com) prod .Product.has-is-product .is-product.⟨_,_⟩ q≤a q≤b .com = idl _ ∙ sym (pullr (it .p₁∘universal) ∙ sym (q≤a .com) ∙ idl _) prod .Product.has-is-product .is-product.π₁∘⟨⟩ = prop! prod .Product.has-is-product .is-product.π₂∘⟨⟩ = prop! prod .Product.has-is-product .is-product.unique _ _ = prop!
Univalence🔗
Since identity of is given by identity of the underlying objects and identity-over of the corresponding morphisms, if is univalent, we can conclude that is, too. Since is always thin, we can summarise the situation by saying that is a partial order if is univalent.
Sub-is-category : ∀ {y} → is-category B → is-category (Sub y) Sub-is-category b-cat .to-path {a} {b} x = Sub-path (b-cat .to-path i) (Univalent.Hom-pathp-refll-iso b-cat (sym (x .Sub.from .com) ∙ idl _)) where i : a .dom ≅ b .dom i = make-iso (x .Sub.to .map) (x .Sub.from .map) (ap map (Sub.invl x)) (ap map (Sub.invr x)) Sub-is-category b-cat .to-path-over p = Sub.≅-pathp refl _ prop!
As a consequence, the collection of subobjects of any object of a univalent category forms a set.
Subobject-is-set : is-category B → ∀ {A} → is-set (Subobject A) Subobject-is-set b-cat {A} = Poset.Ob-is-set $ thin→poset (Sub A) (λ _ _ → ≤-over-is-prop) (Sub-is-category b-cat)