Documentation

Mathlib.CategoryTheory.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 piComparison G f is an isomorphism iff G preserves the limit of f.

The map of a fan is a limit iff the fan consisting of the mapped morphisms is a limit. This essentially lets us commute Fan.mk with Functor.mapCone.

Instances For

    The property of preserving products expressed in terms of fans.

    Instances For

      The property of reflecting products expressed in terms of fans.

      Instances For

        If G preserves products and C has them, then the fan constructed of the mapped projection of a product is a limit.

        Instances For

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

          Instances For

            The map of a cofan is a colimit iff the cofan consisting of the mapped morphisms is a colimit. This essentially lets us commute Cofan.mk with Functor.mapCocone.

            Instances For

              The property of preserving coproducts expressed in terms of cofans.

              Instances For

                The property of reflecting coproducts expressed in terms of cofans.

                Instances For

                  If G preserves coproducts and C has them, then the cofan constructed of the mapped inclusion of a coproduct is a colimit.

                  Instances For

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

                    Instances For