# mathlibdocumentation

category_theory.limits.constructions.finite_products_of_binary_products

# 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.

def category_theory.extend_fan {C : Type u} {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.fan (λ (i : fin n), f i.succ)) (c₂ : c₁.X) :

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

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

Equations
@[simp]
theorem category_theory.extend_fan_π_app {C : Type u} {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.fan (λ (i : fin n), f i.succ)) (c₂ : c₁.X) (X : category_theory.discrete (fin (n + 1))) :
c₂).π.app X = fin.cases c₂.fst (λ (i : fin n), c₂.snd c₁.π.app {as := i}) X.as
@[simp]
theorem category_theory.extend_fan_X {C : Type u} {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.fan (λ (i : fin n), f i.succ)) (c₂ : c₁.X) :
c₂).X = c₂.X
def category_theory.extend_fan_is_limit {C : Type u} {n : } (f : fin (n + 1) → C) {c₁ : category_theory.limits.fan (λ (i : fin n), f i.succ)} {c₂ : c₁.X} (t₁ : category_theory.limits.is_limit c₁) (t₂ : category_theory.limits.is_limit c₂) :

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

Equations

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

noncomputable def category_theory.preserves_fin_of_preserves_binary_and_terminal {C : Type u} {D : Type u'} (F : C D) (n : ) (f : fin n → C) :

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

Equations

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

Equations

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

Equations
@[simp]
theorem category_theory.extend_cofan_X {C : Type u} {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.cofan (λ (i : fin n), f i.succ)) (c₂ : c₁.X) :
c₂).X = c₂.X
@[simp]
theorem category_theory.extend_cofan_ι_app {C : Type u} {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.cofan (λ (i : fin n), f i.succ)) (c₂ : c₁.X) (X : category_theory.discrete (fin (n + 1))) :
c₂).ι.app X = fin.cases c₂.inl (λ (i : fin n), c₁.ι.app {as := i} c₂.inr) X.as
def category_theory.extend_cofan {C : Type u} {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.cofan (λ (i : fin n), f i.succ)) (c₂ : c₁.X) :

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

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

Equations
def category_theory.extend_cofan_is_colimit {C : Type u} {n : } (f : fin (n + 1) → C) {c₁ : category_theory.limits.cofan (λ (i : fin n), f i.succ)} {c₂ : c₁.X}  :

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

Equations

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

noncomputable def category_theory.preserves_fin_of_preserves_binary_and_initial {C : Type u} {D : Type u'} (F : C D) (n : ) (f : fin n → C) :

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

Equations

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

Equations

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

Equations