preservesCoproduct_of_preservesBiproduct

English

If a functor preserves biproducts, it preserves coproducts.

Русский

Если функтор сохраняет биопродукты, он сохраняет coproducts.

LaTeX

$$$\mathrm{PreservesBiproduct}\ f F \Rightarrow \mathrm{PreservesCoproduct}\ f F$$$

Lean4

/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite coproducts. -/
theorem preservesCoproduct_of_preservesBiproduct {f : J → C} [PreservesBiproduct f F] :
    PreservesColimit (Discrete.functor f) F where
  preserves {c}
    hc :=
    let ⟨_⟩ := nonempty_fintype J
    ⟨IsColimit.ofIsoColimit
          ((IsColimit.precomposeHomEquiv (Discrete.compNatIsoDiscrete _ _) _).symm
            (isBilimitOfPreserves F (biconeIsBilimitOfColimitCoconeOfIsColimit hc)).isColimit) <|
        Cocones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

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