Fiber sequences of short exact sequences induced by pullback

[jarlg]

We prove that a short exact sequence B -> E -> C of abelian groups induces a fiber sequence AbSES C A -> AbSES E A -> AbSES B A by pulling back (isexact_abses_pullback). Our strategy is to prove the analog of exactness on path data and deduce actual exactness from that. The reason being that path data consists of functions which compute, and this makes the "path algebra" manageable. (Recall that path data between two short exact sequences are morphisms between their middles respecting the inclusions and projections.)

We also show that loops (AbSES B A) is the set of group homomorphisms B -> A (loops_abses). Thus the long exact sequence of homotopy groups associated to the fiber sequence above recovers the usual six-term exact sequence of Ext groups — though we have not yet formalised the details of this.

I've separated the commits into logical chunks, with the 3rd, second to last, and last commits being the most interesting ones. There are mostly additions so the "unified" view ought to be fine for reviewing.

There is one kink I hope we can work out: the Defined. on line 248 of Algebra/AbGroups/AbSES/PullbackFiberSequence.v takes about 24s on my laptop. Any suggestions for how to speed it up? (If no good suggestions come up, I might try redefining hfiber_cxfib' and friends as records. But I'm hoping there's some smaller tweak that can be done.)

[jdchristensen]

Wow, thanks for this huge contribution! I skimmed it over, and think it looks good.

I made a few minor comments. And I couldn't quickly see how to speed up the slow parts, but I might take another look later.

[Alizter]

@jarlg If you rebase the CI should (mostly) work.

[jarlg]

I defined base point preserving functors and pointed transformations between them, which specialise to the pullback functors and their "path data homotopies" I had earlier. Like Dan suggsted above, to_pointed preserves composition in this generality.

[jdchristensen]

Nice! Not only is this cleaner, it makes several things faster. For example, the really slow Defined at the end of hfiber_cxfib'_inhabited in PullbackFiberSequence.v went from 11.7s to 1.5s on my machine. It still takes about 15s to build the six files in the AbSES directory, so there's room for improvement, but I don't think that should block merging.

[jarlg]

I managed to shave off a couple of seconds in AbSES/PullbackFiberSequence.v by splitting out two lemmas and marking abses_pullback' opaque for one of them. Not sure why line 179 (exact (@pr2_cxfib' _ A B C E U).) isn't instant since it's supplying a term of the right type, but it's pretty fast now.

[jdchristensen]

These two files should be listed in AbSES.v:

Algebra/AbGroups/AbSES/Ext.v
Algebra/AbGroups/AbSES/PullbackFiberSequence.v

I'm working on some speedups. Can I push them to your branch later today?

[jarlg]

Sure. Feel free to add those lines in AbSES.v and correct "transparent" to "opaque". Or I can fix those afterwards. Thanks!

[jdchristensen]

I addressed the two recent comments I made, and also sped things up a bit. I didn't see any easy ways to address the remaining slow parts. So I think this is ready to merge, once someone checks my two commits.

[jarlg]

Looks good to me. Thanks! I also removed two "todo"s I forgot to remove earlier.

[jarlg]

Does anyone else want to have a look at this? Commits 6 (c47d445) and 11 (0c103af) are the ones which touch on WildCats, if anyone just wants to comment on just those changes.

[Alizter]

Wildcat stuff is fine with me

[jarlg]

Alright, thanks @Alizter! I think this is ready to merge then.