# mathlib3documentation

category_theory.limits.shapes.binary_products

# Binary (co)products #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We define a category `walking_pair`, which is the index category for a binary (co)product diagram. A convenience method `pair X Y` constructs the functor from the walking pair, hitting the given objects.

We define `prod X Y` and `coprod X Y` as limits and colimits of such functors.

Typeclasses `has_binary_products` and `has_binary_coproducts` assert the existence of (co)limits shaped as walking pairs.

We include lemmas for simplifying equations involving projections and coprojections, and define braiding and associating isomorphisms, and the product comparison morphism.

## References #

@[protected, instance]

The type of objects for the diagram indexing a binary (co)product.

Instances for `category_theory.limits.walking_pair`
@[protected, instance]

The equivalence swapping left and right.

Equations

An equivalence from `walking_pair` to `bool`, sometimes useful when reindexing limits.

Equations
def category_theory.limits.pair_function {C : Type u} (X Y : C) :

The function on the walking pair, sending the two points to `X` and `Y`.

Equations
@[simp]
theorem category_theory.limits.pair_function_left {C : Type u} (X Y : C) :
@[simp]
theorem category_theory.limits.pair_function_right {C : Type u} (X Y : C) :
def category_theory.limits.pair {C : Type u} (X Y : C) :

The diagram on the walking pair, sending the two points to `X` and `Y`.

Equations
Instances for `category_theory.limits.pair`
@[simp]
theorem category_theory.limits.pair_obj_left {C : Type u} (X Y : C) :
@[simp]
theorem category_theory.limits.pair_obj_right {C : Type u} (X Y : C) :

The natural transformation between two functors out of the walking pair, specified by its components.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.limits.map_pair_iso_hom_app {C : Type u}  :
= (category_theory.discrete.rec (category_theory.limits.walking_pair.rec f g) X).hom

The natural isomorphism between two functors out of the walking pair, specified by its components.

Equations
@[simp]
theorem category_theory.limits.map_pair_iso_inv_app {C : Type u}  :
= (category_theory.discrete.rec (category_theory.limits.walking_pair.rec f g) X).inv

Every functor out of the walking pair is naturally isomorphic (actually, equal) to a `pair`

