mathlib3 documentation

category_theory.limits.preserves.shapes.products

Preserving products #

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

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.