mathlib3 documentation

category_theory.limits.constructions.over.products

Products in the over category #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Shows that products in the over category can be derived from wide pullbacks in the base category. The main result is over_product_of_wide_pullback, which says that if C has J-indexed wide pullbacks, then over B has J-indexed products.

@[reducible]

(Implementation) Given a product diagram in C/B, construct the corresponding wide pullback diagram in C.

Equations

Construct terminal object in the over category. This isn't an instance as it's not typically the way we want to define terminal objects. (For instance, this gives a terminal object which is different from the generic one given by over_product_of_wide_pullback above.)