additive_of_preservesBinaryBiproducts

English

Let Z be an object property of C. Then the inclusion Z.ι.Additive holds as before.

Русский

Пусть Z — свойство объектов C. Тогда включение Z.ι аддитивно, как и ранее.

LaTeX

$$$ Z.ι.Additive $$$

Lean4

theorem additive_of_preservesBinaryBiproducts [HasBinaryBiproducts C] [PreservesZeroMorphisms F]
    [PreservesBinaryBiproducts F] : Additive F where
  map_add
    {X Y f
      g} := by
    rw [biprod.add_eq_lift_id_desc, F.map_comp, ← biprod.lift_mapBiprod, ← biprod.mapBiprod_hom_desc, Category.assoc,
      Iso.inv_hom_id_assoc, F.map_id, biprod.add_eq_lift_id_desc]

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