Open semorrison opened 5 years ago
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:
nat
and those over int
(or something like int x int
)nat x 3
or int x 3
instead of nat
or int
. (see the same Zulip discussion for reasons)Things I would do differently:
succ_str
a typeclassComments:
nat
going upwards and those going downwards. That is, sequences
... -> X n -> X (n+1) -> X (n+2) -> ...
and
... -> X (n+2) -> X (n+1) -> X n -> ...
The approach in Lean 2 HoTT was to always use maps X n -> X (S n)
where S
was any endofunction (like succ
or pred
), encapsulated in a "successor structure". This gives you mostly what you want, except in the case where you use pred
over nat
, because then you have a superfluous function X 0 -> X (pred 0)
, i.e. X 0 -> X 0
.
@semorrison @TwoFX I guess we have homology and exactness now, right?
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.