Products in the over category #
Shows that products in the over category can be derived from wide pullbacks in the base category.
The main result is over_product_of_widePullback
, which says that if C
has J
-indexed wide
pullbacks, then Over B
has J
-indexed products.
Note that the binary case is done separately to ensure defeqs with the pullback in the base category.
TODO #
- Generalise from arbitrary products to arbitrary limits. This is done in Toric.
- Dualise to get the
Under X
results.
Binary products #
In this section we construct binary products in Over X
and binary coproducts in Under X
explicitly as the pullbacks and pushouts of binary (co)fans in the base category.
For Over X
, one could construct these binary products from the general theory of arbitrary
products from the next section, ie
(Cones.postcomposeEquivalence (diagramIsoCospan _).symm).trans
(Over.ConstructProducts.conesEquiv _ (pair (Over.mk f) (Over.mk g)))
but this gives worse defeqs.
For Under X
, there is currently no general theory of arbitrary coproducts.
Pullback cones to X
are the same thing as binary fans in Over X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A binary fan in Over X
is a limit if its corresponding pullback cone to X
is a limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A pullback cone to X
is a limit if its corresponding binary fan in Over X
is a limit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Pushout cocones from X
are the same thing as binary cofans in Under X
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A binary cofan in Under X
is a colimit if its corresponding pushout cocone from X
is a
colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A pushout cocone from X
is a colimit if its corresponding binary cofan in Under X
is a
colimit.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The product of Y
and Z
in Over X
is isomorpic to Y ×ₓ Z
.
Equations
- Y.prodLeftIsoPullback Z = ⋯.isoPullback
Instances For
Arbitrary products #
In this section, we prove that J
-indexed products in Over X
correspond to J
-indexed pullbacks
in C
.
(Implementation)
Given a product diagram in C/B
, construct the corresponding wide pullback diagram
in C
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Impl) A preliminary definition to avoid timeouts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Impl) A preliminary definition to avoid timeouts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Impl) A preliminary definition to avoid timeouts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Impl) A preliminary definition to avoid timeouts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Impl) A preliminary definition to avoid timeouts.
Equations
- One or more equations did not get rendered due to their size.
Instances For
(Impl) Establish an equivalence between the category of cones for F
and for the "grown" F
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Use the above equivalence to prove we have a limit.
Given a wide pullback in C
, construct a product in C/B
.
Given a pullback in C
, construct a binary product in C/B
.
Given all wide pullbacks in C
, construct products in C/B
.
Given all finite wide pullbacks in C
, construct finite products in C/B
.
Construct terminal object in the over category. This isn't an instance as it's not typically the
way we want to define terminal objects.
(For instance, this gives a terminal object which is different from the generic one given by
over_product_of_widePullback
above.)