Five lemma

[mzhang28]

I tried to define a more general notion of exact sequences for groups (as well as Fin-indexed, N-indexed, and Z-indexed), as well as use the definition to prove the five lemma.

I'm still very new to this, so I anticipate this might not be the best way to define them. Let me know if there are problems with the design of the data structures.

[felixwellen]

I have suggestions for improvement:
Maybe it is better to use something more abstract as indices for exact sequences. I remember Floris van Doorn wrote in his phd-thesis on the formalization of Serre's spectral sequence, that he ended up using an abstract "successor structure", also to allow the use of something like (Fin 3) x N as indices for a long exact cohomology sequence.
I think it would be better to use something like that (if possible), to avoid different notions of (exact) sequence.

[mzhang28]

ohhhh i see... that's a good idea. i think that would generalize the infinite ones, but for Fin n, it's still necessary to handle it slightly differently since you would need different sizes of indexes for the group sequence, homomorphism sequence, and the exact sequence. Maybe that could be generalized into some sort of "finite" successor structure.. i don't know. I'll play around with it and see what I can come up with

[mzhang28]

Ran into a problem... I was going to try unifying the new definition with Exact4, but I didn't notice until now that it was polymorphic over the universe levels of each of the individual groups! I'm thinking I could introduce yet another sequence, starting with a (levelSeq : N -> ℓ), then using having (groupSeq : (n : N) -> Group (levelSeq n)) and then having some kind of max-level over a sequence for the big type. I have not been successful with this approach yet.

For now, I implemented this with uniform level. I'm not going to touch the existing theorems yet, maybe possibly in a future revision.

Also, one other question I have is that I'm using this definition now:

isExactAt : {A B C : Group ℓ} (f : GroupHom A B) (g : GroupHom B C) → Type ℓ
isExactAt {B = B} f g = (b : ⟨ B ⟩) → isInKer g b ≃ isInIm f b

Based on my current understanding of exactness from literature, it seems that these should be an equivalence at the very least. But the existing lemma for Exact4 is just using invertible functions. Will the extra data pose any problems?