module Cat.Diagram.Pullback.Properties {o β„“} {C : Precategory o β„“} where

Properties of pullbacksπŸ”—

This module chronicles some general properties of pullbacks.

Pasting lawπŸ”—

The pasting law for pullbacks says that, if in the commutative diagram below the the right square is a pullback, then the left square is universal if, and only if, the outer rectangle is, too. Note the emphasis on the word commutative: if we don’t know that both squares (and the outer rectangle) all commute, the pasting law does not go through.

module _ {a b c d e f : Ob}
         {a→d : Hom a d} {a→b : Hom a b} {b→c : Hom b c}
         {d→e : Hom d e} {b→e : Hom b e} {e→f : Hom e f}
         {c→f : Hom c f}
         (right-pullback : is-pullback b→c c→f b→e e→f)
  where

  private module right = is-pullback right-pullback

Let’s start with proving that, if the outer rectangle is a pullback, then so is the left square. Assume, then, that we have some other object which fits into a cone, like in the diagram below. I’ve coloured the two arrows we assume commutative.

  pasting-outer→left-is-pullback
    : is-pullback (bβ†’c ∘ aβ†’b) cβ†’f aβ†’d (eβ†’f ∘ dβ†’e)
    β†’ (square : bβ†’e ∘ aβ†’b ≑ dβ†’e ∘ aβ†’d)
    → is-pullback a→b b→e a→d d→e
  pasting-outer→left-is-pullback outer square = pb where
    module outer = is-pullback outer

To appeal to the universal property of the outer pullback, we must somehow extend our red cone over to one over Can we do this? Yes! By assumption, the square on the right commutes, which lets us apply commutativity of the red diagram (the assumption in the code). Check out the calculation below:

    abstract
      path : βˆ€ {P} {Pβ†’b : Hom P b} {Pβ†’d : Hom P d} (p : bβ†’e ∘ Pβ†’b ≑ dβ†’e ∘ Pβ†’d)
           β†’ cβ†’f ∘ bβ†’c ∘ Pβ†’b ≑ (eβ†’f ∘ dβ†’e) ∘ Pβ†’d
      path {_} {P→b} {P→d} p =
        cβ†’f ∘ bβ†’c ∘ Pβ†’b   β‰‘βŸ¨ extendl right.square βŸ©β‰‘
        eβ†’f ∘ bβ†’e ∘ Pβ†’b   β‰‘βŸ¨ ap (eβ†’f ∘_) p βŸ©β‰‘
        eβ†’f ∘ dβ†’e ∘ Pβ†’d   β‰‘βŸ¨ cat! C βŸ©β‰‘
        (eβ†’f ∘ dβ†’e) ∘ Pβ†’d ∎

    pb : is-pullback _ _ _ _
    pb .is-pullback.square =
      bβ†’e ∘ aβ†’b β‰‘βŸ¨ square βŸ©β‰‘
      dβ†’e ∘ aβ†’d ∎

We thus have an induced map which, since is a pullback, makes everything in sight commute, and does so uniquely.

    pb .universal {p₁' = Pβ†’b} {pβ‚‚' = Pβ†’d} p =
      outer.universal {p₁' = bβ†’c ∘ Pβ†’b} {pβ‚‚' = Pβ†’d} (path p)

    pb .pβ‚βˆ˜universal {p₁' = Pβ†’b} {pβ‚‚' = Pβ†’d} {p = p} =
      right.uniqueβ‚‚ {p = pulll right.square βˆ™ pullr p}
        (assoc _ _ _ βˆ™ outer.pβ‚βˆ˜universal)
        (pulll square βˆ™ pullr outer.pβ‚‚βˆ˜universal)
        refl p

    pb .pβ‚‚βˆ˜universal {p₁' = Pβ†’b} {pβ‚‚' = Pβ†’d} {p = p} = outer.pβ‚‚βˆ˜universal

    pb .unique {p = p} q r =
      outer.unique (sym (ap (_ ∘_) (sym q) βˆ™ assoc _ _ _)) r

