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)

  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.

    : 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 \leftarrow d to one over cβ†’f←ec \to f \leftarrow 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:

      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 .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 cβ†’f←dc \to f \leftarrow 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 \leftarrow d; By the universal property of the left square, we then have a map xβ†’ax \to a, as we wanted.

    : 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}
    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
        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          ∎


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 .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:

  : βˆ€ {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
    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
  : βˆ€ {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

  : βˆ€ {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 = ∘ 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))

  : βˆ€ {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
    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 _)

  : βˆ€ {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))

    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)

      : βˆ€ {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β€²} =
      (Ξ» 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β€²

  : βˆ€ {β„“β€²} (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)
    pbβ€² : Pullback _ _
    pbβ€² = record { has-is-pb = pb }