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