mathlib documentation

category_theory.limits.shapes.binary_products

Binary (co)products #

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 #

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

Instances for category_theory.limits.walking_pair

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

Equations

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

Equations

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} [category_theory.category C] (X Y : C) :
Type (max u v)

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

def category_theory.limits.binary_fan.is_limit.mk {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_fan X Y) (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} [category_theory.category C] {W X Y : C} {s : category_theory.limits.binary_fan X Y} (h : category_theory.limits.is_limit s) {f g : W s.X} (h₁ : f s.fst = g s.fst) (h₂ : f s.snd = g s.snd) :
f = g
@[reducible]

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

def category_theory.limits.binary_cofan.is_colimit.mk {C : Type u} [category_theory.category C] {X Y : C} (s : category_theory.limits.binary_cofan X Y) (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
@[simp]
theorem category_theory.limits.binary_fan.mk_X {C : Type u} [category_theory.category C] {X Y P : C} (π₁ : P X) (π₂ : P Y) :
def category_theory.limits.binary_fan.mk {C : Type u} [category_theory.category C] {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} [category_theory.category C] {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} [category_theory.category C] {X Y P : C} (π₁ : P X) (π₂ : P Y) :
@[simp]
theorem category_theory.limits.binary_fan.mk_snd {C : Type u} [category_theory.category C] {X Y P : C} (π₁ : P X) (π₂ : P Y) :
@[simp]
theorem category_theory.limits.binary_cofan.mk_inl {C : Type u} [category_theory.category C] {X Y P : C} (ι₁ : X P) (ι₂ : Y P) :
@[simp]
theorem category_theory.limits.binary_cofan.mk_inr {C : Type u} [category_theory.category C] {X Y P : C} (ι₁ : X P) (ι₂ : Y P) :
def category_theory.limits.binary_fan.is_limit_mk {C : Type u} [category_theory.category C] {X Y W : C} {fst : W X} {snd : W Y} (lift : Π (s : category_theory.limits.binary_fan X Y), s.X W) (fac_left : (s : category_theory.limits.binary_fan X Y), lift s fst = s.fst) (fac_right : (s : category_theory.limits.binary_fan X Y), lift s snd = s.snd) (uniq : (s : category_theory.limits.binary_fan X Y) (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} [category_theory.category C] {X Y W : C} {inl : X W} {inr : Y W} (desc : Π (s : category_theory.limits.binary_cofan X Y), W s.X) (fac_left : (s : category_theory.limits.binary_cofan X Y), inl desc s = s.inl) (fac_right : (s : category_theory.limits.binary_cofan X Y), inr desc s = s.inr) (uniq : (s : category_theory.limits.binary_cofan X Y) (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

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

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
@[reducible]

An abbreviation for has_limit (pair X Y).

@[reducible]

An abbreviation for has_colimit (pair X Y).

@[reducible]

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

@[reducible]

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

@[reducible]

The projection map to the first component of the product.

@[reducible]

The projecton map to the second component of the product.

@[reducible]

The inclusion map from the first component of the coproduct.

@[reducible]

The inclusion map from the second component of the coproduct.

@[reducible]
noncomputable def category_theory.limits.prod.lift {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_product X Y] (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]

diagonal arrow of the binary product in the category fam I

@[reducible]
noncomputable def category_theory.limits.coprod.desc {C : Type u} [category_theory.category C] {W X Y : C} [category_theory.limits.has_binary_coproduct X Y] (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]

codiagonal arrow of the binary coproduct

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

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

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

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
@[simp]
theorem category_theory.limits.prod.map_map_assoc {C : Type u} [category_theory.category C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [category_theory.limits.has_binary_product A₁ B₁] [category_theory.limits.has_binary_product A₂ B₂] [category_theory.limits.has_binary_product A₃ B₃] (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) {X' : C} (f' : A₃ B₃ X') :
@[simp]

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
@[simp]
theorem category_theory.limits.coprod.map_map_assoc {C : Type u} [category_theory.category C] {A₁ A₂ A₃ B₁ B₂ B₃ : C} [category_theory.limits.has_binary_coproduct A₁ B₁] [category_theory.limits.has_binary_coproduct A₂ B₂] [category_theory.limits.has_binary_coproduct A₃ B₃] (f : A₁ A₂) (g : B₁ B₂) (h : A₂ A₃) (k : B₂ B₃) {X' : C} (f' : A₃ ⨿ B₃ X') :

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
@[reducible]

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

See https://stacks.math.columbia.edu/tag/001T.

@[reducible]

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

See https://stacks.math.columbia.edu/tag/04AP.

theorem category_theory.limits.prod.associator_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.limits.has_binary_products C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) {X' : C} (f' : Y₁ (Y₂ Y₃) X') :

The binary product functor.

Equations

The binary coproduct functor.

Equations

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

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

Equations