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.
def
is_binary_product_of_is_terminal_is_pullback
{C : Type u}
[category_theory.category C]
(F : category_theory.discrete category_theory.limits.walking_pair ⥤ C)
(c : category_theory.limits.cone F)
{X : C}
(hX : category_theory.limits.is_terminal X)
(f : F.obj {as := category_theory.limits.walking_pair.left} ⟶ X)
(g : F.obj {as := category_theory.limits.walking_pair.right} ⟶ X)
(hc : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk (c.π.app {as := category_theory.limits.walking_pair.left}) (c.π.app {as := category_theory.limits.walking_pair.right}) _)) :
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' := _}
def
is_product_of_is_terminal_is_pullback
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(h : W ⟶ X)
(k : W ⟶ Y)
(H₁ : category_theory.limits.is_terminal Z)
(H₂ : category_theory.limits.is_limit (category_theory.limits.pullback_cone.mk h k _)) :
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₂
def
is_pullback_of_is_terminal_is_product
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(h : W ⟶ X)
(k : W ⟶ Y)
(H₁ : category_theory.limits.is_terminal Z)
(H₂ : category_theory.limits.is_limit (category_theory.limits.binary_fan.mk h k)) :
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), _⟩)
noncomputable
def
limit_cone_of_terminal_and_pullbacks
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_pullbacks C]
(F : category_theory.discrete category_theory.limits.walking_pair ⥤ C) :
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})))}
theorem
has_binary_products_of_has_terminal_and_pullbacks
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_pullbacks C] :
Any category with pullbacks and terminal object has binary products.
noncomputable
def
preserves_binary_products_of_preserves_terminal_and_pullbacks
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.has_terminal C]
[category_theory.limits.has_pullbacks C]
[category_theory.limits.preserves_limits_of_shape (category_theory.discrete pempty) F]
[category_theory.limits.preserves_limits_of_shape category_theory.limits.walking_cospan F] :
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}))))}
noncomputable
def
prod_iso_pullback
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_terminal C]
[category_theory.limits.has_pullbacks C]
(X Y : C)
[category_theory.limits.has_binary_product X Y] :
In a category with a terminal object and pullbacks,
a product of objects X and Y is isomorphic to a pullback.
def
is_binary_coproduct_of_is_initial_is_pushout
{C : Type u}
[category_theory.category C]
(F : category_theory.discrete category_theory.limits.walking_pair ⥤ C)
(c : category_theory.limits.cocone F)
{X : C}
(hX : category_theory.limits.is_initial X)
(f : X ⟶ F.obj {as := category_theory.limits.walking_pair.left})
(g : X ⟶ F.obj {as := category_theory.limits.walking_pair.right})
(hc : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk (c.ι.app {as := category_theory.limits.walking_pair.left}) (c.ι.app {as := category_theory.limits.walking_pair.right}) _)) :
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' := _}
def
is_coproduct_of_is_initial_is_pushout
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(h : W ⟶ X)
(k : W ⟶ Y)
(H₁ : category_theory.limits.is_initial W)
(H₂ : category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.mk f g _)) :
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₂
def
is_pushout_of_is_initial_is_coproduct
{C : Type u}
[category_theory.category C]
{W X Y Z : C}
(f : X ⟶ Z)
(g : Y ⟶ Z)
(h : W ⟶ X)
(k : W ⟶ Y)
(H₁ : category_theory.limits.is_initial W)
(H₂ : category_theory.limits.is_colimit (category_theory.limits.binary_cofan.mk f g)) :
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), _⟩)
noncomputable
def
colimit_cocone_of_initial_and_pushouts
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_pushouts C]
(F : category_theory.discrete category_theory.limits.walking_pair ⥤ C) :
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})))}
theorem
has_binary_coproducts_of_has_initial_and_pushouts
(C : Type u)
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_pushouts C] :
Any category with pushouts and initial object has binary coproducts.
noncomputable
def
preserves_binary_coproducts_of_preserves_initial_and_pushouts
{C : Type u}
[category_theory.category C]
{D : Type u'}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.limits.has_initial C]
[category_theory.limits.has_pushouts C]
[category_theory.limits.preserves_colimits_of_shape (category_theory.discrete pempty) F]
[category_theory.limits.preserves_colimits_of_shape category_theory.limits.walking_span F] :
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}))))}
noncomputable
def
coprod_iso_pushout
{C : Type u}
[category_theory.category C]
[category_theory.limits.has_initial C]
[category_theory.limits.has_pushouts C]
(X Y : C)
[category_theory.limits.has_binary_coproduct X Y] :
In a category with an initial object and pushouts,
a coproduct of objects X and Y is isomorphic to a pushout.