English
If a functor preserves finite products and biproducts, the preadditive structure is determined uniquely.
Русский
Если функтор сохраняет конечные произведения и биопродукты, предадитивная структура определяется однозначно.
LaTeX
$$$\text{PreservesProductOfShape} \Rightarrow \text{PreservesBiproductOfShape}$$$
Lean4
/-- If the (product-like) biproduct comparison for `F` and `f` is a monomorphism, then `F`
preserves the biproduct of `f`. For the converse, see `mapBiproduct`. -/
theorem preservesBiproduct_of_mono_biproductComparison {f : J → C} [HasBiproduct f] [HasBiproduct (F.obj ∘ f)]
[Mono (biproductComparison F f)] : PreservesBiproduct f F :=
by
haveI : HasProduct fun b => F.obj (f b) := by
change HasProduct (F.obj ∘ f)
infer_instance
have that :
piComparison F f =
(F.mapIso (biproduct.isoProduct f)).inv ≫ biproductComparison F f ≫ (biproduct.isoProduct _).hom :=
by
ext j
convert piComparison_comp_π F f j; simp [← Function.comp_def, ← Functor.map_comp]
haveI : IsIso (biproductComparison F f) := isIso_of_mono_of_isSplitEpi _
haveI : IsIso (piComparison F f) := by
rw [that]
infer_instance
haveI := PreservesProduct.of_iso_comparison F f
apply preservesBiproduct_of_preservesProduct
