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 : ulift (fin (n + 1)) → C} (c₁ : category_theory.limits.fan (λ (i : ulift (fin n)), f {down := i.down.succ})) (c₂ : category_theory.limits.binary_fan (f {down := 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 : ulift (fin (n + 1)) → C} (c₁ : category_theory.limits.fan (λ (i : ulift (fin n)), f {down := i.down.succ})) (c₂ : category_theory.limits.binary_fan (f {down := 0}) c₁.X) (b : ulift (fin (n + 1))) :
(category_theory.extend_fan c₁ c₂).π.app b = b.cases_on (λ (i : fin (n + 1)), fin.cases c₂.fst (λ (i : fin n), c₂.snd c₁.π.app {down := i}) i)
@[simp]
theorem category_theory.extend_fan_X {C : Type u} [category_theory.category C] {n : } {f : ulift (fin (n + 1)) → C} (c₁ : category_theory.limits.fan (λ (i : ulift (fin n)), f {down := i.down.succ})) (c₂ : category_theory.limits.binary_fan (f {down := 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 ulift (fin n) for any n.

Equations
@[simp]
theorem category_theory.extend_cofan_X {C : Type u} [category_theory.category C] {n : } {f : ulift (fin (n + 1)) → C} (c₁ : category_theory.limits.cofan (λ (i : ulift (fin n)), f {down := i.down.succ})) (c₂ : category_theory.limits.binary_cofan (f {down := 0}) c₁.X) :
@[simp]
theorem category_theory.extend_cofan_ι_app {C : Type u} [category_theory.category C] {n : } {f : ulift (fin (n + 1)) → C} (c₁ : category_theory.limits.cofan (λ (i : ulift (fin n)), f {down := i.down.succ})) (c₂ : category_theory.limits.binary_cofan (f {down := 0}) c₁.X) (b : ulift (fin (n + 1))) :
(category_theory.extend_cofan c₁ c₂).ι.app b = b.cases_on (λ (i : fin (n + 1)), fin.cases c₂.inl (λ (i : fin n), c₁.ι.app {down := i} c₂.inr) i)
def category_theory.extend_cofan {C : Type u} [category_theory.category C] {n : } {f : ulift (fin (n + 1)) → C} (c₁ : category_theory.limits.cofan (λ (i : ulift (fin n)), f {down := i.down.succ})) (c₂ : category_theory.limits.binary_cofan (f {down := 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 ulift (fin n) for any n.

Equations