For the converse, suppose that both small squares are a pullback, and we have a cone over By the universal property of the right pullback, we can find a map forming the left leg of a cone over By the universal property of the left square, we then have a map as we wanted.

  pasting-left→outer-is-pullback
    : is-pullback a→b b→e a→d d→e
    β†’ (square : cβ†’f ∘ bβ†’c ∘ aβ†’b ≑ (eβ†’f ∘ dβ†’e) ∘ aβ†’d)
    β†’ is-pullback (bβ†’c ∘ aβ†’b) cβ†’f aβ†’d (eβ†’f ∘ dβ†’e)
  pasting-left→outer-is-pullback left square = pb where
    module left = is-pullback left

    pb : is-pullback (bβ†’c ∘ aβ†’b) cβ†’f aβ†’d (eβ†’f ∘ dβ†’e)
    pb .is-pullback.square =
      cβ†’f ∘ bβ†’c ∘ aβ†’b   β‰‘βŸ¨ square βŸ©β‰‘
      (eβ†’f ∘ dβ†’e) ∘ aβ†’d ∎
    pb .universal {p₁' = Pβ†’c} {pβ‚‚' = Pβ†’d} x =
      left.universal {p₁' = right.universal (x βˆ™ sym (assoc _ _ _))} {pβ‚‚' = Pβ†’d}
        right.pβ‚‚βˆ˜universal
    pb .pβ‚βˆ˜universal = pullr left.pβ‚βˆ˜universal βˆ™ right.pβ‚βˆ˜universal
    pb .pβ‚‚βˆ˜universal = left.pβ‚‚βˆ˜universal
    pb .unique {p₁' = Pβ†’c} {Pβ†’d} {p = p} {lim'} q r =
      left.unique (right.unique (assoc _ _ _ βˆ™ q) s) r
      where
        s : bβ†’e ∘ aβ†’b ∘ lim' ≑ dβ†’e ∘ Pβ†’d
        s =
          bβ†’e ∘ aβ†’b ∘ lim'   β‰‘βŸ¨ pulll left.square βŸ©β‰‘
          (dβ†’e ∘ aβ†’d) ∘ lim' β‰‘βŸ¨ pullr r βŸ©β‰‘
          dβ†’e ∘ Pβ†’d          ∎

MonomorphismsπŸ”—

Being a monomorphism is a β€œlimit property”. Specifically, is a monomorphism iff. the square below is a pullback.

module _ {a b} {f : Hom a b} where
  is-monic→is-pullback : is-monic f → is-pullback id f id f
  is-monic→is-pullback mono .square = refl
  is-monicβ†’is-pullback mono .universal {p₁' = p₁'} p = p₁'
  is-monicβ†’is-pullback mono .pβ‚βˆ˜universal = idl _
  is-monicβ†’is-pullback mono .pβ‚‚βˆ˜universal {p = p} = idl _ βˆ™ mono _ _ p
  is-monicβ†’is-pullback mono .unique p q = introl refl βˆ™ p

  is-pullback→is-monic : is-pullback id f id f → is-monic f
  is-pullbackβ†’is-monic pb f g p = sym (pb .pβ‚βˆ˜universal {p = p}) βˆ™ pb .pβ‚‚βˆ˜universal

Pullbacks additionally preserve monomorphisms, as shown below:

is-monic→pullback-is-monic
  : βˆ€ {x y z} {f : Hom x z} {g : Hom y z} {p} {p1 : Hom p x} {p2 : Hom p y}
  β†’ is-monic f
  β†’ is-pullback p1 f p2 g
  β†’ is-monic p2
