category_theory.limits.constructions.binary_products

source

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

category_theory.limits.is_limit (category_theory.limits.binary_fan.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₂ = {lift := λ (c : category_theory.limits.cone (category_theory.limits.pair X Y)), H₂.lift (category_theory.limits.pullback_cone.mk (c.π.app {as := category_theory.limits.walking_pair.left}) (c.π.app {as := category_theory.limits.walking_pair.right}) _), fac' := _, uniq' := _}

source

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

category_theory.limits.is_limit (category_theory.limits.pullback_cone.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), _⟩)

source

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

category_theory.limits.limit_cone F

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 := {lift := λ (c : category_theory.limits.cone F), category_theory.limits.pullback.lift (c.π.app {as := category_theory.limits.walking_pair.left}) (c.π.app {as := category_theory.limits.walking_pair.right}) _, fac' := _, uniq' := _}}

source

theorem has_binary_products_of_terminal_and_pullbacks (C : Type u) [category_theory.category C] [category_theory.limits.has_terminal C] [category_theory.limits.has_pullbacks C] :

category_theory.limits.has_binary_products C

Any category with pullbacks and terminal object has binary products.

source

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

X ⨯ Y ≅ category_theory.limits.pullback (category_theory.limits.terminal.from X) (category_theory.limits.terminal.from Y)

In a category with a terminal object and pullbacks, a product of objects X and Y is isomorphic to a pullback.

Equations

prod_iso_pullback C X Y = category_theory.limits.limit.iso_limit_cone (limit_cone_of_terminal_and_pullbacks (category_theory.limits.pair X Y))

source

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

category_theory.limits.is_colimit (category_theory.limits.binary_cofan.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₂ = {desc := λ (c : category_theory.limits.cocone (category_theory.limits.pair X Y)), H₂.desc (category_theory.limits.pushout_cocone.mk (c.ι.app {as := category_theory.limits.walking_pair.left}) (c.ι.app {as := category_theory.limits.walking_pair.right}) _), fac' := _, uniq' := _}

source

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

category_theory.limits.is_colimit (category_theory.limits.pushout_cocone.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), _⟩)

source

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

category_theory.limits.colimit_cocone F

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 := {desc := λ (c : category_theory.limits.cocone F), category_theory.limits.pushout.desc (c.ι.app {as := category_theory.limits.walking_pair.left}) (c.ι.app {as := category_theory.limits.walking_pair.right}) _, fac' := _, uniq' := _}}

source

theorem has_binary_coproducts_of_initial_and_pushouts (C : Type u) [category_theory.category C] [category_theory.limits.has_initial C] [category_theory.limits.has_pushouts C] :

category_theory.limits.has_binary_coproducts C

Any category with pushouts and initial object has binary coproducts.

source

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

X ⨿ Y ≅ category_theory.limits.pushout (category_theory.limits.initial.to X) (category_theory.limits.initial.to Y)

In a category with an initial object and pushouts, a coproduct of objects X and Y is isomorphic to a pushout.

Equations

coprod_iso_pushout C X Y = category_theory.limits.colimit.iso_colimit_cocone (colimit_cocone_of_initial_and_pushouts (category_theory.limits.pair X Y))

mathlib documentation

Constructing binary product from pullbacks and terminal object. #