Constructing finite products from binary products and terminal. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.
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.
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 {as := 0}) (t₁.lift {X := s.X, π := category_theory.discrete.nat_trans (λ (_x : category_theory.discrete (fin n)), category_theory.extend_fan_is_limit._match_1 f s _x)})).val, fac' := _, uniq' := _}
- category_theory.extend_fan_is_limit._match_1 f s {as := i} = s.π.app {as := i.succ}
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
- category_theory.preserves_fin_of_preserves_binary_and_terminal F (n + 1) = λ (f : 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 : fin n), f i.succ))) (category_theory.limits.limit.is_limit (category_theory.limits.pair (f 0) (category_theory.limits.limit.cone (category_theory.discrete.functor (λ (i : fin n), f i.succ))).X))) (⇑((category_theory.limits.is_limit_map_cone_fan_mk_equiv F (λ (j : fin (n + 1)), f j) (fin.cases (category_theory.limits.binary_fan.fst (category_theory.limits.limit.cone (category_theory.limits.pair (f 0) (category_theory.limits.limit.cone (category_theory.discrete.functor (λ (i : fin n), f i.succ))).X))) (λ (i : fin n), category_theory.limits.binary_fan.snd (category_theory.limits.limit.cone (category_theory.limits.pair (f 0) (category_theory.limits.limit.cone (category_theory.discrete.functor (λ (i : fin n), f i.succ))).X)) ≫ (category_theory.limits.limit.cone (category_theory.discrete.functor (λ (i : fin n), f i.succ))).π.app {as := i}))).symm) (let this : category_theory.limits.is_limit (category_theory.extend_fan (category_theory.limits.fan.mk (F.obj (∏ λ (i : fin n), f i.succ)) (λ (j : fin n), F.map (category_theory.limits.pi.π (λ (i : fin n), f i.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 : fin (n + 1)), F.obj (f i)) (category_theory.limits.is_limit_of_has_product_of_preserves_limit F (λ (i : fin n), f i.succ)) (category_theory.limits.is_limit_of_has_binary_product_of_preserves_limit F (f 0) (∏ λ (i : fin n), f i.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 : fin n), f i.succ)) (λ (j : fin n), F.map (category_theory.limits.pi.π (λ (i : fin n), f i.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 : fin 0 → C), let _inst : category_theory.limits.preserves_limits_of_shape (category_theory.discrete (fin 0)) F := category_theory.limits.preserves_limits_of_shape_of_equiv (category_theory.discrete.equivalence fin_zero_equiv'.symm) F in category_theory.limits.preserves_limits_of_shape.preserves_limit
If F
preserves the terminal object and binary products, then it preserves limits of shape
discrete (fin n)
.
Equations
- category_theory.preserves_shape_fin_of_preserves_binary_and_terminal F n = {preserves_limit := λ (K : category_theory.discrete (fin n) ⥤ C), let this : category_theory.discrete.functor (λ (n_1 : fin n), K.obj {as := n_1}) ≅ K := category_theory.discrete.nat_iso (λ (_x : category_theory.discrete (fin n)), category_theory.preserves_shape_fin_of_preserves_binary_and_terminal._match_1 n K _x) in category_theory.limits.preserves_limit_of_iso_diagram F this}
- category_theory.preserves_shape_fin_of_preserves_binary_and_terminal._match_1 n K {as := i} = category_theory.iso.refl ((category_theory.discrete.functor (λ (n_1 : fin n), K.obj {as := n_1})).obj {as := i})
If F
preserves the terminal object and binary products then it preserves finite products.
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.
Show that if the two given cofans in extend_cofan
are colimits,
then the constructed cofan is also a colimit.
Equations
- category_theory.extend_cofan_is_colimit f t₁ t₂ = {desc := λ (s : category_theory.limits.cocone (category_theory.discrete.functor f)), (category_theory.limits.binary_cofan.is_colimit.desc' t₂ (s.ι.app {as := 0}) (t₁.desc {X := s.X, ι := category_theory.discrete.nat_trans (λ (i : category_theory.discrete (fin n)), s.ι.app {as := i.as.succ})})).val, fac' := _, uniq' := _}
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
- category_theory.preserves_fin_of_preserves_binary_and_initial F (n + 1) = λ (f : fin (n + 1) → C), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.extend_cofan_is_colimit f (category_theory.limits.colimit.is_colimit (category_theory.discrete.functor (λ (i : fin n), f i.succ))) (category_theory.limits.colimit.is_colimit (category_theory.limits.pair (f 0) (category_theory.limits.colimit.cocone (category_theory.discrete.functor (λ (i : fin n), f i.succ))).X))) (⇑((category_theory.limits.is_colimit_map_cocone_cofan_mk_equiv F (λ (j : fin (n + 1)), f j) (fin.cases (category_theory.limits.binary_cofan.inl (category_theory.limits.colimit.cocone (category_theory.limits.pair (f 0) (category_theory.limits.colimit.cocone (category_theory.discrete.functor (λ (i : fin n), f i.succ))).X))) (λ (i : fin n), (category_theory.limits.colimit.cocone (category_theory.discrete.functor (λ (i : fin n), f i.succ))).ι.app {as := i} ≫ category_theory.limits.binary_cofan.inr (category_theory.limits.colimit.cocone (category_theory.limits.pair (f 0) (category_theory.limits.colimit.cocone (category_theory.discrete.functor (λ (i : fin n), f i.succ))).X))))).symm) (let this : category_theory.limits.is_colimit (category_theory.extend_cofan (category_theory.limits.cofan.mk (F.obj (∐ λ (i : fin n), f i.succ)) (λ (j : fin n), F.map (category_theory.limits.sigma.ι (λ (i : fin n), f i.succ) j))) (category_theory.limits.binary_cofan.mk (F.map category_theory.limits.coprod.inl) (F.map category_theory.limits.coprod.inr))) := category_theory.extend_cofan_is_colimit (λ (i : fin (n + 1)), F.obj (f i)) (category_theory.limits.is_colimit_of_has_coproduct_of_preserves_colimit F (λ (i : fin n), f i.succ)) (category_theory.limits.is_colimit_of_has_binary_coproduct_of_preserves_colimit F (f 0) (∐ λ (i : fin n), f i.succ)) in this.of_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl (category_theory.extend_cofan (category_theory.limits.cofan.mk (F.obj (∐ λ (i : fin n), f i.succ)) (λ (j : fin n), F.map (category_theory.limits.sigma.ι (λ (i : fin n), f i.succ) j))) (category_theory.limits.binary_cofan.mk (F.map category_theory.limits.coprod.inl) (F.map category_theory.limits.coprod.inr))).X) _)))
- category_theory.preserves_fin_of_preserves_binary_and_initial F 0 = λ (f : fin 0 → C), let _inst : category_theory.limits.preserves_colimits_of_shape (category_theory.discrete (fin 0)) F := category_theory.limits.preserves_colimits_of_shape_of_equiv (category_theory.discrete.equivalence fin_zero_equiv'.symm) F in category_theory.limits.preserves_colimits_of_shape.preserves_colimit
If F
preserves the initial object and binary coproducts, then it preserves colimits of shape
discrete (fin n)
.
Equations
- category_theory.preserves_shape_fin_of_preserves_binary_and_initial F n = {preserves_colimit := λ (K : category_theory.discrete (fin n) ⥤ C), let this : category_theory.discrete.functor (λ (n_1 : fin n), K.obj {as := n_1}) ≅ K := category_theory.discrete.nat_iso (λ (_x : category_theory.discrete (fin n)), category_theory.preserves_shape_fin_of_preserves_binary_and_initial._match_1 n K _x) in category_theory.limits.preserves_colimit_of_iso_diagram F this}
- category_theory.preserves_shape_fin_of_preserves_binary_and_initial._match_1 n K {as := i} = category_theory.iso.refl ((category_theory.discrete.functor (λ (n_1 : fin n), K.obj {as := n_1})).obj {as := i})
If F
preserves the initial object and binary coproducts then it preserves finite products.