A fan over f : β → C
consists of a collection of maps from an object P
to every f b
.
A cofan over f : β → C
consists of a collection of maps from every f b
to an object P
.
A fan over f : β → C
consists of a collection of maps from an object P
to every f b
.
Equations
- category_theory.limits.fan.mk P p = {X := P, π := {app := p, naturality' := _}}
A cofan over f : β → C
consists of a collection of maps from every f b
to an object P
.
Equations
- category_theory.limits.cofan.mk P p = {X := P, ι := {app := p, naturality' := _}}
An abbreviation for has_limit (discrete.functor f)
.
An abbreviation for has_colimit (discrete.functor f)
.
An abbreviation for has_limits_of_shape (discrete f)
.
An abbreviation for has_colimits_of_shape (discrete f)
.
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.)
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.)
The b
-th projection from the pi object over f
has the form ∏ f ⟶ f b
.
The b
-th inclusion into the sigma object over f
has the form f b ⟶ ∐ f
.
The fan constructed of the projections from the product is limiting.
A collection of morphisms P ⟶ f b
induces a morphism P ⟶ ∏ f
.
A collection of morphisms f b ⟶ P
induces a morphism ∐ f ⟶ P
.
Construct a morphism between categorical products (indexed by the same type) from a family of morphisms between the factors.
Construct an isomorphism between categorical products (indexed by the same type) from a family of isomorphisms between the factors.
Construct a morphism between categorical coproducts (indexed by the same type) from a family of morphisms between the factors.
Construct an isomorphism between categorical coproducts (indexed by the same type) from a family of isomorphisms between the factors.
The comparison morphism for the product of f
.
Equations
- category_theory.limits.pi_comparison G f = category_theory.limits.pi.lift (λ (b : β), G.map (category_theory.limits.pi.π f b))
The comparison morphism for the coproduct of f
.
Equations
- category_theory.limits.sigma_comparison G f = category_theory.limits.sigma.desc (λ (b : β), G.map (category_theory.limits.sigma.ι f b))
An abbreviation for Π J, has_limits_of_shape (discrete J) C
Instances
An abbreviation for Π J, has_colimits_of_shape (discrete J) C