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

Instances For
def CategoryTheory.extendFanIsLimit {C : Type u} {n : } (f : Fin (n + 1)C) {c₁ : CategoryTheory.Limits.Fan fun i => f ()} {c₂ : CategoryTheory.Limits.BinaryFan (f 0) c₁.pt} (t₁ : ) (t₂ : ) :

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

Instances For

If C has a terminal object and binary products, then it has finite products.

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

Equations
• One or more equations did not get rendered due to their size.
• = fun f => inferInstance
Instances For

If F preserves the terminal object and binary products, then it preserves limits of shape Discrete (Fin n).

Instances For

If F preserves the terminal object and binary products then it preserves finite products.

Instances For
@[simp]
theorem CategoryTheory.extendCofan_pt {C : Type u} {n : } {f : Fin (n + 1)C} (c₁ : CategoryTheory.Limits.Cofan fun i => f ()) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) :
().pt = c₂.pt
@[simp]
theorem CategoryTheory.extendCofan_ι_app {C : Type u} {n : } {f : Fin (n + 1)C} (c₁ : CategoryTheory.Limits.Cofan fun i => f ()) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt) (X : CategoryTheory.Discrete (Fin (n + 1))) :
().ι.app X = Fin.cases () (fun i => CategoryTheory.CategoryStruct.comp (c₁.app { as := i }) ()) X.as
def CategoryTheory.extendCofan {C : Type u} {n : } {f : Fin (n + 1)C} (c₁ : CategoryTheory.Limits.Cofan fun i => f ()) (c₂ : CategoryTheory.Limits.BinaryCofan (f 0) 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
def CategoryTheory.extendCofanIsColimit {C : Type u} {n : } (f : Fin (n + 1)C) {c₁ : CategoryTheory.Limits.Cofan fun i => f ()} {c₂ : CategoryTheory.Limits.BinaryCofan (f 0) c₁.pt} (t₁ : ) (t₂ : ) :

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

Instances For

If C has an initial object and binary coproducts, then it has finite coproducts.

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

Equations
• One or more equations did not get rendered due to their size.
• = fun f => inferInstance
Instances For

If F preserves the initial object and binary coproducts, then it preserves colimits of shape Discrete (Fin n).

Instances For

If F preserves the initial object and binary coproducts then it preserves finite products.

Instances For