open import Cat.Diagram.Pullback.Properties
open import Cat.Diagram.Pullback
open import Cat.Prelude

import Cat.Displayed.Instances.Subobjects as Subobjs
import Cat.Reasoning as Cat

module Cat.Diagram.Pullback.Along where

Pullbacks along an indeterminate morphism🔗

module _ {o ℓ} (C : Precategory o ℓ) where
  open Precategory C

This module defines the auxiliary notion of a map $p_{1} : P \to X$ being the pullback of a map $g : Y \to Z$ along a map $f : X \to Z,$ by summing over the possible maps $P \to Y$ 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 $g$ is the generic subobject $true : ⊤ \to Ω .$

  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

open is-pullback-along
open is-pullback
open Pullback

module _ {o ℓ} {C : Precategory o ℓ} where
  open Subobjs C
  open Cat C

  private
    unquoteDecl eqv = declare-record-iso eqv (quote is-pullback-along)
    variable
      U V W X Y Z : Ob
      f g h k m n l nm l₁ b₁ t₁ r₁ l₂ b₂ t₂ r₂ l₃ r₃ : Hom X Y
  abstract

Warning

Despite the name is-pullback-along, nothing about the definition guarantees that this type is a proposition after fixing the three maps $p_{1},$ $f$ and $g .$ However, we choose to name this auxiliary notion as though it were always a proposition, since it will most commonly be used when $g$ 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 $k$ is the pullback of $l$ along $n,$ and $h$ is the pullback of $k$ along $m,$ as in the diagram below, then $h$ is also the pullback of $l$ along $n \circ m .$

  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))))

Similarly, if some $l_{2}$ is the pullback of $r_{2}$ along some $t_{1},$ and $t_{1}$ is the roof of a pullback square $b_{1} \circ l_{1} = r_{1} \circ t_{1},$ then $r_{1} \circ r_{2}$ is the pullback of $l_{1} \circ l_{2}$ along $b_{1} .$ 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₂)

We also note that $f$ is the pullback of itself along $id .$

  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 $m : X ↪ Y$ is monic, then every $f : A \to X$ is the pullback of $m \circ f$ along $m .$

  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 $f$ pulls back to itself along $id .$ Moreover, the bottom square is also a pullback, as $m$ 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