preservesBiproduct_of_preservesCoproduct

English

If a functor preserves products for shape J, it preserves biproducts for shape J.

Русский

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

LaTeX

$$$[PreservesLimitsOfShape (Discrete J) F] \Rightarrow [PreservesBiproductsOfShape J F]$$$

Lean4

/-- A functor between preadditive categories that preserves (zero morphisms and) finite coproducts
preserves finite biproducts. -/
theorem preservesBiproduct_of_preservesCoproduct {f : J → C} [PreservesColimit (Discrete.functor f) F] :
    PreservesBiproduct f F where
  preserves {b}
    hb :=
    let ⟨_⟩ := nonempty_fintype J
    ⟨isBilimitOfIsColimit _ <|
        IsColimit.ofIsoColimit
            ((IsColimit.precomposeInvEquiv (Discrete.compNatIsoDiscrete _ _) (F.mapCocone b.toCocone)).symm
              (isColimitOfPreserves F hb.isColimit)) <|
          Cocones.ext (Iso.refl _) (by rintro ⟨⟩; simp)⟩

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