bounding mapping cone

Stream: condensed mathematics

[Johan Commelin]

Did someone already define the mapping cone as bounded complex? And the corresponding triangle?

[Adam Topaz]

It must be there since that's how the pretriangulated structure on the bounded homotopy category is defined.

[Adam Topaz]

There is cone.triangle

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/cf8e493f4883c2b7c6ef4297d8b4b0a3d0cb5d92/src/for_mathlib/mapping_cone.lean#L98

[Adam Topaz]

Looks like I proved boundedness by hand here
https://github.com/leanprover-community/lean-liquid/blob/cf8e493f4883c2b7c6ef4297d8b4b0a3d0cb5d92/src/for_mathlib/derived/bounded_homotopy_category.lean#L162
That should probably be pullled out into a separate lemma

[Adam Topaz]

The key is is_zero_biprod

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/cf8e493f4883c2b7c6ef4297d8b4b0a3d0cb5d92/src/for_mathlib/abelian_category.lean#L178

[Johan Commelin]

Ok, thanks for the pointers

[Johan Commelin]

Aahrg bounded_homotopy_category.lean is giving me timeouts in VSCode. So I guess I'll wait till I'm back in the office tomorrow, where I have a proper machine.