mathlib documentation

category_theory.limits.shapes.products

source
def category_theory.limits.fan {β : Type v} {C : Type u} [category_theory.category C] :
(β → C) → Type (max 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 v} {C : Type u} [category_theory.category C] :
(β → C) → Type (max 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 v} {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 v} {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 v} {C : Type u} [category_theory.category C] {f : β → C} (P : C) :
(Π (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 v} {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 v} {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 v} {C : Type u} [category_theory.category C] {f : β → C} (P : C) :
(Π (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 v} {C : Type u} [category_theory.category C] :
(β → C) → Prop

An abbreviation for has_limit (discrete.functor f).

Instances
source
def category_theory.limits.has_coproduct {β : Type v} {C : Type u} [category_theory.category C] :
(β → 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
def category_theory.limits.pi_obj {β : Type v} {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
def category_theory.limits.sigma_obj {β : Type v} {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
def category_theory.limits.pi.π {β : Type v} {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
def category_theory.limits.sigma.ι {β : Type v} {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
def category_theory.limits.pi.lift {β : Type v} {C : Type u} [category_theory.category C] {f : β → C} [category_theory.limits.has_product f] {P : C} :
(Π (b : β), P ⟶ f b) → (P ⟶ ∏ f)

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

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

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

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

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

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

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

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

Instances
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