open import Cat.Prelude
open import Cat.Univalent

open import Order.Base

import Cat.Reasoning

module Order.Instances.Subobjects where

Posets of subobjectsπŸ”—

Let C\mathcal{C} be a category and A:CA : \mathcal{C} an arbitrary object. We’re interested here in the restriction of the slice category C/A\mathcal{C}/A to those objects whose map is a monomorphism. This restriction turns out to be a poset.

Here’s why: First, we define the ≀\le relation β€œas usual”, i.e., X≀YX \le Y consists of the commuting triangles as in the diagram below.

  Subobjects : C.Ob β†’ Poset _ _
  Subobjects A = to-poset (Ξ£ C.Ob Ξ» B β†’ B C.β†ͺ A) mk where
    open make-poset

    mk : make-poset β„“ (Ξ£ (C .Precategory.Ob) (Ξ» B β†’ B C.β†ͺ A))
    mk .rel (B , f) (C , h) = Ξ£ (C.Hom B C) Ξ» g β†’ h .mor C.∘ g ≑ f .mor
    mk .id = C.id , C.idr _
    mk .trans (f , Ξ±) (g , Ξ²) = g C.∘ f , C.pulll Ξ² βˆ™ Ξ±

The first thing we must verify is that this is indeed a proposition: there is at most one such triangle. Why? Well, YY is a monomorphism! Suppose we have f,f′:B→Cf, f' : B \to C as in the diagram. Then we have Yf=g=Yf′Yf = g = Yf', so f=f′f = f'.

    mk .thin {y = y} (f , Ξ±) (g , Ξ²) = Ξ£-prop-path! (y .snd .monic _ _ (Ξ± βˆ™ sym Ξ²))

Now, it’s certainly not the case that you can get an isomorphism Aβ‰…BA \cong B from any ol’ pair of morphisms f:Aβ†’Bf : A \to B and g:Bβ†’Ag : B \to A. But if we’re talking morphisms in a slice between monomorphisms, then we have a much better shot: Instead of having to show fg=idfg = {{\mathrm{id}}_{}} (hard), we can show Yfg=YYfg = Y, which follows from commutativity of the triangles. So the subjects of AA are a poset!

    mk .antisym {X , x} {Y , y} (f , Ξ±) (g , Ξ²) =
      Ξ£-pathp (c-cat .to-path im) (C.β†ͺ-pathp (Univalent.Hom-pathp-refll-iso c-cat Ξ²))
      where
        im : X C.β‰… Y
        im = C.make-iso f g (y .monic _ _ (C.pulll Ξ± Β·Β· Ξ² Β·Β· C.intror refl))
                            (x .monic _ _ (C.pulll Ξ² Β·Β· Ξ± Β·Β· C.intror refl))