Dependent products in categories

[finegeometer]

Hi,

I am unsure whether or not this pull request is a good idea. But since I only second-guessed myself after writing the code, it seems sensible to leave the choice up to you.

I provide two modules. The first defines the notion of "being a dependent product" in a category, by analogy to "being an exponential object". It then shows that when a morphism supports all dependent products, the base change functor has a right adjoint. The second module defines dependent products in a category of presheaves, thereby showing that PSh C is locally cartesian closed.

But I'm no longer sure this is worth adding to the 1Lab. My original motivation was to make it easy to state "this functor preserves dependent products", but I realized afterwards that we can simply say "preserves exponentials in slice categories", to the same effect. And while we certainly do want a proof that presheaves are locally cartesian closed, it may be better to just directly construct exponentials in slices of presheaves.

I'll leave it up to you. If you feel these definitions are worth adding, great! If they aren't, feel free to simply close this pull request.

[Lavenza]

Pull request preview

New pages

• Cat.Diagram.DependentProduct (+168, -0)
• Cat.Instances.Presheaf.DependentProducts (+166, -0)

[ncfavier]

I'm not opposed to this in principle, but I think the notions of exponentiable object and exponentiable morphism could be tied together a bit more neatly.

• https://1lab.dev/Cat.Diagram.Exponential.html#exponentiable-objects shows that if an object $B$ is exponentiable then the morphism $B \to 1$ is exponentiable (under some assumptions).
• https://1lab.dev/Cat.CartesianClosed.Locally.html shows that a morphism $f : A \to B$ is exponentiable if and only if it is exponentiable as an object of $\mathcal{C}/B$ (under some assumptions).

There should at least be links between these and the new page, which defines exponentiable morphisms.

It might be worth mentioning that these "dependent products" are also called distributivity pullbacks (a terrible name).

The computation in presheaves could be simplified by considering dependent products along $\alpha : F \Rightarrow 1$. The special case where $\alpha : F \Rightarrow G$ can be recovered by working in the slice over $G$, which is still a presheaf category.

Please avoid Title Case.