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 : Fin n) => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) :
(CategoryTheory.extendFan c₁ c₂).pt = c₂.pt
@[simp]
theorem CategoryTheory.extendFan_π_app {C : Type u} [CategoryTheory.Category.{v, u} C] {n : } {f : Fin (n + 1)C} (c₁ : CategoryTheory.Limits.Fan fun (i : Fin n) => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) :
def CategoryTheory.extendFan {C : Type u} [CategoryTheory.Category.{v, u} C] {n : } {f : Fin (n + 1)C} (c₁ : CategoryTheory.Limits.Fan fun (i : Fin n) => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt) :

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.

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

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

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

      If F preserves the terminal object and binary products, then it preserves products indexed by Fin n for any n.

      Equations
      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 : Fin n) => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) :
        (CategoryTheory.extendCofan c₁ c₂).pt = c₂.pt
        @[simp]
        theorem CategoryTheory.extendCofan_ι_app {C : Type u} [CategoryTheory.Category.{v, u} C] {n : } {f : Fin (n + 1)C} (c₁ : CategoryTheory.Limits.Cofan fun (i : Fin n) => f (Fin.succ i)) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) :

        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.

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

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

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

            If F preserves the initial object and binary coproducts, then it preserves products indexed by Fin n for any n.

            Equations
            Instances For