preservesBinaryBiproduct_of_preservesBiproduct

English

A functor that preserves a biproduct of a pair yields a preserved binary biproduct.

Русский

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

LaTeX

$$$\text{PreservesBinaryBiproduct} X Y F$ given $\text{PreservesBiproduct}(\text{pairFunction } X Y) F$$$

Lean4

/-- A functor that preserves biproducts of a pair preserves binary biproducts. -/
theorem preservesBinaryBiproduct_of_preservesBiproduct (F : C ⥤ D) [PreservesZeroMorphisms F] (X Y : C)
    [PreservesBiproduct (pairFunction X Y) F] : PreservesBinaryBiproduct X Y F where
  preserves {b}
    hb :=
    ⟨{  isLimit :=
          IsLimit.ofIsoLimit
              ((IsLimit.postcomposeHomEquiv (diagramIsoPair _) _).symm
                (isBilimitOfPreserves F (b.toBiconeIsBilimit.symm hb)).isLimit) <|
            Cones.ext (Iso.refl _) fun j => by rcases j with ⟨⟨⟩⟩ <;> simp
        isColimit :=
          IsColimit.ofIsoColimit
              ((IsColimit.precomposeInvEquiv (diagramIsoPair _) _).symm
                (isBilimitOfPreserves F (b.toBiconeIsBilimit.symm hb)).isColimit) <|
            Cocones.ext (Iso.refl _) fun j => by rcases j with ⟨⟨⟩⟩ <;> simp }⟩

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