Zulip Chat Archive

Stream: condensed mathematics

Topic: extending complexes


Johan Commelin (Mar 11 2022 at 14:25):

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 (Mar 11 2022 at 14:25):

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

Johan Commelin (Mar 11 2022 at 14:27):

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

Adam Topaz (Mar 11 2022 at 14:32):

I think @Andrew Yang has already done that?

Adam Topaz (Mar 11 2022 at 14:33):

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

Matthew Ballard (Mar 11 2022 at 14:36):

This sounds very related to implementing brutal/stupid truncations

Johan Commelin (Mar 11 2022 at 14:39):

We can now get those by restricting and then extending.

Johan Commelin (Mar 11 2022 at 14:40):

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 (Mar 11 2022 at 14:41):

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

Adam Topaz (Mar 11 2022 at 14:42):

Johan Commelin said:

We can now get those by restricting and then extending.

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

Matthew Ballard (Mar 11 2022 at 14:53):

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

Johan Commelin (Mar 11 2022 at 14:56):

I don't think so


Last updated: Dec 20 2023 at 11:08 UTC