preservesBinaryBiproduct_of_preservesBinaryProduct

English

If F preserves the limit of the pair diagram, then F preserves binary biproducts; i.e. preservation of the binary product structure follows from preservation of the limit of the pair diagram.

Русский

Если F сохраняет предел пары диаграмм, то F сохраняет бинарные би-производные; т.е. сохранение структуры би-производного следует из сохранения предела пары.

LaTeX

$$$$\\forall X,Y,\\; \\PreservesLimit(\\mathrm{pair}(X,Y),F) \\Rightarrow \\PreservesBinaryBiproduct X Y F.$$$$

Lean4

/-- A functor between preadditive categories that preserves (zero morphisms and) binary products
preserves binary biproducts. -/
theorem preservesBinaryBiproduct_of_preservesBinaryProduct {X Y : C} [PreservesLimit (pair X Y) F] :
    PreservesBinaryBiproduct X Y F where
  preserves {b}
    hb :=
    ⟨isBinaryBilimitOfIsLimit _ <|
        IsLimit.ofIsoLimit
            ((IsLimit.postcomposeHomEquiv (diagramIsoPair _) (F.mapCone b.toCone)).symm
              (isLimitOfPreserves F hb.isLimit)) <|
          Cones.ext (by dsimp; rfl) fun j => by rcases j with ⟨⟨⟩⟩ <;> simp⟩

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