Categorical (co)products #
This file defines (co)products as special cases of (co)limits.
A product is the categorical generalization of the object Π i, f i
where f : ι → C
. It is a
limit cone over the diagram formed by f
, implemented by converting f
into a functor
Discrete ι ⥤ C
.
A coproduct is the dual concept.
Main definitions #
- a
Fan
is a cone over a discrete category Fan.mk
constructs a fan from an indexed collection of maps- a
Pi
is alimit (Discrete.functor f)
Each of these has a dual.
Implementation notes #
As with the other special shapes in the limits library, all the definitions here are given as
abbreviation
s of the general statements for limits, so all the simp
lemmas and theorems about
general limits can be used.
A fan over f : β → C
consists of a collection of maps from an object P
to every f b
.
Instances For
A cofan over f : β → C
consists of a collection of maps from every f b
to an object P
.
Instances For
A fan over f : β → C
consists of a collection of maps from an object P
to every f b
.
Instances For
A cofan over f : β → C
consists of a collection of maps from every f b
to an object P
.
Instances For
Get the j
th map in the fan
Instances For
Get the j
th map in the cofan
Instances For
An abbreviation for HasLimit (Discrete.functor f)
.
Instances For
An abbreviation for HasColimit (Discrete.functor f)
.
Instances For
Make a fan f
into a limit fan by providing lift
, fac
, and uniq
--
just a convenience lemma to avoid having to go through Discrete
Instances For
Make a cofan f
into a colimit cofan by providing desc
, fac
, and uniq
--
just a convenience lemma to avoid having to go through Discrete
Instances For
An abbreviation for HasLimitsOfShape (Discrete f)
.
Instances For
An abbreviation for HasColimitsOfShape (Discrete f)
.
Instances For
piObj 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 piObj f
, you will just use general facts about limits.)
Instances For
sigmaObj 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 sigmaObj f
, you will just use general facts about colimits.)
Instances For
notation for categorical products
Instances For
notation for categorical coproducts
Instances For
The b
-th projection from the pi object over f
has the form ∏ f ⟶ f b
.
Instances For
The b
-th inclusion into the sigma object over f
has the form f b ⟶ ∐ f
.
Instances For
The fan constructed of the projections from the product is limiting.
Instances For
The cofan constructed of the inclusions from the coproduct is colimiting.
Instances For
A collection of morphisms P ⟶ f b
induces a morphism P ⟶ ∏ f
.
Instances For
A collection of morphisms f b ⟶ P
induces a morphism ∐ f ⟶ P
.
Instances For
Construct a morphism between categorical products (indexed by the same type) from a family of morphisms between the factors.
Instances For
Construct a morphism between categorical products from a family of morphisms between the factors.
Instances For
Construct an isomorphism between categorical products (indexed by the same type) from a family of isomorphisms between the factors.
Instances For
Construct a morphism between categorical coproducts (indexed by the same type) from a family of morphisms between the factors.
Instances For
Construct a morphism between categorical coproducts from a family of morphisms between the factors.
Instances For
Construct an isomorphism between categorical coproducts (indexed by the same type) from a family of isomorphisms between the factors.
Instances For
Two products which differ by an equivalence in the indexing type, and up to isomorphism in the factors, are isomorphic.
Instances For
Two coproducts which differ by an equivalence in the indexing type, and up to isomorphism in the factors, are isomorphic.
Instances For
An iterated product is a product over a sigma type.
Instances For
An iterated coproduct is a coproduct over a sigma type.
Instances For
The comparison morphism for the product of f
. This is an iso iff G
preserves the product
of f
, see PreservesProduct.ofIsoComparison
.
Instances For
The comparison morphism for the coproduct of f
. This is an iso iff G
preserves the coproduct
of f
, see PreservesCoproduct.ofIsoComparison
.
Instances For
An abbreviation for Π J, HasLimitsOfShape (Discrete J) C
Instances For
An abbreviation for Π J, HasColimitsOfShape (Discrete J) C
Instances For
(Co)products over a type with a unique term.
The limit cone for the product over an index type with exactly one term.
Instances For
A product over an index type with exactly one term is just the object over that term.
Instances For
The colimit cocone for the coproduct over an index type with exactly one term.
Instances For
A coproduct over an index type with exactly one term is just the object over that term.
Instances For
Reindex a categorical product via an equivalence of the index types.
Instances For
Reindex a categorical coproduct via an equivalence of the index types.