Constructing finite products from binary products and terminal. #
If a category has binary products and a terminal object then it has finite products. If a functor preserves binary products and the terminal object then it preserves finite products.
TODO #
Provide the dual results. Show the analogous results for functors which reflect or create (co)limits.
Given n+1
objects of C
, a fan for the last n
with point c₁.pt
and
a binary fan on c₁.pt
and f 0
, we can build a fan for all n+1
.
In extendFanIsLimit
we show that if the two given fans are limits, then this fan is also a
limit.
Instances For
Show that if the two given fans in extendFan
are limits, then the constructed fan is also a
limit.
Instances For
If C
has a terminal object and binary products, then it has finite products.
If F
preserves the terminal object and binary products, then it preserves products indexed by
Fin n
for any n
.
Equations
- One or more equations did not get rendered due to their size.
- CategoryTheory.preservesFinOfPreservesBinaryAndTerminal F 0 = fun f => inferInstance
Instances For
If F
preserves the terminal object and binary products, then it preserves limits of shape
Discrete (Fin n)
.
Instances For
If F
preserves the terminal object and binary products then it preserves finite products.
Instances For
Given n+1
objects of C
, a cofan for the last n
with point c₁.pt
and a binary cofan on c₁.X
and f 0
, we can build a cofan for all n+1
.
In extendCofanIsColimit
we show that if the two given cofans are colimits,
then this cofan is also a colimit.
Instances For
Show that if the two given cofans in extendCofan
are colimits,
then the constructed cofan is also a colimit.
Instances For
If C
has an initial object and binary coproducts, then it has finite coproducts.
If F
preserves the initial object and binary coproducts, then it preserves products indexed by
Fin n
for any n
.
Equations
- One or more equations did not get rendered due to their size.
- CategoryTheory.preservesFinOfPreservesBinaryAndInitial F 0 = fun f => inferInstance
Instances For
If F
preserves the initial object and binary coproducts, then it preserves colimits of shape
Discrete (Fin n)
.
Instances For
If F
preserves the initial object and binary coproducts then it preserves finite products.