Zulip Chat Archive

Stream: Is there code for X?

Topic: additive functors preserve binary biproducts

Johan Commelin (May 02 2022 at 13:46):

Does mathlib not yet have this?

instance category_theory.limits.preserves_binary_biproduct_of_additive
  {𝓐 𝓑 : Type*} [category 𝓐] [category 𝓑] [abelian 𝓐] [abelian 𝓑]
  (F : 𝓐 ⥤ 𝓑) [functor.additive F] (X Y : 𝓐) :
  preserves_binary_biproduct X Y F :=
sorry

We need this for LTE.

Adam Topaz (May 02 2022 at 14:57):

https://github.com/leanprover-community/mathlib/blob/61d5d308c6b2268799d2e4377a6232b34aced678/src/category_theory/preadditive/additive_functor.lean#L108

Adam Topaz (May 02 2022 at 14:58):

And https://github.com/leanprover-community/mathlib/blob/61d5d308c6b2268799d2e4377a6232b34aced678/src/category_theory/limits/preserves/shapes/biproducts.lean#L121

Johan Commelin (May 02 2022 at 15:05):

Thanks! So I'm just missing imports.

Johan Commelin (May 02 2022 at 15:11):

Wait, neither of those is about binary biproducts.

Johan Commelin (May 02 2022 at 15:11):

So there's still glue missing.

Adam Topaz (May 02 2022 at 15:11):

Oh?

Adam Topaz (May 02 2022 at 15:12):

There we go:
https://github.com/leanprover-community/mathlib/blob/61d5d308c6b2268799d2e4377a6232b34aced678/src/category_theory/limits/preserves/shapes/biproducts.lean#L143

Last updated: Dec 20 2023 at 11:08 UTC