mathlib documentation

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 #

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.

source
def category_theory.limits.fan {β : Type w} {C : Type u} [category_theory.category C] (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.

source
def category_theory.limits.cofan {β : Type w} {C : Type u} [category_theory.category C] (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.

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

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

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

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

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

An abbreviation for has_limit (discrete.functor f).

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

An abbreviation for has_colimit (discrete.functor f).

source
def category_theory.limits.has_products_of_shape (β : Type v) (C : Type u_1) [category_theory.category C] :
Prop

An abbreviation for has_limits_of_shape (discrete f).

source
def category_theory.limits.has_coproducts_of_shape (β : Type v) (C : Type u_1) [category_theory.category C] :
Prop

An abbreviation for has_colimits_of_shape (discrete f).

source
noncomputable def category_theory.limits.pi_obj {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_product f] :
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.)

source
noncomputable def category_theory.limits.sigma_obj {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_coproduct f] :
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.)

source
noncomputable def category_theory.limits.pi.π {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_product f] (b : β) :
∏ f ⟶ f b

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

source
noncomputable def category_theory.limits.sigma.ι {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_coproduct f] (b : β) :
f b ⟶ ∐ f

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

source
noncomputable def category_theory.limits.product_is_product {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_product f] :
category_theory.limits.is_limit (category_theory.limits.fan.mk (∏ f) (category_theory.limits.pi.π f))

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

Equations
source
noncomputable def category_theory.limits.coproduct_is_coproduct {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_coproduct f] :
category_theory.limits.is_colimit (category_theory.limits.cofan.mk (∐ f) (category_theory.limits.sigma.ι f))

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

Equations
source
noncomputable def category_theory.limits.pi.lift {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} [category_theory.limits.has_product f] {P : C} (p : Π (b : β), P ⟶ f b) :
P ⟶ ∏ f

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

source
noncomputable def category_theory.limits.sigma.desc {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} [category_theory.limits.has_coproduct f] {P : C} (p : Π (b : β), f b ⟶ P) :
∐ f ⟶ P

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

source
noncomputable def category_theory.limits.pi.map {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_product f] [category_theory.limits.has_product g] (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.

source
noncomputable def category_theory.limits.pi.map_iso {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_products_of_shape β 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.

source
noncomputable def category_theory.limits.sigma.map {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct g] (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.

source
noncomputable def category_theory.limits.sigma.map_iso {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_coproducts_of_shape β 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.

source
noncomputable def category_theory.limits.pi_comparison {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [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
source
@[simp]
theorem category_theory.limits.pi_comparison_comp_π {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (b : β) :
category_theory.limits.pi_comparison G f ≫ category_theory.limits.pi.π (λ (b : β), G.obj (f b)) b = G.map (category_theory.limits.pi.π f b)
source
@[simp]
theorem category_theory.limits.pi_comparison_comp_π_assoc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (b : β) {X' : D} (f' : G.obj (f b) ⟶ X') :
category_theory.limits.pi_comparison G f ≫ category_theory.limits.pi.π (λ (b : β), G.obj (f b)) b ≫ f' = G.map (category_theory.limits.pi.π f b) ≫ f'
source
@[simp]
theorem category_theory.limits.map_lift_pi_comparison {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), P ⟶ f j) :
G.map (category_theory.limits.pi.lift g) ≫ category_theory.limits.pi_comparison G f = category_theory.limits.pi.lift (λ (j : β), G.map (g j))
source
@[simp]
theorem category_theory.limits.map_lift_pi_comparison_assoc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [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') :
G.map (category_theory.limits.pi.lift g) ≫ category_theory.limits.pi_comparison G f ≫ f' = category_theory.limits.pi.lift (λ (j : β), G.map (g j)) ≫ f'
source
noncomputable def category_theory.limits.sigma_comparison {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [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
source
@[simp]
theorem category_theory.limits.ι_comp_sigma_comparison_assoc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [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 ≫ category_theory.limits.sigma_comparison G f ≫ f' = G.map (category_theory.limits.sigma.ι f b) ≫ f'
source
@[simp]
theorem category_theory.limits.ι_comp_sigma_comparison {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (b : β) :
category_theory.limits.sigma.ι (λ (b : β), G.obj (f b)) b ≫ category_theory.limits.sigma_comparison G f = G.map (category_theory.limits.sigma.ι f b)
source
@[simp]
theorem category_theory.limits.sigma_comparison_map_desc_assoc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [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_comparison G f ≫ G.map (category_theory.limits.sigma.desc g) ≫ f' = category_theory.limits.sigma.desc (λ (j : β), G.map (g j)) ≫ f'
source
@[simp]
theorem category_theory.limits.sigma_comparison_map_desc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), f j ⟶ P) :
category_theory.limits.sigma_comparison G f ≫ G.map (category_theory.limits.sigma.desc g) = category_theory.limits.sigma.desc (λ (j : β), G.map (g j))
source
def category_theory.limits.has_products (C : Type u) [category_theory.category C] :
Prop

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

source
def category_theory.limits.has_coproducts (C : Type u) [category_theory.category C] :
Prop

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