is-monic→pullback-is-monic {f = f} {g} {p1 = p1} {p2} mono pb h j p = eq
  where
    module pb = is-pullback pb
    q : f ∘ p1 ∘ h ≑ f ∘ p1 ∘ j
    q =
      f ∘ p1 ∘ h β‰‘βŸ¨ extendl pb.square βŸ©β‰‘
      g ∘ p2 ∘ h β‰‘βŸ¨ ap (g ∘_) p βŸ©β‰‘
      g ∘ p2 ∘ j β‰‘Λ˜βŸ¨ extendl pb.square βŸ©β‰‘Λ˜
      f ∘ p1 ∘ j ∎

    r : p1 ∘ h ≑ p1 ∘ j
    r = mono _ _ q

    eq : h ≑ j
    eq = pb.uniqueβ‚‚ {p = extendl pb.square} r p refl refl
rotate-pullback
  : βˆ€ {x y z} {f : Hom x z} {g : Hom y z} {p} {p1 : Hom p x} {p2 : Hom p y}
  β†’ is-pullback p1 f p2 g
  β†’ is-pullback p2 g p1 f
rotate-pullback pb .square = sym (pb .square)
rotate-pullback pb .universal p = pb .universal (sym p)
rotate-pullback pb .pβ‚βˆ˜universal = pb .pβ‚‚βˆ˜universal
rotate-pullback pb .pβ‚‚βˆ˜universal = pb .pβ‚βˆ˜universal
rotate-pullback pb .unique p q = pb .unique q p

