Zulip Chat Archive

Yes, it's just a type with a successor function. The reason we used that is that if we have a sequence X of types over the natural numbers or the integers, then the maps can go from X n -> X (n+1) or from X n -> X (n-1).

Floris van Doorn (May 24 2019 at 18:04):

(there are other options, for example maps X (n-1) -> X n or X (n+1) -> X n, which are equivalent (but not definitionally equal to) when indexing over the integers and "almost equivalent" when indexing over the natural numbers. We didn't feel a need to use these in Lean 2)

Floris van Doorn (May 24 2019 at 18:07):

We also used other indexing types. For example for the long exact sequence of homotopy groups, we indexed over nat \times fin 3. The reason is that if you index over nat then X(3n)=\pi_n(B) and X(3n+1)=\pi_n(E) and X(3n+2)=\pi_n(F)(if you start with a map E -> B with fiber F). However, there is no way to get these equalities definitionally, which would be a huge pain. You can get them definitionally if you index over N x 3 (where (n,i) of course represents 3n+i).

Johan Commelin (May 24 2019 at 18:11):

This seems like a pretty good approach! Once the monoidal cats land, we should build additive/abelian cats and port this stuff over from Lean 2.

Reid Barton (May 24 2019 at 18:12):

Yes, it looks very useful. And sometimes you encounter Z/2-graded chain complexes or even just ungraded ones ( $d : A \to A$ with $d^2 = 0$ )

Reid Barton (May 24 2019 at 18:13):

I wondered if there might be some extra axiom like two elements with the same successor are equal... since I can't think of a reasonable situation where that would fail

Floris van Doorn (May 24 2019 at 18:15):

You can also read the comment at the top of this file with some explanation: https://github.com/leanprover/lean2/blob/master/hott/homotopy/LES_of_homotopy_groups.hlean

One disadvantage is that these sequences are a bit hard to work with. For example, all the constructions with long exact sequences are with pointed sets, but then at the bottom of the LES-file we need to convince Lean that most of these pointed sets are actually groups (and most of those are abelian). This turned out to be a bit awkward.

Floris van Doorn (May 24 2019 at 18:16):

Also, it is not quite general to capture short exact sequences (where some elements don't have a successor).
And as Reid mentions: it is interesting that we never have to use that the successor is injective (at least if we formulate all results in the right way)

Floris van Doorn (May 24 2019 at 18:22):

In Agda they used a different approach, which is definitely worth considering.
Instead of a single long exact sequence

... ->
\pi_{n+2}(F) -> \pi_{n+2}(E) -> \pi_{n+2}(B) ->
\pi_{n+1}(F) -> \pi_{n+1}(E) -> \pi_{n+1}(B) ->
\pi_n(F) -> \pi_n(E) -> \pi_n(B) ->
...

you consider a sequence of short exact sequences

\pi_{n+2}(B) -> \pi_{n+1}(F) -> \pi_{n+1}(E) -> \pi_{n+1}(B) -> \pi_n(F)

one for each n.

This captures the same information and has the advantage that you only have to consider short exact sequences, not SESs and LESs separately. (And all my attempts to find a common generalization of LESs and SESs seems like it is more work than doing them separately.)

Johan Commelin (May 24 2019 at 18:24):

Won't we want the category of complexes anyway? As soon as we start doing homological algebra, derived categories, etc...

Johan Commelin (May 24 2019 at 18:25):

So you would at least need a very good interface to "long" sequences.

Floris van Doorn (May 24 2019 at 18:26):

Oh, that's a good point. Once we start to talk about the category of LESs, then we would indeed want them as a single type.

Last updated: Dec 20 2023 at 11:08 UTC