extending complexes

Stream: condensed mathematics

[Johan Commelin]

We can now extend ℕ-indexed complexes to ℤ-indexed complexes: https://github.com/leanprover-community/lean-liquid/blob/master/src/for_mathlib/complex_extend.lean

[Johan Commelin]

This also allows to embed cochain complexes indexed by ℕ into chain complexes indexed by ℤ, by flipping the directions. (And vice versa)

[Johan Commelin]

Next target: if an ℕ-complex is_projective_resolution then you get is_K_projective after pushing it through this functor, etc...

[Adam Topaz]

I think @Andrew Yang has already done that?

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/829d2657ad15f020af7fd1df73f93e214c084a42/src/for_mathlib/projective_replacement.lean#L709

[Matthew Ballard]

This sounds very related to implementing brutal/stupid truncations

[Johan Commelin]

We can now get those by restricting and then extending.

[Johan Commelin]

Adam Topaz said:

https://github.com/leanprover-community/lean-liquid/blob/829d2657ad15f020af7fd1df73f93e214c084a42/src/for_mathlib/projective_replacement.lean#L709

Cool, that will make the proof really short (-;

[Adam Topaz]

I thought Andrew also worked on extending from $\mathbb{N}$ to $\mathbb{Z}$, but maybe I misremembered because I can't seem to find it.

[Adam Topaz]

Johan Commelin said:

We can now get those by restricting and then extending.

If you want to truncate somewhere other than $0$, then you would need to shift, restrict, extend and unshift, which would be really annoying for defeq reasons.

[Matthew Ballard]

In general, is there pleasant API for working with isomorphisms between $[m,\infty) \cap \mathbb{Z}$ as $\mathbb{N}$-modules?

[Johan Commelin]

I don't think so