is-pullback-iso
  : βˆ€ {p p' x y z} {f : Hom x z} {g : Hom y z} {p1 : Hom p x} {p2 : Hom p y}
  β†’ (i : p β‰… p')
  β†’ is-pullback p1 f p2 g
  β†’ is-pullback (p1 ∘ _β‰…_.from i) f (p2 ∘ _β‰…_.from i) g
is-pullback-iso {f = f} {g} {p1} {p2} i pb = pb' where
  module i = _β‰…_ i
  pb' : is-pullback _ _ _ _
  pb' .square = extendl (pb .square)
  pb' .universal p = i.to ∘ pb .universal p
  pb' .pβ‚βˆ˜universal = cancel-inner i.invr βˆ™ pb .pβ‚βˆ˜universal
  pb' .pβ‚‚βˆ˜universal = cancel-inner i.invr βˆ™ pb .pβ‚‚βˆ˜universal
  pb' .unique p q = invertibleβ†’monic (isoβ†’invertible (i Iso⁻¹)) _ _ $ sym $
    cancell i.invr βˆ™ sym (pb .unique (assoc _ _ _ βˆ™ p) (assoc _ _ _ βˆ™ q))

pullback-unique
  : βˆ€ {p p' x y z} {f : Hom x z} {g : Hom y z} {p1 : Hom p x} {p2 : Hom p y}
      {p1' : Hom p' x} {p2' : Hom p' y}
  β†’ is-pullback p1 f p2 g
  β†’ is-pullback p1' f p2' g
  β†’ p β‰… p'
pullback-unique {f = f} {g} {p1} {p2} {p1'} {p2'} pb pb'
  = make-iso pb→pb' pb'→pb il ir
  where
    pb→pb' = pb' .universal (pb .square)
    pb'β†’pb = pb .universal (pb' .square)
    il = uniqueβ‚‚ pb' {p = pb' .square}
      (pulll (pb' .pβ‚βˆ˜universal) βˆ™ pb .pβ‚βˆ˜universal)
      (pulll (pb' .pβ‚‚βˆ˜universal) βˆ™ pb .pβ‚‚βˆ˜universal)
      (idr _) (idr _)
    ir = uniqueβ‚‚ pb {p = pb .square}
      (pulll (pb .pβ‚βˆ˜universal) βˆ™ pb' .pβ‚βˆ˜universal)
      (pulll (pb .pβ‚‚βˆ˜universal) βˆ™ pb' .pβ‚‚βˆ˜universal)
      (idr _) (idr _)

Pullback-unique
  : βˆ€ {x y z} {f : Hom x z} {g : Hom y z}
  β†’ is-category C
  β†’ is-prop (Pullback f g)
Pullback-unique {x = X} {Y} {Z} {f} {g} c-cat x y = p where
  open Pullback
  module x = Pullback x
  module y = Pullback y
  apices = c-cat .to-path (pullback-unique (x .has-is-pb) (y .has-is-pb))

  abstract
    p1s : PathP (Ξ» i β†’ Hom (apices i) X) x.p₁ y.p₁
    p1s = Univalent.Hom-pathp-refll-iso c-cat (x.pβ‚βˆ˜universal)

    p2s : PathP (Ξ» i β†’ Hom (apices i) Y) x.pβ‚‚ y.pβ‚‚
    p2s = Univalent.Hom-pathp-refll-iso c-cat (x.pβ‚‚βˆ˜universal)

    lims
      : βˆ€ {P'} {p1' : Hom P' X} {p2' : Hom P' Y} (p : f ∘ p1' ≑ g ∘ p2')
      β†’ PathP (Ξ» i β†’ Hom P' (apices i)) (x.universal p) (y.universal p)
    lims p = Univalent.Hom-pathp-reflr-iso c-cat $
      y.unique (pulll y.pβ‚βˆ˜universal βˆ™ x.pβ‚βˆ˜universal)
              (pulll y.pβ‚‚βˆ˜universal βˆ™ x.pβ‚‚βˆ˜universal)

  p : x ≑ y
  p i .apex = apices i
  p i .p₁ = p1s i
  p i .pβ‚‚ = p2s i
  p i .has-is-pb .square =
    is-propβ†’pathp (Ξ» i β†’ Hom-set (apices i) Z (f ∘ p1s i) (g ∘ p2s i))
      x.square y.square i
  p i .has-is-pb .universal p = lims p i
  p i .has-is-pb .pβ‚βˆ˜universal {p = p} =
    is-propβ†’pathp (Ξ» i β†’ Hom-set _ X (p1s i ∘ lims p i) _)
      x.pβ‚βˆ˜universal y.pβ‚βˆ˜universal i
  p i .has-is-pb .pβ‚‚βˆ˜universal {p = p} =
    is-propβ†’pathp (Ξ» i β†’ Hom-set _ _ (p2s i ∘ lims p i) _)
      x.pβ‚‚βˆ˜universal y.pβ‚‚βˆ˜universal i
  p i .has-is-pb .unique {P' = P'} {p₁' = p₁'} {pβ‚‚' = pβ‚‚'} {p = p'} {lim' = lim'} =
    is-prop→pathp
      (Ξ» i   β†’ Ξ -is-hlevel {A = Hom P' (apices i)} 1
       Ξ» lim β†’ Ξ -is-hlevel {A = p1s i ∘ lim ≑ p₁'} 1
       Ξ» p   β†’ Ξ -is-hlevel {A = p2s i ∘ lim ≑ pβ‚‚'} 1
       Ξ» q   β†’ Hom-set P' (apices i) lim (lims p' i))
      (Ξ» lim β†’ x.unique {lim' = lim})
      (Ξ» lim β†’ y.unique {lim' = lim})
      i lim'

canonically-stable
  : βˆ€ {β„“'} (P : βˆ€ {a b} β†’ Hom a b β†’ Type β„“')
  β†’ is-category C
  β†’ (pb : βˆ€ {a b c} (f : Hom a c) (g : Hom b c) β†’ Pullback f g)
  β†’ ( βˆ€ {A B X} (f : Hom A B) (g : Hom X B)
    β†’ P f β†’ P (pb g f .Pullback.p₁) )
  β†’ is-pullback-stable P
canonically-stable P C-cat pbs stab f g Pf pb =
  transport (Ξ» i β†’ P (Pullback-unique C-cat (pbs g f) pb' i .Pullback.p₁))
    (stab f g Pf)
  where
    pb' : Pullback _ _
    pb' = record { has-is-pb = pb }