# mathlibdocumentation

category_theory.limits.shapes.products

def category_theory.limits.fan {β : Type v} {C : Type u}  :
(β → C)Type (max 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 v} {C : Type u}  :
(β → C)Type (max 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 v} {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 v} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), P f b) :
= P

def category_theory.limits.fan.mk {β : Type v} {C : Type u} {f : β → C} (P : C) :
(Π (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 v} {C : Type u} {f : β → C} (P : C) (p : Π (b : β), f b P) :

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

def category_theory.limits.cofan.mk {β : Type v} {C : Type u} {f : β → C} (P : C) :
(Π (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 v} {C : Type u}  :
(β → C) → Prop

An abbreviation for has_limit (discrete.functor f).

Instances
def category_theory.limits.has_coproduct {β : Type v} {C : Type u}  :
(β → 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).

def category_theory.limits.pi_obj {β : Type v} {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.)

def category_theory.limits.sigma_obj {β : Type v} {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.)

def category_theory.limits.pi.π {β : Type v} {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.

def category_theory.limits.sigma.ι {β : Type v} {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.

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

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

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

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

def category_theory.limits.pi.map {β : Type v} {C : Type u} {f g : β → C}  :
(Π (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.

def category_theory.limits.pi.map_iso {β : Type v} {C : Type u} {f g : β → C}  :
(Π (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.

def category_theory.limits.sigma.map {β : Type v} {C : Type u} {f g : β → C}  :
(Π (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.

def category_theory.limits.sigma.map_iso {β : Type v} {C : Type u} {f g : β → C}  :
(Π (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.

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

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

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

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