mathlibdocumentation

category_theory.limits.shapes.products

Categorical (co)products #

This file defines (co)products as special cases of (co)limits.

A product is the categorical generalization of the object Π i, f i where f : ι → C. It is a limit cone over the diagram formed by f, implemented by converting f into a functor discrete ι ⥤ C.

A coproduct is the dual concept.

Main definitions #

• a fan is a cone over a discrete category
• fan.mk constructs a fan from an indexed collection of maps
• a pi is a limit (discrete.functor f)

Each of these has a dual.

Implementation notes #

As with the other special shapes in the limits library, all the definitions here are given as abbreviations of the general statements for limits, so all the simp lemmas and theorems about general limits can be used.

def category_theory.limits.fan {β : Type w} {C : Type u} (f : β → C) :
Type (max w u v)

A fan over f : β → C consists of a collection of maps from an object P to every f b.

def category_theory.limits.cofan {β : Type w} {C : Type u} (f : β → C) :
Type (max w u v)

A cofan over f : β → C consists of a collection of maps from every f b to an object P.

@[simp]
theorem category_theory.limits.fan.mk_π_app {β : Type w} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), P f b) (b : β) :
b = p b
@[simp]
theorem category_theory.limits.fan.mk_X {β : Type w} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), P f b) :
= P
def category_theory.limits.fan.mk {β : Type w} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), P f b) :

A fan over f : β → C consists of a collection of maps from an object P to every f b.

Equations
@[simp]
theorem category_theory.limits.cofan.mk_X {β : Type w} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), f b P) :
@[simp]
theorem category_theory.limits.cofan.mk_ι_app {β : Type w} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), f b P) (b : β) :
b = p b
def category_theory.limits.cofan.mk {β : Type w} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), f b P) :

A cofan over f : β → C consists of a collection of maps from every f b to an object P.

Equations
def category_theory.limits.has_product {β : Type w} {C : Type u} (f : β → C) :
Prop

An abbreviation for has_limit (discrete.functor f).

def category_theory.limits.has_coproduct {β : Type w} {C : Type u} (f : β → C) :
Prop

An abbreviation for has_colimit (discrete.functor f).

def category_theory.limits.has_products_of_shape (β : Type v) (C : Type u_1)  :
Prop

An abbreviation for has_limits_of_shape (discrete f).

def category_theory.limits.has_coproducts_of_shape (β : Type v) (C : Type u_1)  :
Prop

An abbreviation for has_colimits_of_shape (discrete f).

noncomputable def category_theory.limits.pi_obj {β : Type w} {C : Type u} (f : β → C)  :
C

pi_obj f computes the product of a family of elements f. (It is defined as an abbreviation for limit (discrete.functor f), so for most facts about pi_obj f, you will just use general facts about limits.)

noncomputable def category_theory.limits.sigma_obj {β : Type w} {C : Type u} (f : β → C)  :
C

sigma_obj f computes the coproduct of a family of elements f. (It is defined as an abbreviation for colimit (discrete.functor f), so for most facts about sigma_obj f, you will just use general facts about colimits.)

noncomputable def category_theory.limits.pi.π {β : Type w} {C : Type u} (f : β → C) (b : β) :
f f b

The b-th projection from the pi object over f has the form ∏ f ⟶ f b.

noncomputable def category_theory.limits.sigma.ι {β : Type w} {C : Type u} (f : β → C) (b : β) :
f b f

The b-th inclusion into the sigma object over f has the form f b ⟶ ∐ f.

noncomputable def category_theory.limits.product_is_product {β : Type w} {C : Type u} (f : β → C)  :

The fan constructed of the projections from the product is limiting.

Equations
noncomputable def category_theory.limits.coproduct_is_coproduct {β : Type w} {C : Type u} (f : β → C)  :

The cofan constructed of the inclusions from the coproduct is colimiting.

Equations
noncomputable def category_theory.limits.pi.lift {β : Type w} {C : Type u} {f : β → C} {P : C} (p : Π (b : β), P f b) :
P f

