Constructing binary product from pullbacks and terminal object. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
The product is the pullback over the terminal objects. In particular, if a category has pullbacks and a terminal object, then it has binary products.
We also provide the dual.
If a span is the pullback span over the terminal object, then it is a binary product.
Equations
- is_binary_product_of_is_terminal_is_pullback F c hX f g hc = {lift := λ (s : category_theory.limits.cone F), hc.lift (category_theory.limits.pullback_cone.mk (s.π.app {as := category_theory.limits.walking_pair.left}) (s.π.app {as := category_theory.limits.walking_pair.right}) _), fac' := _, uniq' := _}
The pullback over the terminal object is the product
Equations
- is_product_of_is_terminal_is_pullback f g h k H₁ H₂ = is_binary_product_of_is_terminal_is_pullback (category_theory.limits.pair X Y) (category_theory.limits.binary_fan.mk h k) H₁ f g H₂
The product is the pullback over the terminal object.
Equations
- is_pullback_of_is_terminal_is_product f g h k H₁ H₂ = (category_theory.limits.pullback_cone.mk h k _).is_limit_aux' (λ (s : category_theory.limits.pullback_cone f g), ⟨H₂.lift (category_theory.limits.binary_fan.mk s.fst s.snd), _⟩)
Any category with pullbacks and a terminal object has a limit cone for each walking pair.
Equations
- limit_cone_of_terminal_and_pullbacks F = {cone := {X := category_theory.limits.pullback (category_theory.limits.terminal.from (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.terminal.from (F.obj {as := category_theory.limits.walking_pair.right})) _, π := category_theory.discrete.nat_trans (λ (x : category_theory.discrete category_theory.limits.walking_pair), x.cases_on (λ (x : category_theory.limits.walking_pair), x.cases_on category_theory.limits.pullback.fst category_theory.limits.pullback.snd))}, is_limit := is_binary_product_of_is_terminal_is_pullback F {X := category_theory.limits.pullback (category_theory.limits.terminal.from (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.terminal.from (F.obj {as := category_theory.limits.walking_pair.right})) _, π := category_theory.discrete.nat_trans (λ (x : category_theory.discrete category_theory.limits.walking_pair), x.cases_on (λ (x : category_theory.limits.walking_pair), x.cases_on category_theory.limits.pullback.fst category_theory.limits.pullback.snd))} category_theory.limits.terminal_is_terminal (category_theory.limits.terminal.from (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.terminal.from (F.obj {as := category_theory.limits.walking_pair.right})) (category_theory.limits.pullback_is_pullback (category_theory.limits.terminal.from (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.terminal.from (F.obj {as := category_theory.limits.walking_pair.right})))}
Any category with pullbacks and terminal object has binary products.
A functor that preserves terminal objects and pullbacks preserves binary products.
Equations
- preserves_binary_products_of_preserves_terminal_and_pullbacks F = {preserves_limit := λ (K : category_theory.discrete category_theory.limits.walking_pair ⥤ C), category_theory.limits.preserves_limit_of_preserves_limit_cone (limit_cone_of_terminal_and_pullbacks K).is_limit (is_binary_product_of_is_terminal_is_pullback (K ⋙ F) (F.map_cone (limit_cone_of_terminal_and_pullbacks K).cone) (category_theory.limits.is_limit_of_has_terminal_of_preserves_limit F) (F.map (category_theory.limits.terminal.from (K.obj {as := category_theory.limits.walking_pair.left}))) (F.map (category_theory.limits.terminal.from (K.obj {as := category_theory.limits.walking_pair.right}))) (category_theory.limits.is_limit_of_has_pullback_of_preserves_limit F (category_theory.limits.terminal.from (K.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.terminal.from (K.obj {as := category_theory.limits.walking_pair.right}))))}
In a category with a terminal object and pullbacks,
a product of objects X
and Y
is isomorphic to a pullback.
If a cospan is the pushout cospan under the initial object, then it is a binary coproduct.
Equations
- is_binary_coproduct_of_is_initial_is_pushout F c hX f g hc = {desc := λ (s : category_theory.limits.cocone F), hc.desc (category_theory.limits.pushout_cocone.mk (s.ι.app {as := category_theory.limits.walking_pair.left}) (s.ι.app {as := category_theory.limits.walking_pair.right}) _), fac' := _, uniq' := _}
The pushout under the initial object is the coproduct
Equations
- is_coproduct_of_is_initial_is_pushout f g h k H₁ H₂ = is_binary_coproduct_of_is_initial_is_pushout (category_theory.limits.pair X Y) (category_theory.limits.binary_cofan.mk f g) H₁ h k H₂
The coproduct is the pushout under the initial object.
Equations
- is_pushout_of_is_initial_is_coproduct f g h k H₁ H₂ = (category_theory.limits.pushout_cocone.mk f g _).is_colimit_aux' (λ (s : category_theory.limits.pushout_cocone h k), ⟨H₂.desc (category_theory.limits.binary_cofan.mk s.inl s.inr), _⟩)
Any category with pushouts and an initial object has a colimit cocone for each walking pair.
Equations
- colimit_cocone_of_initial_and_pushouts F = {cocone := {X := category_theory.limits.pushout (category_theory.limits.initial.to (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.initial.to (F.obj {as := category_theory.limits.walking_pair.right})) _, ι := category_theory.discrete.nat_trans (λ (x : category_theory.discrete category_theory.limits.walking_pair), x.cases_on (λ (x : category_theory.limits.walking_pair), x.cases_on category_theory.limits.pushout.inl category_theory.limits.pushout.inr))}, is_colimit := is_binary_coproduct_of_is_initial_is_pushout F {X := category_theory.limits.pushout (category_theory.limits.initial.to (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.initial.to (F.obj {as := category_theory.limits.walking_pair.right})) _, ι := category_theory.discrete.nat_trans (λ (x : category_theory.discrete category_theory.limits.walking_pair), x.cases_on (λ (x : category_theory.limits.walking_pair), x.cases_on category_theory.limits.pushout.inl category_theory.limits.pushout.inr))} category_theory.limits.initial_is_initial (category_theory.limits.initial.to (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.initial.to (F.obj {as := category_theory.limits.walking_pair.right})) (category_theory.limits.pushout_is_pushout (category_theory.limits.initial.to (F.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.initial.to (F.obj {as := category_theory.limits.walking_pair.right})))}
Any category with pushouts and initial object has binary coproducts.
A functor that preserves initial objects and pushouts preserves binary coproducts.
Equations
- preserves_binary_coproducts_of_preserves_initial_and_pushouts F = {preserves_colimit := λ (K : category_theory.discrete category_theory.limits.walking_pair ⥤ C), category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (colimit_cocone_of_initial_and_pushouts K).is_colimit (is_binary_coproduct_of_is_initial_is_pushout (K ⋙ F) (F.map_cocone (colimit_cocone_of_initial_and_pushouts K).cocone) (category_theory.limits.is_colimit_of_has_initial_of_preserves_colimit F) (F.map (category_theory.limits.initial.to (K.obj {as := category_theory.limits.walking_pair.left}))) (F.map (category_theory.limits.initial.to (K.obj {as := category_theory.limits.walking_pair.right}))) (category_theory.limits.is_colimit_of_has_pushout_of_preserves_colimit F (category_theory.limits.initial.to (K.obj {as := category_theory.limits.walking_pair.left})) (category_theory.limits.initial.to (K.obj {as := category_theory.limits.walking_pair.right}))))}
In a category with an initial object and pushouts,
a coproduct of objects X
and Y
is isomorphic to a pushout.