English
Let F be as above and f : J → C with HasBiproduct f and PreservesBiproduct f F. Then HasBiproduct of the diagram i ↦ F.obj (f i) exists, with the same construction using F.mapBicone and F-preservation of bilimits.
Русский
Пусть F удовлетворяет условиям и f : J → C имеет би-произведение, причём F сохраняет би-произведение f. Тогда существует би-произведение диаграммы i ↦ F.obj (f i) в D, задаваемое образами би-производства через F.
LaTeX
$$$\\operatorname{HasBiproduct}(F\\circ f)\\;\\text{(as for a family } f: J\\to C\\text{)}$$$
Lean4
/-- This instance applies more often than `hasBiproduct_of_preserves`, but the discrimination
tree key matches a lot more (since it does not look through lambdas). -/
instance (priority := low) hasBiproduct_of_preserves' : HasBiproduct fun i => F.obj (f i) :=
HasBiproduct.mk
{ bicone := F.mapBicone (biproduct.bicone f)
isBilimit := isBilimitOfPreserves _ (biproduct.isBilimit _) }