A collection of morphisms P ⟶ f b induces a morphism P ⟶ ∏ f.

noncomputable def category_theory.limits.sigma.desc {β : Type w} {C : Type u} {f : β → C} {P : C} (p : Π (b : β), f b P) :
f P

A collection of morphisms f b ⟶ P induces a morphism ∐ f ⟶ P.

noncomputable def category_theory.limits.pi.map {β : Type w} {C : Type u} {f g : β → C} (p : Π (b : β), f b g b) :
f g

Construct a morphism between categorical products (indexed by the same type) from a family of morphisms between the factors.

noncomputable def category_theory.limits.pi.map_iso {β : Type w} {C : Type u} {f g : β → C} (p : Π (b : β), f b g b) :
f g

Construct an isomorphism between categorical products (indexed by the same type) from a family of isomorphisms between the factors.

noncomputable def category_theory.limits.sigma.map {β : Type w} {C : Type u} {f g : β → C} (p : Π (b : β), f b g b) :
f g

Construct a morphism between categorical coproducts (indexed by the same type) from a family of morphisms between the factors.

noncomputable def category_theory.limits.sigma.map_iso {β : Type w} {C : Type u} {f g : β → C} (p : Π (b : β), f b g b) :
f g

Construct an isomorphism between categorical coproducts (indexed by the same type) from a family of isomorphisms between the factors.

noncomputable def category_theory.limits.pi_comparison {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_product (λ (b : β), G.obj (f b))] :
G.obj ( f) λ (b : β), G.obj (f b)

The comparison morphism for the product of f. This is an iso iff G preserves the product of f, see preserves_product.of_iso_comparison.

Equations
@[simp]
theorem category_theory.limits.pi_comparison_comp_π {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (b : β) :
category_theory.limits.pi.π (λ (b : β), G.obj (f b)) b = G.map
@[simp]
theorem category_theory.limits.pi_comparison_comp_π_assoc {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (b : β) {X' : D} (f' : G.obj (f b) X') :
category_theory.limits.pi.π (λ (b : β), G.obj (f b)) b f' = G.map f'
@[simp]
theorem category_theory.limits.map_lift_pi_comparison {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), P f j) :
= category_theory.limits.pi.lift (λ (j : β), G.map (g j))
@[simp]
theorem category_theory.limits.map_lift_pi_comparison_assoc {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), P f j) {X' : D} (f' : ( λ (b : β), G.obj (f b)) X') :
= category_theory.limits.pi.lift (λ (j : β), G.map (g j)) f'
noncomputable def category_theory.limits.sigma_comparison {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] :
( λ (b : β), G.obj (f b)) G.obj ( f)

The comparison morphism for the coproduct of f. This is an iso iff G preserves the coproduct of f, see preserves_coproduct.of_iso_comparison.

Equations
@[simp]
theorem category_theory.limits.ι_comp_sigma_comparison_assoc {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (b : β) {X' : D} (f' : G.obj ( f) X') :
category_theory.limits.sigma.ι (λ (b : β), G.obj (f b)) b = f'
@[simp]
theorem category_theory.limits.ι_comp_sigma_comparison {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (b : β) :
category_theory.limits.sigma.ι (λ (b : β), G.obj (f b)) b =
@[simp]
theorem category_theory.limits.sigma_comparison_map_desc_assoc {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), f j P) {X' : D} (f' : G.obj P X') :
= category_theory.limits.sigma.desc (λ (j : β), G.map (g j)) f'
@[simp]
theorem category_theory.limits.sigma_comparison_map_desc {β : Type w} {C : Type u} {D : Type u₂} (G : C D) (f : β → C) [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), f j P) :
= category_theory.limits.sigma.desc (λ (j : β), G.map (g j))
def category_theory.limits.has_products (C : Type u)  :
Prop

An abbreviation for Π J, has_limits_of_shape (discrete J) C

def category_theory.limits.has_coproducts (C : Type u)  :
Prop

An abbreviation for Π J, has_colimits_of_shape (discrete J) C