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.

source

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) :

category_theory.limits.fan f

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

category_theory.extend_fan c₁ c₂ = category_theory.limits.fan.mk c₂.X (λ (b : ulift (fin (n + 1))), b.cases_on (λ (i : fin (n + 1)), fin.cases c₂.fst (λ (i : fin n), c₂.snd ≫ c₁.π.app {down := i}) i))

source

@[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)

source

@[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

source

def category_theory.extend_fan_is_limit {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} (t₁ : category_theory.limits.is_limit c₁) (t₂ : category_theory.limits.is_limit c₂) :

category_theory.limits.is_limit (category_theory.extend_fan c₁ c₂)

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

Equations

category_theory.extend_fan_is_limit f t₁ t₂ = {lift := λ (s : category_theory.limits.cone (category_theory.discrete.functor f)), (category_theory.limits.binary_fan.is_limit.lift' t₂ (s.π.app {down := 0}) (t₁.lift {X := s.X, π := category_theory.discrete.nat_trans (λ (i : category_theory.discrete (ulift (fin n))), s.π.app {down := i.down.succ})})).val, fac' := _, uniq' := _}

source

theorem category_theory.has_finite_products_of_has_binary_and_terminal {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] [category_theory.limits.has_terminal C] :

category_theory.limits.has_finite_products C

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

source

def category_theory.preserves_fin_of_preserves_binary_and_terminal {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) F] [category_theory.limits.has_finite_products C] (n : ℕ) (f : ulift (fin n) → C) :

category_theory.limits.preserves_limit (category_theory.discrete.functor f) F

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

Equations

category_theory.preserves_fin_of_preserves_binary_and_terminal F (n + 1) = λ (f : ulift (fin (n + 1)) → C), category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.extend_fan_is_limit f (category_theory.limits.limit.is_limit (category_theory.discrete.functor (λ (i : ulift (fin n)), f {down := i.down.succ}))) (category_theory.limits.limit.is_limit (category_theory.limits.pair (f {down := 0}) (category_theory.limits.limit.cone (category_theory.discrete.functor (λ (i : ulift (fin n)), f {down := i.down.succ}))).X))) (⇑((category_theory.limits.is_limit_map_cone_fan_mk_equiv F (λ (j : ulift (fin (n + 1))), f j) (λ (b : ulift (fin (n + 1))), b.cases_on (λ (i : fin (n + 1)), fin.cases (category_theory.limits.binary_fan.fst (category_theory.limits.limit.cone (category_theory.limits.pair (f {down := 0}) (category_theory.limits.limit.cone (category_theory.discrete.functor (λ (i : ulift (fin n)), f {down := i.down.succ}))).X))) (λ (i : fin n), category_theory.limits.binary_fan.snd (category_theory.limits.limit.cone (category_theory.limits.pair (f {down := 0}) (category_theory.limits.limit.cone (category_theory.discrete.functor (λ (i : ulift (fin n)), f {down := i.down.succ}))).X)) ≫ (category_theory.limits.limit.cone (category_theory.discrete.functor (λ (i : ulift (fin n)), f {down := i.down.succ}))).π.app {down := i}) i))).symm) (let this : category_theory.limits.is_limit (category_theory.extend_fan (category_theory.limits.fan.mk (F.obj (∏ λ (i : ulift (fin n)), f {down := i.down.succ})) (λ (j : ulift (fin n)), F.map (category_theory.limits.pi.π (λ (i : ulift (fin n)), f {down := i.down.succ}) j))) (category_theory.limits.binary_fan.mk (F.map category_theory.limits.prod.fst) (F.map category_theory.limits.prod.snd))) := category_theory.extend_fan_is_limit (λ (i : ulift (fin (n + 1))), F.obj (f i)) (category_theory.limits.is_limit_of_has_product_of_preserves_limit F (λ (i : ulift (fin n)), f {down := i.down.succ})) (category_theory.limits.is_limit_of_has_binary_product_of_preserves_limit F (f {down := 0}) (∏ λ (i : ulift (fin n)), f {down := i.down.succ})) in this.of_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl (category_theory.extend_fan (category_theory.limits.fan.mk (F.obj (∏ λ (i : ulift (fin n)), f {down := i.down.succ})) (λ (j : ulift (fin n)), F.map (category_theory.limits.pi.π (λ (i : ulift (fin n)), f {down := i.down.succ}) j))) (category_theory.limits.binary_fan.mk (F.map category_theory.limits.prod.fst) (F.map category_theory.limits.prod.snd))).X) _)))
category_theory.preserves_fin_of_preserves_binary_and_terminal F 0 = λ (f : ulift (fin 0) → C), let _inst : category_theory.limits.preserves_limits_of_shape (category_theory.discrete (ulift (fin 0))) F := category_theory.limits.preserves_limits_of_shape_of_equiv (category_theory.discrete.equivalence (equiv.ulift.trans fin_zero_equiv').symm) F in category_theory.limits.preserves_limits_of_shape.preserves_limit

source

def category_theory.preserves_ulift_fin_of_preserves_binary_and_terminal {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) F] [category_theory.limits.has_finite_products C] (n : ℕ) :

category_theory.limits.preserves_limits_of_shape (category_theory.discrete (ulift (fin n))) F

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

Equations

category_theory.preserves_ulift_fin_of_preserves_binary_and_terminal F n = {preserves_limit := λ (K : category_theory.discrete (ulift (fin n)) ⥤ C), let this : category_theory.discrete.functor K.obj ≅ K := category_theory.discrete.nat_iso (λ (i : category_theory.discrete (category_theory.discrete (ulift (fin n)))), category_theory.iso.refl ((category_theory.discrete.functor K.obj).obj i)) in category_theory.limits.preserves_limit_of_iso_diagram F this}

source

def category_theory.preserves_finite_products_of_preserves_binary_and_terminal {C : Type u} [category_theory.category C] {D : Type u'} [category_theory.category D] (F : C ⥤ D) [category_theory.limits.preserves_limits_of_shape (category_theory.discrete category_theory.limits.walking_pair) F] [category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) F] [category_theory.limits.has_finite_products C] (J : Type v) [fintype J] :

category_theory.limits.preserves_limits_of_shape (category_theory.discrete J) F

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

Equations

category_theory.preserves_finite_products_of_preserves_binary_and_terminal F J = (fintype.equiv_fin J).rec_on_subsingleton (λ (e : J ≃ fin (fintype.card J)), category_theory.limits.preserves_limits_of_shape_of_equiv (category_theory.discrete.equivalence (e.trans equiv.ulift.symm)).symm F)