Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Preserving binary products #

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

In particular, we show that ProdComparison G X Y is an isomorphism iff G preserves the product of X and Y.

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

Instances For

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

    Instances For

      If G preserves the product of (X,Y), then the product comparison map for G at (X,Y) is an isomorphism.

      Instances For

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

        Instances For

          If G preserves binary coproducts and C has them, then the binary cofan constructed of the mapped morphisms of the binary product cocone is a colimit.

          Instances For

            If G preserves the coproduct of (X,Y), then the coproduct comparison map for G at (X,Y) is an isomorphism.

            Instances For