category_theory.limits.shapes.finite_products

@[class]

structure category_theory.limits.has_finite_products (C : Type u) [category_theory.category C] :

Prop

out : ∀ (J : Type ?) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_limits_of_shape (category_theory.discrete J) C

A category has finite products if there is a chosen limit for every diagram with shape discrete J, where we have [decidable_eq J] and [fintype J].

Instances

source

@[instance]

def category_theory.limits.has_limits_of_shape_discrete (C : Type u) [category_theory.category C] (J : Type v) [fintype J] [category_theory.limits.has_finite_products C] :

category_theory.limits.has_limits_of_shape (category_theory.discrete J) C

source

theorem category_theory.limits.has_finite_products_of_has_finite_limits (C : Type u) [category_theory.category C] [category_theory.limits.has_finite_limits C] :

category_theory.limits.has_finite_products C

If C has finite limits then it has finite products.

source

theorem category_theory.limits.has_finite_products_of_has_products (C : Type u) [category_theory.category C] [category_theory.limits.has_products C] :

category_theory.limits.has_finite_products C

If a category has all products then in particular it has finite products.

source

@[class]

structure category_theory.limits.has_finite_coproducts (C : Type u) [category_theory.category C] :

Prop

out : ∀ (J : Type ?) [_inst_2 : decidable_eq J] [_inst_3 : fintype J], category_theory.limits.has_colimits_of_shape (category_theory.discrete J) C

A category has finite coproducts if there is a chosen colimit for every diagram with shape discrete J, where we have [decidable_eq J] and [fintype J].

Instances

source

@[instance]

def category_theory.limits.has_colimits_of_shape_discrete (C : Type u) [category_theory.category C] (J : Type v) [fintype J] [category_theory.limits.has_finite_coproducts C] :

category_theory.limits.has_colimits_of_shape (category_theory.discrete J) C

source

theorem category_theory.limits.has_finite_coproducts_of_has_finite_colimits (C : Type u) [category_theory.category C] [category_theory.limits.has_finite_colimits C] :

category_theory.limits.has_finite_coproducts C

If C has finite colimits then it has finite coproducts.

source

theorem category_theory.limits.has_finite_coproducts_of_has_coproducts (C : Type u) [category_theory.category C] [category_theory.limits.has_coproducts C] :

category_theory.limits.has_finite_coproducts C

If a category has all coproducts then in particular it has finite coproducts.