module Cat.Diagram.Pullback.Along where

Pullbacks along an indeterminate morphism🔗

This module defines the auxiliary notion of a map being the pullback of a map along a map by summing over the possible maps fitting in the diagram below.

While this is a rather artificial notion, it comes up a lot in the context of elementary topos theory, especially in the case where is the generic subobject

  record is-pullback-along {P X Y Z} (p₁ : Hom P X) (f : Hom X Z) (g : Hom Y Z) : Type (o  ) where
    no-eta-equality
    field
      top       : Hom P Y
      has-is-pb : is-pullback C p₁ f top g
    open is-pullback has-is-pb public
\ Warning

Despite the name is-pullback-along, nothing about the definition guarantees that this type is a proposition after fixing the three maps and However, we choose to name this auxiliary notion as though it were always a proposition, since it will most commonly be used when is a monomorphism, and, under this assumption, it is propositional:

    is-monic→is-pullback-along-is-prop
      :  {P X Y Z} {f : Hom P X} {g : Hom X Z} {h : Hom Y Z}
       is-monic h
       is-prop (is-pullback-along C f g h)
    is-monic→is-pullback-along-is-prop h-monic = Iso→is-hlevel 1 eqv λ (_ , x) (_ , y) 
      Σ-prop-path! (h-monic _ _ (sym (x .square)  y .square))

Of course, the notion of being a pullback along a map is closed under composition: if is the pullback of along and is the pullback of along as in the diagram below, then is also the pullback of along

  paste-is-pullback-along
    : is-pullback-along C k n l  is-pullback-along C h m k
     n  m  nm  is-pullback-along C h nm l
  paste-is-pullback-along p q r .top = p .top  q .top
  paste-is-pullback-along p q r .has-is-pb =
    subst-is-pullback refl r refl refl (rotate-pullback (pasting-left→outer-is-pullback
      (rotate-pullback (p .has-is-pb))
      (rotate-pullback (q .has-is-pb))
      ( extendl (sym (p .is-pullback-along.square))
       pushr (sym (q .is-pullback-along.square)))))

Similarly, if some is the pullback of along some and is the roof of a pullback square then is the pullback of along This is best understood diagramatically:

  extend-is-pullback-along
    : is-pullback C l₁ b₁ t₁ r₁
     is-pullback-along C l₂ t₁ r₂
     l₁  l₂  l₃
     r₁  r₂  r₃
     is-pullback-along C l₃ b₁ r₃
This follows immediately from the pasting lemma for pullbacks, so we will skip over the details.
  extend-is-pullback-along pb₁ pb₂ l-comm r-comm .top = pb₂ .top
  extend-is-pullback-along pb₁ pb₂ l-comm r-comm .has-is-pb =
    subst-is-pullback l-comm refl refl r-comm $
    pasting-left→outer-is-pullback pb₁ (has-is-pb pb₂) $
    pulll (pb₁ .square)  extendr (pb₂ .is-pullback-along.square)

We also note that is the pullback of itself along

  is-pullback-along-id : is-pullback-along C f id f
  is-pullback-along-id .top = id
  is-pullback-along-id .has-is-pb = rotate-pullback id-is-pullback

If some is monic, then every is the pullback of along

  is-pullback-along-monic : is-monic m  is-pullback-along C f m (m  f)

This is yet another instance of a pullback pasting. We can arrange our morphisms into the following set of squares:

The upper square is always a pullback square, as pulls back to itself along Moreover, the bottom square is also a pullback, as is monic. This means that the outer square is itself a pullback, which completes the proof.

  is-pullback-along-monic m-monic =
    extend-is-pullback-along
      (is-monic→is-pullback m-monic)
      is-pullback-along-id
      (idl _) refl