mathlib documentation

category_theory.limits.shapes.products

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

@[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) :

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

@[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 : β) :

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

An abbreviation for has_limit (discrete.functor f).

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

An abbreviation for has_colimit (discrete.functor f).

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

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

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

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

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.

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.

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} (p : Π (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} [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.

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

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] (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.

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

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] (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.

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

Equations
@[simp]

@[simp]
theorem category_theory.limits.pi_comparison_comp_π_assoc {β : Type v} {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') :

@[simp]
theorem category_theory.limits.map_lift_pi_comparison {β : Type v} {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) :

@[simp]
theorem category_theory.limits.map_lift_pi_comparison_assoc {β : Type v} {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') :

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

Equations
@[simp]
theorem category_theory.limits.ι_comp_sigma_comparison_assoc {β : Type v} {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') :

@[simp]
theorem category_theory.limits.sigma_comparison_map_desc_assoc {β : Type v} {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') :

@[simp]
theorem category_theory.limits.sigma_comparison_map_desc {β : Type v} {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) :

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

Instances

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