open import Cat.Prelude

import Cat.Diagram.Pullback
import Cat.Reasoning

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 xx, 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 bβ†’e←db \to e \ot d to one over cβ†’f←ec \to f \ot e. Can we do this? Yes! By assumption, the square on the right commutes, which lets us apply commutativity of the red diagram (the assumption pp 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 x→ax \to a, which, since aa is a pullback, makes everything in sight commute, and does so uniquely.

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

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

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

    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 cβ†’f←dc \to f \ot d. By the universal property of the right pullback, we can find a map xβ†’bx \to b forming the left leg of a cone over bβ†’e←db \to e \ot d; By the universal property of the left square, we then have a map xβ†’ax \to a, 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 .limiting {p₁' = Pβ†’c} {pβ‚‚' = Pβ†’d} x =
      left.limiting {p₁' = right.limiting (x βˆ™ sym (assoc _ _ _))} {pβ‚‚' = Pβ†’d}
        right.pβ‚‚βˆ˜limiting
    pb .pβ‚βˆ˜limiting = pullr left.pβ‚βˆ˜limiting βˆ™ right.pβ‚βˆ˜limiting
    pb .pβ‚‚βˆ˜limiting = left.pβ‚‚βˆ˜limiting
    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, f:Aβ†’Bf : A \to B 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 .limiting {p₁' = p₁'} p = p₁'
  is-monicβ†’is-pullback mono .pβ‚βˆ˜limiting = idl _
  is-monicβ†’is-pullback mono .pβ‚‚βˆ˜limiting {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β‚βˆ˜limiting {p = p}) βˆ™ pb .pβ‚‚βˆ˜limiting

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