Forks and pullbacks

Stream: new members

[Coleton Kotch]

Given $f : X \rightarrow Z$ $g: Y \rightarrow Z$, and some $e : X \rightarrow Z$ which factors through $g$ as $e = g \circ p$, we have that any Fork (or equalizer cone) on $f$ and $e$, gives a pullback cone for $f$ and $g$ (and $p$ is a lift for the square). Conversely, given any pullback cone on $f$ and $g$ such that we have a lift, then we have a Fork.

In particular, given the case that $Y$ is a terminal object, then we have a bijection as any pullback cone will give a fork.

As far as I can tell, we do not have any form of this in the library. Implementing it and its dual should not be too much work, but better to ask first.

[Joël Riou]

I do not think we have anything like this in mathlib, though as independent lemmas/definitions I am not convinced that these would be very welcomed additions to mathlib, unless they are used in order to prove something more substantial.

[Coleton Kotch]

I was looking at using them to prove a that in a category with subobject classifiers, monomorphisms are all regular monomorphisms. Though this doesn’t require the dual notion and only needs the specific case where Y is terminal.