combining pullbacks

Stream: maths

[Edward van de Meent]

tldr; I'd like some help finding the right statement/proof for showing that you can combine pullback squares in a certain way.

i'm considering doing some small topos theory lemmas (eventually) about Lawvere-Tierney topologies. on the way to defining those, i came across the following lemma:

Given two pullback squares where the top morphisms are $f : A_1 \rightarrow Z$ and $g : B_1 \rightarrow Z$ respectively, there is a (specific) square which is a pullback square, where the top morphism is the diagonal of the pullback square of $f$ and $g$. (i.e. this diagram).

I've proven this in lean, but the proof is very verbal (read: lots of unfolding definitions, proving certain squares commute) in a way i wasn't used from the CategoryTheory part of the library.

I suspect that this is because this is not the right (generality) lemma or not the right proof, but it might also be because i might have overlooked some clearer proof...

Does anyone have suggestions for simplifying this statement/proof? (i'm also not convinced that my naming sense here is correct at all)

[Joël Riou]

If the category has binary products, then the pullback square of your lemma can be obtained as a vertical composition of two pullback squares:
diagram.png

[Joël Riou]

The bottom square is obtained as a binary product of two pullback squares, and the top square relates the fiber product and the binary product via the diagonal of Z.

[Edward van de Meent]

i don't think we have the binary product of pullback squares in mathlib, right?

[Joël Riou]

No, but at least, this splits the lemma into two general more basic tasks.

[Edward van de Meent]

it's indeed an improvement in argument, i was just checking to prevent duplicate work

[Edward van de Meent]

but this argument does need all corner pairs to have products, rather than just the bottom two.

[Joël Riou]

This is the reason why I added "If the category has binary products", which should not be an issue for a topos!

[Joël Riou]

Otherwise, I do not see how your proof could be improved significantly!

[Edward van de Meent]

do you think that mathlib would accept the form where you just assume HasBinaryProducts C+HasPullback (or even HasFiniteLimits C)? Or would it be rejected for being not as general as possible?

[Joël Riou]

If I am the one reviewing it, it would be fine :-) Nevertheless, I think it is important to allow arbitrary limit binary fans/pullback cones. For example, for binary products of pullback squares, we probably want a general version, and two corollaries phrased in terms of the binary product from the limits API and the chosen binary product (assuming CartesianMonoidalCategory).