Documentation

Mathlib.CategoryTheory.Limits.Constructions.FiniteProductsOfBinaryProducts

Constructing finite products from binary products and terminal. #

If a category has binary products and a terminal object then it has finite products. If a functor preserves binary products and the terminal object then it preserves finite products.

TODO #

Provide the dual results. Show the analogous results for functors which reflect or create (co)limits.

@[simp]
theorem CategoryTheory.extendFan_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {n : } {f : Fin (n + 1)C} (c₁ : CategoryTheory.Limits.Fan fun i => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) :
(CategoryTheory.extendFan c₁ c₂).pt = c₂.pt
@[simp]

Given n+1 objects of C, a fan for the last n with point c₁.pt and a binary fan on c₁.pt and f 0, we can build a fan for all n+1.

In extendFanIsLimit we show that if the two given fans are limits, then this fan is also a limit.

Instances For

    Show that if the two given fans in extendFan are limits, then the constructed fan is also a limit.

    Instances For
      @[simp]
      theorem CategoryTheory.extendCofan_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {n : } {f : Fin (n + 1)C} (c₁ : CategoryTheory.Limits.Cofan fun i => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) :
      (CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt

      Given n+1 objects of C, a cofan for the last n with point c₁.pt and a binary cofan on c₁.X and f 0, we can build a cofan for all n+1.

      In extendCofanIsColimit we show that if the two given cofans are colimits, then this cofan is also a colimit.

      Instances For

        Show that if the two given cofans in extendCofan are colimits, then the constructed cofan is also a colimit.

        Instances For