def
category_theory.limits.fan
{β : Type v}
{C : Type u}
[category_theory.category C] :
(β → C) → Type (max u v)
def
category_theory.limits.cofan
{β : Type v}
{C : Type u}
[category_theory.category C] :
(β → C) → Type (max u v)
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
Equations
- category_theory.limits.fan.mk p = {X := P, π := {app := p, naturality' := _}}
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
Equations
- category_theory.limits.cofan.mk p = {X := P, ι := {app := p, naturality' := _}}
@[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).π.app b = p b
@[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).ι.app b = p b
def
category_theory.limits.has_product
{β : Type v}
{C : Type u}
[category_theory.category C] :
(β → C) → Type (max u v)
An abbreviation for has_limit (discrete.functor f).
def
category_theory.limits.has_coproduct
{β : Type v}
{C : Type u}
[category_theory.category C] :
(β → C) → Type (max u v)
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] :
Type (max u_1 v)
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] :
Type (max u_1 v)
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 : β) :
def
category_theory.limits.sigma.ι
{β : Type v}
{C : Type u}
[category_theory.category C]
(f : β → C)
[category_theory.limits.has_coproduct f]
(b : β) :
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} :
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} :
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] :
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] :
def
category_theory.limits.has_products
(C : Type u)
[category_theory.category C] :
Type (max (v+1) u v)
An abbreviation for Π J, has_limits_of_shape (discrete J) C
def
category_theory.limits.has_coproducts
(C : Type u)
[category_theory.category C] :
Type (max (v+1) u v)
An abbreviation for Π J, has_colimits_of_shape (discrete J) C