preservesBinaryCoproducts_of_preservesInitial_and_pushouts

English

A functor that preserves initial objects and pushouts preserves binary coproducts.

Русский

Функтор, сохраняющий начальный объект и пушауты, сохраняет бинарные копродукты.

LaTeX

$$$\\forall F:\\,C\\to D,\\ HasInitial C\\,\\land\\ HasPushouts C\\Rightarrow\\ PreservesCollimitsOfShape (Discrete WalkingPair) F\\Rightarrow PreservesCollimitsOfShape (Discrete WalkingPair) F$$$

Lean4

/-- A functor that preserves initial objects and pushouts preserves binary coproducts. -/
theorem preservesBinaryCoproducts_of_preservesInitial_and_pushouts [HasInitial C] [HasPushouts C]
    [PreservesColimitsOfShape (Discrete.{0} PEmpty) F] [PreservesColimitsOfShape WalkingSpan F] :
    PreservesColimitsOfShape (Discrete WalkingPair) F :=
  ⟨fun {K} =>
    preservesColimit_of_preserves_colimit_cocone (colimitCoconeOfInitialAndPushouts K).2
      (by
        apply isBinaryCoproductOfIsInitialIsPushout _ _ (isColimitOfHasInitialOfPreservesColimit F)
        apply isColimitOfHasPushoutOfPreservesColimit)⟩

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