mathlib documentation

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} [category_theory.category C] {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.fan (λ (i : fin n), f i.succ)) (c₂ : category_theory.limits.binary_fan (f 0) 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} [category_theory.category C] {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.fan (λ (i : fin n), f i.succ)) (c₂ : category_theory.limits.binary_fan (f 0) c₁.X) (X : category_theory.discrete (fin (n + 1))) :
(category_theory.extend_fan c₁ 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} [category_theory.category C] {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.fan (λ (i : fin n), f i.succ)) (c₂ : category_theory.limits.binary_fan (f 0) c₁.X) :
(category_theory.extend_fan c₁ c₂).X = c₂.X

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

Equations

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
@[simp]
theorem category_theory.extend_cofan_X {C : Type u} [category_theory.category C] {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.cofan (λ (i : fin n), f i.succ)) (c₂ : category_theory.limits.binary_cofan (f 0) c₁.X) :
@[simp]
theorem category_theory.extend_cofan_ι_app {C : Type u} [category_theory.category C] {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.cofan (λ (i : fin n), f i.succ)) (c₂ : category_theory.limits.binary_cofan (f 0) c₁.X) (X : category_theory.discrete (fin (n + 1))) :
(category_theory.extend_cofan c₁ 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} [category_theory.category C] {n : } {f : fin (n + 1) → C} (c₁ : category_theory.limits.cofan (λ (i : fin n), f i.succ)) (c₂ : category_theory.limits.binary_cofan (f 0) 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

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

Equations

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