preservesBinaryCoproduct_of_preservesBinaryBiproduct

English

A functor that preserves binary biproducts preserves binary coproducts; i.e., preserves colimits of walking pair shape.

Русский

Функтор, сохраняющий бинарные би-производные, сохраняет бинарные копроизведения; т.е. колимиты формы WalkingPair сохраняются.

LaTeX

$$$$\\PreservesBinaryBiproducts F \\Rightarrow \\PreservesColimit(\\mathrm{pair},F).$$$$

Lean4

/-- A functor between preadditive categories that preserves (zero morphisms and) binary biproducts
preserves binary coproducts. -/
theorem preservesBinaryCoproduct_of_preservesBinaryBiproduct {X Y : C} [PreservesBinaryBiproduct X Y F] :
    PreservesColimit (pair X Y) F where
  preserves {c}
    hc :=
    ⟨IsColimit.ofIsoColimit
          ((IsColimit.precomposeHomEquiv (diagramIsoPair _) _).symm
            (isBinaryBilimitOfPreserves F (binaryBiconeIsBilimitOfColimitCoconeOfIsColimit hc)).isColimit) <|
        Cocones.ext (by dsimp; rfl) fun j => by rcases j with ⟨⟨⟩⟩ <;> simp⟩

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