English
If F preserves a mono biprodComparison between X and Y (under HasBinaryBiproducts), then F preserves binary biproducts of X and Y.
Русский
Если biprodComparison F X Y является моно-морфизмом, тогда F сохраняет бинарный би-производный X Y.
LaTeX
$$$$\\text{If }\\mathrm{biprodComparison}(F,X,Y) \\text{ is mono, then }\\PreservesBinaryBiproduct X Y F.$$$$
Lean4
/-- If the (product-like) biproduct comparison for `F`, `X` and `Y` is a monomorphism, then
`F` preserves the biproduct of `X` and `Y`. For the converse, see `map_biprod`. -/
theorem preservesBinaryBiproduct_of_mono_biprodComparison {X Y : C} [HasBinaryBiproduct X Y]
[HasBinaryBiproduct (F.obj X) (F.obj Y)] [Mono (biprodComparison F X Y)] : PreservesBinaryBiproduct X Y F :=
by
have that :
prodComparison F X Y = (F.mapIso (biprod.isoProd X Y)).inv ≫ biprodComparison F X Y ≫ (biprod.isoProd _ _).hom := by
ext <;> simp [← Functor.map_comp]
haveI : IsIso (biprodComparison F X Y) := isIso_of_mono_of_isSplitEpi _
haveI : IsIso (prodComparison F X Y) := by
rw [that]
infer_instance
haveI := PreservesLimitPair.of_iso_prod_comparison F X Y
apply preservesBinaryBiproduct_of_preservesBinaryProduct
