# 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.

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

@[reducible]
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) (X : category_theory.discrete β) :
X = p X.as
@[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) (X : category_theory.discrete β) :
X = p X.as
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.fan.proj {β : Type w} {C : Type u} {f : β → C} (j : β) :
p.X f j

Get the jth map in the fan

Equations
@[simp]
theorem category_theory.limits.fan_mk_proj {β : Type w} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), P f b) (j : β) :
= p j
@[reducible]
def category_theory.limits.has_product {β : Type w} {C : Type u} (f : β → C) :
Prop

An abbreviation for has_limit (discrete.functor f).

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

An abbreviation for has_colimit (discrete.functor f).

@[simp]
theorem category_theory.limits.mk_fan_limit_lift {β : Type w} {C : Type u} {f : β → C} (lift : Π (s : , s.X t.X) (fac : ∀ (s : (j : β), lift s t.proj j = s.proj j) (uniq : ∀ (s : (m : s.X t.X), (∀ (j : β), m t.proj j = s.proj j)m = lift s)  :
fac uniq).lift s = lift s
def category_theory.limits.mk_fan_limit {β : Type w} {C : Type u} {f : β → C} (lift : Π (s : , s.X t.X) (fac : ∀ (s : (j : β), lift s t.proj j = s.proj j) (uniq : ∀ (s : (m : s.X t.X), (∀ (j : β), m t.proj j = s.proj j)m = lift s) :

Make a fan f into a limit fan by providing lift, fac, and uniq -- just a convenience lemma to avoid having to go through discrete

Equations
@[reducible]
def category_theory.limits.has_products_of_shape (β : Type v) (C : Type u_1)  :
Prop

An abbreviation for has_limits_of_shape (discrete f).

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

An abbreviation for has_colimits_of_shape (discrete f).

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

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

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

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

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

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

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

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

@[reducible]
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
Instances for category_theory.limits.pi_comparison
@[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
Instances for category_theory.limits.sigma_comparison
@[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))
@[reducible]
def category_theory.limits.has_products (C : Type u)  :
Prop

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

@[reducible]
def category_theory.limits.has_coproducts (C : Type u)  :
Prop

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

theorem category_theory.limits.has_products_of_limit_fans {C : Type u} (lf : Π {J : Type w} (f : J → C), ) (lf_is_limit : Π {J : Type w} (f : J → C), ) :

(Co)products over a type with a unique term.

@[simp]
theorem category_theory.limits.limit_cone_of_unique_is_limit_lift {β : Type w} {C : Type u} [unique β] (f : β → C)  :
@[simp]
theorem category_theory.limits.limit_cone_of_unique_cone_π_app {β : Type w} {C : Type u} [unique β] (f : β → C) (j : category_theory.discrete β) :
@[simp]
theorem category_theory.limits.limit_cone_of_unique_cone_X {β : Type w} {C : Type u} [unique β] (f : β → C) :
def category_theory.limits.limit_cone_of_unique {β : Type w} {C : Type u} [unique β] (f : β → C) :

The limit cone for the product over an index type with exactly one term.

Equations
@[protected, instance]
def category_theory.limits.has_product_unique {β : Type w} {C : Type u} [unique β] (f : β → C) :
noncomputable def category_theory.limits.product_unique_iso {β : Type w} {C : Type u} [unique β] (f : β → C) :

A product over a index type with exactly one term is just the object over that term.

Equations
@[simp]
theorem category_theory.limits.product_unique_iso_hom {β : Type w} {C : Type u} [unique β] (f : β → C) :
@[simp]
theorem category_theory.limits.product_unique_iso_inv {β : Type w} {C : Type u} [unique β] (f : β → C) :
@[simp]
theorem category_theory.limits.colimit_cocone_of_unique_cocone_X {β : Type w} {C : Type u} [unique β] (f : β → C) :
@[simp]
theorem category_theory.limits.colimit_cocone_of_unique_is_colimit_desc {β : Type w} {C : Type u} [unique β] (f : β → C)  :
def category_theory.limits.colimit_cocone_of_unique {β : Type w} {C : Type u} [unique β] (f : β → C) :

The colimit cocone for the coproduct over an index type with exactly one term.

Equations
@[simp]
theorem category_theory.limits.colimit_cocone_of_unique_cocone_ι_app {β : Type w} {C : Type u} [unique β] (f : β → C) (j : category_theory.discrete β) :
@[protected, instance]
def category_theory.limits.has_coproduct_unique {β : Type w} {C : Type u} [unique β] (f : β → C) :
noncomputable def category_theory.limits.coproduct_unique_iso {β : Type w} {C : Type u} [unique β] (f : β → C) :

A coproduct over a index type with exactly one term is just the object over that term.

Equations
@[simp]
theorem category_theory.limits.coproduct_unique_iso_inv {β : Type w} {C : Type u} [unique β] (f : β → C) :
@[simp]
theorem category_theory.limits.coproduct_unique_iso_hom {β : Type w} {C : Type u} [unique β] (f : β → C) :
noncomputable def category_theory.limits.pi.reindex {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C)  :
f ε f

Reindex a categorical product via an equivalence of the index types.

Equations
@[simp]
theorem category_theory.limits.pi.reindex_hom_π_assoc {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C) (b : β) {X' : C} (f' : f (ε b) X') :
(ε b) f' = b f'
@[simp]
theorem category_theory.limits.pi.reindex_hom_π {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C) (b : β) :
= b
@[simp]
theorem category_theory.limits.pi.reindex_inv_π {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C) (b : β) :
= (ε b)
@[simp]
theorem category_theory.limits.pi.reindex_inv_π_assoc {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C) (b : β) {X' : C} (f' : (f ε) b X') :
b f' = (ε b) f'
noncomputable def category_theory.limits.sigma.reindex {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C)  :
f ε f

Reindex a categorical coproduct via an equivalence of the index types.

Equations
@[simp]
theorem category_theory.limits.sigma.ι_reindex_hom {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C) (b : β) :
=
@[simp]
theorem category_theory.limits.sigma.ι_reindex_hom_assoc {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C) (b : β) {X' : C} (f' : f X') :
b = f'
@[simp]
theorem category_theory.limits.sigma.ι_reindex_inv {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C) (b : β) :
= b
@[simp]
theorem category_theory.limits.sigma.ι_reindex_inv_assoc {β : Type w} {C : Type u} {γ : Type v} (ε : β γ) (f : γ → C) (b : β) {X' : C} (f' : f ε X') :
= b f'