Zulip Chat Archive

Stream: condensed mathematics

I think we need to sit down and formalize https://stacks.math.columbia.edu/tag/014D and https://stacks.math.columbia.edu/tag/014P.
I've created https://github.com/leanprover-community/lean-liquid/issues/74 to track this todo.
As a corollary, we can then redefine derived functors, so that they can be applied to objects in the homotopy category, instead of merely single objects in degree 0.

Note that the mapping cone is done in src/for_mathlib/mapping_cone.lean

As a first step towards getting triangles for homological complexes, I have attempted to refactor shifts.

make shifts more flexible #10573

There is still one pretty annoying sorry left. In general, getting a framework for shifts that works smoothly seems to be quite a challenge.

All ideas are very welcome!

The sorry is gone. I think I've identified a simp-normal-form for "canonical" maps between shifted objects.

So the proof is now straight-forward, even if a bit tedious.

@Andrew Yang helped me out by fixing the rest of the PR. Thanks a lot for that!

@Adam Topaz If you have some time to review #10573, that would be great.

I left a few comments.

Last updated: Dec 20 2023 at 11:08 UTC