Equations
@[simp]
theorem category_theory.limits.diagram_iso_pair_hom_app {C : Type u}  :
= (category_theory.discrete.rec (category_theory.limits.walking_pair.rec X).hom
@[simp]
theorem category_theory.limits.diagram_iso_pair_inv_app {C : Type u}  :
= (category_theory.discrete.rec (category_theory.limits.walking_pair.rec X).inv
def category_theory.limits.pair_comp {C : Type u} {D : Type u} (X Y : C) (F : C D) :
(F.obj Y)

The natural isomorphism between `pair X Y ⋙ F` and `pair (F.obj X) (F.obj Y)`.

Equations
@[reducible]
def category_theory.limits.binary_fan {C : Type u} (X Y : C) :
Type (max u v)

A binary fan is just a cone on a diagram indexing a product.

@[reducible]

The first projection of a binary fan.

@[reducible]

The second projection of a binary fan.

@[simp]
theorem category_theory.limits.binary_fan.π_app_left {C : Type u} {X Y : C}  :
@[simp]
def category_theory.limits.binary_fan.is_limit.mk {C : Type u} {X Y : C} (lift : Π {T : C}, (T X) (T Y) (T s.X)) (hl₁ : {T : C} (f : T X) (g : T Y), lift f g s.fst = f) (hl₂ : {T : C} (f : T X) (g : T Y), lift f g s.snd = g) (uniq : {T : C} (f : T X) (g : T Y) (m : T s.X), m s.fst = f m s.snd = g m = lift f g) :

A convenient way to show that a binary fan is a limit.

Equations
theorem category_theory.limits.binary_fan.is_limit.hom_ext {C : Type u} {W X Y : C} {f g : W s.X} (h₁ : f s.fst = g s.fst) (h₂ : f s.snd = g s.snd) :
f = g
@[reducible]
def category_theory.limits.binary_cofan {C : Type u} (X Y : C) :
Type (max u v)

A binary cofan is just a cocone on a diagram indexing a coproduct.

@[reducible]

The first inclusion of a binary cofan.

@[reducible]

The second inclusion of a binary cofan.

@[simp]
@[simp]
def category_theory.limits.binary_cofan.is_colimit.mk {C : Type u} {X Y : C} (desc : Π {T : C}, (X T) (Y T) (s.X T)) (hd₁ : {T : C} (f : X T) (g : Y T), s.inl desc f g = f) (hd₂ : {T : C} (f : X T) (g : Y T), s.inr desc f g = g) (uniq : {T : C} (f : X T) (g : Y T) (m : s.X T), s.inl m = f s.inr m = g m = desc f g) :

A convenient way to show that a binary cofan is a colimit.

Equations
theorem category_theory.limits.binary_cofan.is_colimit.hom_ext {C : Type u} {W X Y : C} {f g : s.X W} (h₁ : s.inl f = s.inl g) (h₂ : s.inr f = s.inr g) :
f = g
@[simp]
theorem category_theory.limits.binary_fan.mk_X {C : Type u} {X Y P : C} (π₁ : P X) (π₂ : P Y) :
= P
def category_theory.limits.binary_fan.mk {C : Type u} {X Y P : C} (π₁ : P X) (π₂ : P Y) :

A binary fan with vertex `P` consists of the two projections `π₁ : P ⟶ X` and `π₂ : P ⟶ Y`.

Equations
@[simp]
theorem category_theory.limits.binary_cofan.mk_X {C : Type u} {X Y P : C} (ι₁ : X P) (ι₂ : Y P) :
= P
def category_theory.limits.binary_cofan.mk {C : Type u} {X Y P : C} (ι₁ : X P) (ι₂ : Y P) :

A binary cofan with vertex `P` consists of the two inclusions `ι₁ : X ⟶ P` and `ι₂ : Y ⟶ P`.

Equations
@[simp]
theorem category_theory.limits.binary_fan.mk_fst {C : Type u} {X Y P : C} (π₁ : P X) (π₂ : P Y) :
= π₁
@[simp]
theorem category_theory.limits.binary_fan.mk_snd {C : Type u} {X Y P : C} (π₁ : P X) (π₂ : P Y) :
= π₂
@[simp]
theorem category_theory.limits.binary_cofan.mk_inl {C : Type u} {X Y P : C} (ι₁ : X P) (ι₂ : Y P) :
= ι₁
@[simp]
theorem category_theory.limits.binary_cofan.mk_inr {C : Type u} {X Y P : C} (ι₁ : X P) (ι₂ : Y P) :
= ι₂

Every `binary_fan` is isomorphic to an application of `binary_fan.mk`.

Equations

Every `binary_fan` is isomorphic to an application of `binary_fan.mk`.

Equations
def category_theory.limits.binary_fan.is_limit_mk {C : Type u} {X Y W : C} {fst : W X} {snd : W Y} (lift : Π (s : , s.X W) (fac_left : (s : , lift s fst = s.fst) (fac_right : (s : , lift s snd = s.snd) (uniq : (s : (m : s.X W), m fst = s.fst m snd = s.snd m = lift s) :

This is a more convenient formulation to show that a `binary_fan` constructed using `binary_fan.mk` is a limit cone.

Equations
def category_theory.limits.binary_cofan.is_colimit_mk {C : Type u} {X Y W : C} {inl : X W} {inr : Y W} (desc : Π (s : , W s.X) (fac_left : (s : , inl desc s = s.inl) (fac_right : (s : , inr desc s = s.inr) (uniq : (s : (m : W s.X), inl m = s.inl inr m = s.inr m = desc s) :

This is a more convenient formulation to show that a `binary_cofan` constructed using `binary_cofan.mk` is a colimit cocone.

Equations
def category_theory.limits.binary_fan.is_limit.lift' {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
{l // l s.fst = f l s.snd = g}

If `s` is a limit binary fan over `X` and `Y`, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y` induces a morphism `l : W ⟶ s.X` satisfying `l ≫ s.fst = f` and `l ≫ s.snd = g`.

Equations
@[simp]
theorem category_theory.limits.binary_fan.is_limit.lift'_coe {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
def category_theory.limits.binary_cofan.is_colimit.desc' {C : Type u} {W X Y : C} (f : X W) (g : Y W) :
{l // s.inl l = f s.inr l = g}

If `s` is a colimit binary cofan over `X` and `Y`,, then every pair of morphisms `f : X ⟶ W` and `g : Y ⟶ W` induces a morphism `l : s.X ⟶ W` satisfying `s.inl ≫ l = f` and `s.inr ≫ l = g`.

Equations
@[simp]
theorem category_theory.limits.binary_cofan.is_colimit.desc'_coe {C : Type u} {W X Y : C} (f : X W) (g : Y W) :

Binary products are symmetric.

Equations
noncomputable def category_theory.limits.binary_fan.is_limit_comp_left_iso {C : Type u} {X Y X' : C} (f : X X')  :

If `X' ≅ X`, then `X × Y` also is the product of `X'` and `Y`.

Equations
noncomputable def category_theory.limits.binary_fan.is_limit_comp_right_iso {C : Type u} {X Y Y' : C} (f : Y Y')  :

If `Y' ≅ Y`, then `X x Y` also is the product of `X` and `Y'`.

Equations

Binary coproducts are symmetric.

Equations
noncomputable def category_theory.limits.binary_cofan.is_colimit_comp_left_iso {C : Type u} {X Y X' : C} (f : X' X)  :

If `X' ≅ X`, then `X ⨿ Y` also is the coproduct of `X'` and `Y`.

Equations
noncomputable def category_theory.limits.binary_cofan.is_colimit_comp_right_iso {C : Type u} {X Y Y' : C} (f : Y' Y)  :

If `Y' ≅ Y`, then `X ⨿ Y` also is the coproduct of `X` and `Y'`.

Equations
@[reducible]
def category_theory.limits.has_binary_product {C : Type u} (X Y : C) :
Prop

An abbreviation for `has_limit (pair X Y)`.

@[reducible]
def category_theory.limits.has_binary_coproduct {C : Type u} (X Y : C) :
Prop

An abbreviation for `has_colimit (pair X Y)`.

@[reducible]
noncomputable def category_theory.limits.prod {C : Type u} (X Y : C)  :
C

If we have a product of `X` and `Y`, we can access it using `prod X Y` or `X ⨯ Y`.

@[reducible]
noncomputable def category_theory.limits.coprod {C : Type u} (X Y : C)  :
C

If we have a coproduct of `X` and `Y`, we can access it using `coprod X Y` or `X ⨿ Y`.

@[reducible]
noncomputable def category_theory.limits.prod.fst {C : Type u} {X Y : C}  :
X Y X

The projection map to the first component of the product.

@[reducible]
noncomputable def category_theory.limits.prod.snd {C : Type u} {X Y : C}  :
X Y Y

The projecton map to the second component of the product.

@[reducible]
noncomputable def category_theory.limits.coprod.inl {C : Type u} {X Y : C}  :
X X ⨿ Y

The inclusion map from the first component of the coproduct.

@[reducible]
noncomputable def category_theory.limits.coprod.inr {C : Type u} {X Y : C}  :
Y X ⨿ Y

The inclusion map from the second component of the coproduct.

The binary fan constructed from the projection maps is a limit.

Equations

The binary cofan constructed from the coprojection maps is a colimit.

Equations
@[ext]
theorem category_theory.limits.prod.hom_ext {C : Type u} {W X Y : C} {f g : W X Y}  :
f = g
@[ext]
theorem category_theory.limits.coprod.hom_ext {C : Type u} {W X Y : C} {f g : X ⨿ Y W}  :
f = g
@[reducible]
noncomputable def category_theory.limits.prod.lift {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
W X Y

If the product of `X` and `Y` exists, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y` induces a morphism `prod.lift f g : W ⟶ X ⨯ Y`.

@[reducible]
noncomputable def category_theory.limits.diag {C : Type u} (X : C)  :
X X X

diagonal arrow of the binary product in the category `fam I`

@[reducible]
noncomputable def category_theory.limits.coprod.desc {C : Type u} {W X Y : C} (f : X W) (g : Y W) :
X ⨿ Y W

If the coproduct of `X` and `Y` exists, then every pair of morphisms `f : X ⟶ W` and `g : Y ⟶ W` induces a morphism `coprod.desc f g : X ⨿ Y ⟶ W`.

@[reducible]
noncomputable def category_theory.limits.codiag {C : Type u} (X : C)  :
X ⨿ X X

codiagonal arrow of the binary coproduct

@[simp]
theorem category_theory.limits.prod.lift_fst_assoc {C : Type u} {W X Y : C} (f : W X) (g : W Y) {X' : C} (f' : X X') :
@[simp]
theorem category_theory.limits.prod.lift_fst {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
@[simp]
theorem category_theory.limits.prod.lift_snd {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
@[simp]
theorem category_theory.limits.prod.lift_snd_assoc {C : Type u} {W X Y : C} (f : W X) (g : W Y) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.coprod.inl_desc {C : Type u} {W X Y : C} (f : X W) (g : Y W) :
theorem category_theory.limits.coprod.inl_desc_assoc {C : Type u} {W X Y : C} (f : X W) (g : Y W) {X' : C} (f' : W X') :
theorem category_theory.limits.coprod.inr_desc_assoc {C : Type u} {W X Y : C} (f : X W) (g : Y W) {X' : C} (f' : W X') :
@[simp]
theorem category_theory.limits.coprod.inr_desc {C : Type u} {W X Y : C} (f : X W) (g : Y W) :
@[protected, instance]
def category_theory.limits.prod.mono_lift_of_mono_left {C : Type u} {W X Y : C} (f : W X) (g : W Y)  :
@[protected, instance]
def category_theory.limits.prod.mono_lift_of_mono_right {C : Type u} {W X Y : C} (f : W X) (g : W Y)  :
@[protected, instance]
def category_theory.limits.coprod.epi_desc_of_epi_left {C : Type u} {W X Y : C} (f : X W) (g : Y W)  :
@[protected, instance]
def category_theory.limits.coprod.epi_desc_of_epi_right {C : Type u} {W X Y : C} (f : X W) (g : Y W)  :
noncomputable def category_theory.limits.prod.lift' {C : Type u} {W X Y : C} (f : W X) (g : W Y) :
{l //

If the product of `X` and `Y` exists, then every pair of morphisms `f : W ⟶ X` and `g : W ⟶ Y` induces a morphism `l : W ⟶ X ⨯ Y` satisfying `l ≫ prod.fst = f` and `l ≫ prod.snd = g`.

Equations
noncomputable def category_theory.limits.coprod.desc' {C : Type u} {W X Y : C} (f : X W) (g : Y W) :
{l //

If the coproduct of `X` and `Y` exists, then every pair of morphisms `f : X ⟶ W` and `g : Y ⟶ W` induces a morphism `l : X ⨿ Y ⟶ W` satisfying `coprod.inl ≫ l = f` and `coprod.inr ≫ l = g`.

Equations
noncomputable def category_theory.limits.prod.map {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
W X Y Z

If the products `W ⨯ X` and `Y ⨯ Z` exist, then every pair of morphisms `f : W ⟶ Y` and `g : X ⟶ Z` induces a morphism `prod.map f g : W ⨯ X ⟶ Y ⨯ Z`.

Equations
Instances for `category_theory.limits.prod.map`
noncomputable def category_theory.limits.coprod.map {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
W ⨿ X Y ⨿ Z

If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of morphisms `f : W ⟶ Y` and `g : W ⟶ Z` induces a morphism `coprod.map f g : W ⨿ X ⟶ Y ⨿ Z`.

Equations
Instances for `category_theory.limits.coprod.map`
theorem category_theory.limits.prod.comp_lift_assoc {C : Type u} {V W X Y : C} (f : V W) (g : W X) (h : W Y) {X' : C} (f' : X Y X') :
f = (f h) f'
@[simp]
theorem category_theory.limits.prod.comp_lift {C : Type u} {V W X Y : C} (f : V W) (g : W X) (h : W Y) :
= (f h)
theorem category_theory.limits.prod.comp_diag {C : Type u} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.limits.prod.map_fst {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.prod.map_fst_assoc {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.prod.map_snd_assoc {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) {X' : C} (f' : Z X') :
@[simp]
theorem category_theory.limits.prod.map_snd {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.prod.map_id_id {C : Type u} {X Y : C}  :
(𝟙 Y) = 𝟙 (X Y)
@[simp]
@[simp]
theorem category_theory.limits.prod.lift_map_assoc {C : Type u} {V W X Y Z : C} (f : V W) (g : V X) (h : W Y) (k : X Z) {X' : C} (f' : Y Z X') :
= (g k) f'
@[simp]
theorem category_theory.limits.prod.lift_map {C : Type u} {V W X Y Z : C} (f : V W) (g : V X) (h : W Y) (k : X Z) :
@[simp]
theorem category_theory.limits.prod.lift_fst_comp_snd_comp {C : Type u} {W X Y Z : C} (g : W X) (g' : Y Z) :
@[simp]
theorem category_theory.limits.prod.map_map_assoc {C : Type u} {A₁ A₂ A₃ B₁ B₂ B₃ : C} (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) {X' : C} (f' : A₃ B₃ X') :
= (g k) f'
@[simp]
theorem category_theory.limits.prod.map_map {C : Type u} {A₁ A₂ A₃ B₁ B₂ B₃ : C} (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) :
theorem category_theory.limits.prod.map_swap {C : Type u} {A B X Y : C} (f : A B) (g : X Y)  :
theorem category_theory.limits.prod.map_swap_assoc {C : Type u} {A B X Y : C} (f : A B) (g : X Y) {X' : C} (f' : Y B X') :
f' = f'
theorem category_theory.limits.prod.map_comp_id_assoc {C : Type u} {X Y Z W : C} (f : X Y) (g : Y Z) {X' : C} (f' : Z W X') :
(𝟙 W) f' = f'
theorem category_theory.limits.prod.map_comp_id {C : Type u} {X Y Z W : C} (f : X Y) (g : Y Z)  :
(𝟙 W) =
theorem category_theory.limits.prod.map_id_comp {C : Type u} {X Y Z W : C} (f : X Y) (g : Y Z)  :
(f g) =
theorem category_theory.limits.prod.map_id_comp_assoc {C : Type u} {X Y Z W : C} (f : X Y) (g : Y Z) {X' : C} (f' : W Z X') :
(f g) f' = f'
@[simp]
theorem category_theory.limits.prod.map_iso_hom {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.prod.map_iso_inv {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
noncomputable def category_theory.limits.prod.map_iso {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
W X Y Z

If the products `W ⨯ X` and `Y ⨯ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and `g : X ≅ Z` induces an isomorphism `prod.map_iso f g : W ⨯ X ≅ Y ⨯ Z`.

Equations
@[protected, instance]
def category_theory.limits.is_iso_prod {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z)  :
@[protected, instance]
def category_theory.limits.prod.map_mono {C : Type u_1} {W X Y Z : C} (f : W Y) (g : X Z)  :
@[simp]
theorem category_theory.limits.prod.diag_map {C : Type u} {X Y : C} (f : X Y)  :
@[simp]
theorem category_theory.limits.prod.diag_map_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y Y X') :
@[simp]
theorem category_theory.limits.prod.diag_map_fst_snd_assoc {C : Type u} {X Y : C} [ (X Y)] {X' : C} (f' : X Y X') :
@[simp]
theorem category_theory.limits.prod.diag_map_fst_snd {C : Type u} {X Y : C} [ (X Y)] :
@[simp]
theorem category_theory.limits.prod.diag_map_fst_snd_comp {C : Type u} {X X' Y Y' : C} (g : X Y) (g' : X' Y') :
@[simp]
theorem category_theory.limits.prod.diag_map_fst_snd_comp_assoc {C : Type u} {X X' Y Y' : C} (g : X Y) (g' : X' Y') {X'_1 : C} (f' : Y Y' X'_1) :
@[protected, instance]
@[simp]
theorem category_theory.limits.coprod.desc_comp {C : Type u} {V W X Y : C} (f : V W) (g : X V) (h : Y V) :
= (h f)
@[simp]
theorem category_theory.limits.coprod.desc_comp_assoc {C : Type u} {V W X Y : C} (f : V W) (g : X V) (h : Y V) {X' : C} (f' : W X') :
f f' = (h f) f'
theorem category_theory.limits.coprod.diag_comp {C : Type u} {X Y : C} (f : X Y) :
@[simp]
theorem category_theory.limits.coprod.inl_map {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.coprod.inl_map_assoc {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) {X' : C} (f' : Y ⨿ Z X') :
@[simp]
theorem category_theory.limits.coprod.inr_map_assoc {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) {X' : C} (f' : Y ⨿ Z X') :
@[simp]
theorem category_theory.limits.coprod.inr_map {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.coprod.map_id_id {C : Type u} {X Y : C}  :
(𝟙 Y) = 𝟙 (X ⨿ Y)
@[simp]
@[simp]
theorem category_theory.limits.coprod.map_desc {C : Type u} {S T U V W : C} (f : U S) (g : W S) (h : T U) (k : V W) :
theorem category_theory.limits.coprod.map_desc_assoc {C : Type u} {S T U V W : C} (f : U S) (g : W S) (h : T U) (k : V W) {X' : C} (f' : S X') :
= (k g) f'
@[simp]
theorem category_theory.limits.coprod.desc_comp_inl_comp_inr {C : Type u} {W X Y Z : C} (g : W X) (g' : Y Z) :
@[simp]
theorem category_theory.limits.coprod.map_map_assoc {C : Type u} {A₁ A₂ A₃ B₁ B₂ B₃ : C} (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) {X' : C} (f' : A₃ ⨿ B₃ X') :
= (g k) f'
@[simp]
theorem category_theory.limits.coprod.map_map {C : Type u} {A₁ A₂ A₃ B₁ B₂ B₃ : C} (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) :
theorem category_theory.limits.coprod.map_swap {C : Type u} {A B X Y : C} (f : A B) (g : X Y)  :
theorem category_theory.limits.coprod.map_swap_assoc {C : Type u} {A B X Y : C} (f : A B) (g : X Y) {X' : C} (f' : Y ⨿ B X') :
f' = f'
theorem category_theory.limits.coprod.map_comp_id {C : Type u} {X Y Z W : C} (f : X Y) (g : Y Z)  :
(𝟙 W) =
theorem category_theory.limits.coprod.map_comp_id_assoc {C : Type u} {X Y Z W : C} (f : X Y) (g : Y Z) {X' : C} (f' : Z ⨿ W X') :
(𝟙 W) f' = f'
theorem category_theory.limits.coprod.map_id_comp_assoc {C : Type u} {X Y Z W : C} (f : X Y) (g : Y Z) {X' : C} (f' : W ⨿ Z X') :
(f g) f' = f'
theorem category_theory.limits.coprod.map_id_comp {C : Type u} {X Y Z W : C} (f : X Y) (g : Y Z)  :
(f g) =
@[simp]
theorem category_theory.limits.coprod.map_iso_hom {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
@[simp]
theorem category_theory.limits.coprod.map_iso_inv {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
noncomputable def category_theory.limits.coprod.map_iso {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z) :
W ⨿ X Y ⨿ Z

If the coproducts `W ⨿ X` and `Y ⨿ Z` exist, then every pair of isomorphisms `f : W ≅ Y` and `g : W ≅ Z` induces a isomorphism `coprod.map_iso f g : W ⨿ X ≅ Y ⨿ Z`.

Equations
@[protected, instance]
def category_theory.limits.is_iso_coprod {C : Type u} {W X Y Z : C} (f : W Y) (g : X Z)  :
@[protected, instance]
def category_theory.limits.coprod.map_epi {C : Type u_1} {W X Y Z : C} (f : W Y) (g : X Z)  :
@[simp]
theorem category_theory.limits.coprod.map_codiag {C : Type u} {X Y : C} (f : X Y)  :
theorem category_theory.limits.coprod.map_codiag_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
@[simp]
theorem category_theory.limits.coprod.map_inl_inr_codiag_assoc {C : Type u} {X Y : C} [ (X ⨿ Y)] {X' : C} (f' : X ⨿ Y X') :
@[simp]
theorem category_theory.limits.coprod.map_comp_inl_inr_codiag {C : Type u} {X X' Y Y' : C} (g : X Y) (g' : X' Y') :
theorem category_theory.limits.coprod.map_comp_inl_inr_codiag_assoc {C : Type u} {X X' Y Y' : C} (g : X Y) (g' : X' Y') {X'_1 : C} (f' : Y ⨿ Y' X'_1) :
@[reducible]

`has_binary_products` represents a choice of product for every pair of objects.

@[reducible]

`has_binary_coproducts` represents a choice of coproduct for every pair of objects.

If `C` has all limits of diagrams `pair X Y`, then it has all binary products

If `C` has all colimits of diagrams `pair X Y`, then it has all binary coproducts

noncomputable def category_theory.limits.prod.braiding {C : Type u} (P Q : C)  :
P Q Q P

The braiding isomorphism which swaps a binary product.

Equations
@[simp]
@[simp]
theorem category_theory.limits.braid_natural_assoc {C : Type u} {W X Y Z : C} (f : X Y) (g : Z W) {X' : C} (f' : W Y X') :
theorem category_theory.limits.braid_natural {C : Type u} {W X Y Z : C} (f : X Y) (g : Z W) :

The braiding isomorphism can be passed through a map by swapping the order.

theorem category_theory.limits.prod.symmetry_assoc {C : Type u} (P Q : C) {X' : C} (f' : P Q X') :
= f'
theorem category_theory.limits.prod.symmetry {C : Type u} (P Q : C)  :
= 𝟙 (P Q)

The braiding isomorphism is symmetric.

noncomputable def category_theory.limits.prod.associator {C : Type u} (P Q R : C) :
P Q R P (Q R)

The associator isomorphism for binary products.

Equations
theorem category_theory.limits.prod.pentagon {C : Type u} (W X Y Z : C) :
= Z).hom (Y Z)).hom
theorem category_theory.limits.prod.pentagon_assoc {C : Type u} (W X Y Z : C) {X' : C} (f' : W (X (Y Z)) X') :
Z).hom = Z).hom (Y Z)).hom f'
theorem category_theory.limits.prod.associator_naturality_assoc {C : Type u} {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) {X' : C} (f' : Y₁ (Y₂ Y₃) X') :
Y₃).hom f' = X₃).hom
theorem category_theory.limits.prod.associator_naturality {C : Type u} {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :
noncomputable def category_theory.limits.prod.left_unitor {C : Type u} (P : C)  :
⊤_ C P P

The left unitor isomorphism for binary products with the terminal object.

Equations
@[simp]
@[simp]
@[simp]
noncomputable def category_theory.limits.prod.right_unitor {C : Type u} (P : C)  :
P ⊤_ C P

The right unitor isomorphism for binary products with the terminal object.

Equations
@[simp]
theorem category_theory.limits.prod.left_unitor_hom_naturality_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
=
theorem category_theory.limits.prod.left_unitor_inv_naturality_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : ⊤_ C Y X') :
=
theorem category_theory.limits.prod.right_unitor_hom_naturality_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
=
theorem category_theory.limits.prod_right_unitor_inv_naturality_assoc {C : Type u} {X Y : C} (f : X Y) {X' : C} (f' : Y ⊤_ C X') :
=
@[simp]
@[simp]
noncomputable def category_theory.limits.coprod.braiding {C : Type u} (P Q : C) :
P ⨿ Q Q ⨿ P

The braiding isomorphism which swaps a binary coproduct.

Equations
theorem category_theory.limits.coprod.symmetry {C : Type u} (P Q : C) :
= 𝟙 (P ⨿ Q)

The braiding isomorphism is symmetric.

noncomputable def category_theory.limits.coprod.associator {C : Type u} (P Q R : C) :
P ⨿ Q ⨿ R P ⨿ (Q ⨿ R)

The associator isomorphism for binary coproducts.

Equations
theorem category_theory.limits.coprod.pentagon {C : Type u} (W X Y Z : C) :
= Z).hom (Y ⨿ Z)).hom
theorem category_theory.limits.coprod.associator_naturality {C : Type u} {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :
@[simp]
noncomputable def category_theory.limits.coprod.left_unitor {C : Type u} (P : C) :
⊥_ C ⨿ P P

The left unitor isomorphism for binary coproducts with the initial object.

Equations
@[simp]
noncomputable def category_theory.limits.coprod.right_unitor {C : Type u} (P : C) :
P ⨿ ⊥_ C P

The right unitor isomorphism for binary coproducts with the initial object.

Equations
@[simp]
@[simp]
@[simp]
theorem category_theory.limits.prod.functor_obj_obj {C : Type u} (X Y : C) :
= (X Y)
@[simp]
theorem category_theory.limits.prod.functor_obj_map {C : Type u} (X Y Z : C) (g : Y Z) :
@[simp]
theorem category_theory.limits.prod.functor_map_app {C : Type u} (Y Z : C) (f : Y Z) (T : C) :
noncomputable def category_theory.limits.prod.functor {C : Type u}  :
C C C

The binary product functor.

Equations
noncomputable def category_theory.limits.prod.functor_left_comp {C : Type u} (X Y : C) :

The product functor can be decomposed.

Equations
@[simp]
theorem category_theory.limits.coprod.functor_obj_obj {C : Type u} (X Y : C) :
= (X ⨿ Y)
noncomputable def category_theory.limits.coprod.functor {C : Type u}  :
C C C

The binary coproduct functor.

Equations
@[simp]
theorem category_theory.limits.coprod.functor_obj_map {C : Type u} (X Y Z : C) (g : Y Z) :
@[simp]
theorem category_theory.limits.coprod.functor_map_app {C : Type u} (Y Z : C) (f : Y Z) (T : C) :

The coproduct functor can be decomposed.

Equations
noncomputable def category_theory.limits.prod_comparison {C : Type u} {D : Type u₂} (F : C D) (A B : C) [ (F.obj B)] :
F.obj (A B) F.obj A F.obj B

The product comparison morphism.

In `category_theory/limits/preserves` we show this is always an iso iff F preserves binary products.

Equations
Instances for `category_theory.limits.prod_comparison`
@[simp]
theorem category_theory.limits.prod_comparison_fst_assoc {C : Type u} {D : Type u₂} (F : C D) {A B : C} [ (F.obj B)] {X' : D} (f' : F.obj A X') :
@[simp]
theorem category_theory.limits.prod_comparison_fst {C : Type u} {D : Type u₂} (F : C D) {A B : C} [ (F.obj B)] :
@[simp]
theorem category_theory.limits.prod_comparison_snd_assoc {C : Type u} {D : Type u₂} (F : C D) {A B : C} [ (F.obj B)] {X' : D} (f' : F.obj B X') :
@[simp]
theorem category_theory.limits.prod_comparison_snd {C : Type u} {D : Type u₂} (F : C D) {A B : C} [ (F.obj B)] :
theorem category_theory.limits.prod_comparison_natural_assoc {C : Type u} {D : Type u₂} (F : C D) {A A' B B' : C} [ (F.obj B)] [ (F.obj B')] (f : A A') (g : B B') {X' : D} (f' : F.obj A' F.obj B' X') :
f' = (F.map g) f'
theorem category_theory.limits.prod_comparison_natural {C : Type u} {D : Type u₂} (F : C D) {A A' B B' : C} [ (F.obj B)] [ (F.obj B')] (f : A A') (g : B B') :
= (F.map g)

Naturality of the prod_comparison morphism in both arguments.

noncomputable def category_theory.limits.prod_comparison_nat_trans {C : Type u} {D : Type u₂} (F : C D) (A : C) :

The product comparison morphism from `F(A ⨯ -)` to `FA ⨯ F-`, whose components are given by `prod_comparison`.

Equations
@[simp]