preservesBinaryBiproduct_of_epi_biprodComparison'

English

If the epi condition holds for the coproduct-like biproduct comparison, then F preserves the biproduct of X and Y.

Русский

Если сопоставление копроизведения аналогично би-производному является эпиморфизмом, тогда F сохраняет би-производный X и Y.

LaTeX

$$$$\\text{If }\\mathrm{biprodComparison'} F X Y \\text{ is epi, then }\\PreservesBinaryBiproduct X Y F.$$$$

Lean4

/-- If the (coproduct-like) biproduct comparison for `F`, `X` and `Y` is an epimorphism, then
`F` preserves the biproduct of `X` and `Y`. For the converse, see `mapBiprod`. -/
theorem preservesBinaryBiproduct_of_epi_biprodComparison' {X Y : C} [HasBinaryBiproduct X Y]
    [HasBinaryBiproduct (F.obj X) (F.obj Y)] [Epi (biprodComparison' F X Y)] : PreservesBinaryBiproduct X Y F :=
  by
  haveI : Epi (splitEpiBiprodComparison F X Y).section_ := by simpa
  haveI : IsIso (biprodComparison F X Y) := IsIso.of_epi_section' (splitEpiBiprodComparison F X Y)
  apply preservesBinaryBiproduct_of_mono_biprodComparison

Похожие утверждения