mathlib documentation

category_theory.limits.preserves.shapes.products

Preserving products

Constructions to relate the notions of preserving products and reflecting products to concrete fans.

In particular, we show that pi_comparison G f is an isomorphism iff G preserves the limit of f.

The property of reflecting products expressed in terms of fans.

Equations

If G preserves limits, we have an isomorphism from the image of a product to the product of the images.

Equations