-
Notifications
You must be signed in to change notification settings - Fork 298
homological algebra #1063
Comments
Definitely worth checking out https://github.com/cmu-phil/Spectral which goes all the way through spectral sequences, though only for modules over a ring. |
Yes, it it worth checking out what was done in the Lean 2 HoTT library (also e.g. https://github.com/leanprover/lean2/blob/master/hott/homotopy/chain_complex.hlean). What I would do the same:
Things I would do differently:
Comments:
and
The approach in Lean 2 HoTT was to always use maps |
@semorrison @TwoFX I guess we have homology and exactness now, right? |
The definitions are there, yes, though I would say that the API for both is not yet in a shape where you can actually work with them. |
We'd like to have the basics of homological algebra (complexes, chain maps, homotopy equivalences, exact sequences, homology).
There will be some overlap with the theory of simplicial objects: this issue only addresses the pedestrian approach.
I think it is valuable to work quite generally, and use enriched categories (one doesn't want to have to separately prove that if your morphisms form abelian groups, your chain maps form abelian groups, and that if your morphisms form vector spaces, your chains maps form vector spaces). However if enriched categories aren't ready yet, it's reasonable to start on the special cases.
The text was updated successfully, but these errors were encountered: