Leibniz contructions PR

Stream: Infinity-Cosmos

[Jack McKoen]

I've just drafted #33974 for the 'pushout-product' and 'pullback-power' constructions, see https://ncatlab.org/nlab/show/pushout-product, https://ncatlab.org/nlab/show/pullback-power. These are also called Leibniz constructions, though I'm not sure what naming scheme to commit to for mathlib (please advise). Using Joël's PushoutObjObj and PullbackObjObj API, I've defined these constructions in what I think is a suitable generality, culminating in the associated bifunctors on the arrow categories.

In another WIP PR #33935, I'm using these to define a monoidal structure on the arrow category of a cartesian closed category.

[Emily Riehl]

While the historical motivation for the term "Leibniz" is a bit of a stretch, it is nice to have an adjective that can modify any functor of two variables. For me the name "pushout product" suggests that this is the product bifunctor.

[Emily Riehl]

From context (variance of the functor, whether it is a left adjoint or a right adjoint), you can typically tell whether this Leibniz thing should involve a pushout in the target category (for left adjoints, with everything covariant) or a pullback (for right adjoints, with the first argument contravariant). So I don't say "Leibniz pushout tensor" for the Leibniz construction using a pushout associated to the functor "tensor"; I just say "Leibniz tensor". Similarly "Leibniz hom", "Leibniz weighted limit" both of which, as right adjointy things, use pullbacks.

[Emily Riehl]

But this is all on paper. Maybe in mathlib we need something more like "LeibnizPushout F" (for the bifunctor associated to F using a pushout) or "LeibnizPullback F" (for the bifunctor associated to F using a pullback)?

This sort of thing has bothered me in other settings too. For F : C => Type, I'd like Elements F to be the category that projects to C, while for F : C^op => Type, I'd like Elements F to be the category that also projects to C (a different construction than in the first case).

[Jack McKoen]

I think LeibnizPushout F and LeibnizPullback G are good choices, I'll go with them!

[Jack McKoen]

#33974 is merged, next is #33935

[Jack McKoen]

I opened a small PR for the Leibniz adjunction (#34887), and once #33935 is merged I'll try to formalize the rest of Prop. C.2.9 in Elements. I formalized some of this prop specifically for SSet in my thesis, so I don't think it will be too bad.