Documentation

Mathlib.CategoryTheory.Limits.Constructions.ZeroObjects

Limits involving zero objects #

Binary products and coproducts with a zero object always exist, and pullbacks/pushouts over a zero object are products/coproducts.

A zero object is a right unit for categorical product.

Equations
  • One or more equations did not get rendered due to their size.
Instances For

    A zero object is a left unit for categorical coproduct.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      A zero object is a right unit for categorical coproduct.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        The pullback over the zero object is the product.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          The pushout over the zero object is the coproduct.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For