Classify short exact sequences by maps of Eilenberg-Mac Lane spaces by CharlesCNorton · Pull Request #2369 · HoTT/Coq-HoTT

CharlesCNorton · 2026-06-11T11:36:37Z

Short exact sequences of abelian groups are classified by pointed maps of Eilenberg-Mac Lane spaces:

AbSES B A  <~>  (K(B,2) ->* K(A,3))

This is Theorem 2.2.2 of Christensen and Flaten, "Ext groups in homotopy type theory". It follows that AbSES B A and Ext B A are essentially small.

New file

Algebra/AbSES/Classification.v: the classifying map of a short exact sequence (the connecting map of K(-,3) applied to it), its inverse built from the fibre of a pointed map, the two round trips, the resulting equivalence, smallness of AbSES and Ext, and naturality of the classifying map in both variables.

Supporting changes

Homotopy/EMSpace.v: functoriality of K(-,n) (em_fmap), with its identity, composition, connectivity and equivalence lemmas; the delooping equivalence on mapping types; and that every (n-1)-connected n-type is K(Pi n, n).
Homotopy/ExactSequence.v: naturality and rotation of the connecting map.
Homotopy/ClassifyingSpace.v, Pointed/pFiber.v, Truncations/Connectedness.v: supporting lemmas.

jdchristensen · 2026-06-11T13:27:17Z

It's great to see this! I'll wait until you ping me before looking at the details, but feel free to ask me any questions. I've marked this as a draft for now, since you said that there is still more to come.

I took a quick look a ClassifyingSpace.v, but nothing else yet.

The component-level half is done and pushed; the global equivalence is in progress and will be pushed to this PR.

I'm not sure what you mean by "component-level half" and "global equivalence".

CharlesCNorton · 2026-06-17T20:39:51Z

Sorry, I guess I don't get notified when something is marked as ready for review unless you specifically tag me as a reviewer, so I was still waiting to hear that it was ready.

Thanks for doing this. I'm very excited to see it!

However, I do wish you had consulted with @jarlg and me before starting. For one, it seems like you didn't build on https://github.com/jarlg/Yoneda-Ext, which already defines the higher ext groups and proves one of the long exact sequences. That repo is cited in the paper you were working from, so it's odd that you didn't use it. Note that it was likely also in the training data the LLM used.

The reason that we haven't merged that repo into the main library is that most of the material doesn't need to be done for abelian groups. It could be done for R-modules, or even for any abelian category, but the current formalization assumes we are working the category of abelian groups, just for simplicity. So our plan was to first build up the necessary material on abelian wild categories, and then do the formalization in that framework.

In fact, we can likely work in a setting much weaker than an abelian category, and @ThomatoTomato and I are currently exploring this space. For example, see the files AbEnriched.v, EpiStable.v and HomologicalAlgebra.v in the WildCat folder. One of the nice things about this set-up is that it allows proofs by diagram chasing, so traditional element-wise proofs in textbooks can be directly formalized.

Maybe the right way to proceed is to first decide on the kind of wild category that is needed for this work, do the (small?) amount of formalization needed to work in that setting, and then start gradually porting this work to that framework?

Also, it would be best to do at most a few hundred lines of code at a time, so it can be reviewed and feedback can be provided, rather than creating a PR with 6000 lines of new code.

rescoping now.

CharlesCNorton · 2026-06-17T22:19:19Z

@jdchristensen - I've removed the higher Ext development (§2.4–2.7); this PR is now just the §2.2 classification by Eilenberg-Mac Lane spaces. Is that worth landing on its own or would you still like for me to break it up? We're at ~2000 lines

CharlesCNorton · 2026-06-17T22:34:39Z

Forgot to remove LoopGroup.v - now removed. 👍

jdchristensen · 2026-06-17T23:16:04Z

+  #[export] Instance isequiv_em_fmap (G G' : AbGroup) (n : nat)
+    : IsEquiv (fun f : GroupHomomorphism G G' => em_fmap f n.+1).


A slightly more general fact is that for each n, fmap (Pi n.+1) is an equivalence (X ->* Y) -> (Pi n.+1 X $-> Pi n.+1 Y) when X is n-connected and Y is (n+1)-truncated. Specializing to EM spaces implies this result, since em_fmap is an inverse to fmap (Pi n.+1). And I wonder if this slightly more general fact might be just as easy to prove?

It appears that generalizing this needs the universal property of the n-connected cover — to classify maps from K(A, n.+1) into a general (n+1)-truncated target by Pi n.+1. Cover.v has the cover but not that factoring equivalence, so I have kept the direct proof.

jdchristensen · 2026-06-17T23:18:28Z

+      refine (pmap_postwhisker _
+        (pmap_prewhisker _ (fmap2 loops (ptr_natural _ _))) @* _).
+      refine (pmap_postwhisker _
+        (pmap_prewhisker _ (fmap_comp loops _ _)) @* _).
+      refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _) @* _).
+      refine (pmap_postwhisker _
+        (pmap_postwhisker _ (loop_susp_unit_natural _)^*) @* _).
+      refine (pmap_postwhisker _ (pmap_compose_assoc _ _ _)^* @* _).
+      refine (pmap_postwhisker _
+        (pmap_prewhisker _ (loops_em_em_ptr_unit G' n)^*) @* _).
+      refine ((pmap_compose_assoc _ _ _)^* @* _).
+      refine (pmap_prewhisker _ (peissect _) @* _).


I think the lhs', lhs_V', rhs', and rhs_V' tactics would probably work here and make things slightly more readable. They let you avoid ^* and trailing underscores (when combined with napply or rapply).

(These tactics are also good for wild-categories, see, e.g., HomologicalAlgebra.v, and more generally for any symmetric, transitive relation.)

jdchristensen · 2026-06-17T23:20:41Z

+  (** By Freudenthal, the loop-suspension unit of [K(B,2)] is 2-connected,
+      so [Pi 3] of the unit is surjective; since [Pi 3 K(B,2)] is trivial,
+      [psusp K(B,2)] has trivial [Pi 4]. *)
+  Local Instance contr_pi4_psusp_em : Contr (Pi 4 (psusp K(B, 2))).


Does it make anything more complicated to generalize 2 to n?

jdchristensen · 2026-06-18T01:00:06Z

@jdchristensen - I've removed the higher Ext development (§2.4–2.7); this PR is now just the §2.2 classification by Eilenberg-Mac Lane spaces. Is that worth landing on its own or would you still like for me to break it up? We're at ~2000 lines

This is a pretty good thing to target, since it's a part of that material that is specifically about abelian groups. (One can then deduce smallness for Ext of R-modules, but not for a general abelian category.)

I think it's still too big, but I think it might be reasonable to review everything in this PR except for the large, new file Classification.v. That file is ~1100 lines, and the other changes are ~700 lines. Since it's easy to ignore one file, and that file provides context, I think it's ok to leave the PR as it is for now. After review, we could merge the 700 lines, and then start a separate PR for the big file. At that point I might ask you to break up the big file, but let's leave that until we get there.

So far I just skimmed through a few parts and made some comments about various things. A careful review is going to take a while, and hopefully I'll get some help from others: @jarlg @Alizter @ThomatoTomato .

Alizter · 2026-06-19T06:56:01Z


  Section ClassifyingSpace.

+    Local Set Polymorphic Inductive Cumulativity.


Can you annotate the universes for the HIT so that its clear the behaviour you gain by setting this. I'm having some trouble working out why its necessary.

I'm not sure it changes the universes for the HIT. The point is supposed to be that it makes WildCat machinery work when groups are in different universes. I think there should be a comment at this spot in the file explaining this more precisely. (Or maybe pointing to another spot, where there is a comment saying "This line is an example of a place that uses that ClassifyingSpace is a cumulative inductive.")

Alizter · 2026-06-19T08:13:50Z

This file is very slow!

Is the slowness related to this PR? If not, this could be raised in a separate issue. But even so, it would be good to give timing info showing everything that is changed by this PR. I'll post a top-level comment with some instructions.

Alizter · 2026-06-19T09:45:13Z

I have a feeling (and only a feeling) that the proofs in pFiber.v can be simplified in a way that will make them easier to reason about in later lemmas. I didn't have enough time to do this, but I suspect if we explicitly lay out the equivalence in some steps, it might help with reasoning about the homotopies in the naturality lemmas.

I've ran out of time to have a look, but its really encouraging to see such progress in the library. I hope I can find some more time in the future to have a closer look.

Alizter · 2026-06-19T09:55:37Z

One more thing worth mentioning is that we really need to add some infra to the library to help LLMs navigate proofs. I have been using Claude to read and try some things out, but obviously there is still a gap between what I can do and what it is able to do.

The way I did this was make a simple python wrapper around rocq-lsp and told Claude to use that to inspect the proofs in the file. That seemed to give it a better understanding of how to use tactics, but the setup was very adhoc and fragile. rocq-lsp has very rich information such as per-line timings, which can indicate when a proof is "bad". It would be good to invest some time so that we have a sturdy setup and we can let some LLMs in loops try different things out quickly and efficiently, and generally codify some implicit knowledge we have in proof writing.

jdchristensen · 2026-06-19T14:41:50Z

The way I did this was make a simple python wrapper around rocq-lsp and told Claude to use that to inspect the proofs in the file.

Is this better than using https://github.com/LLM4Rocq/rocq-mcp ? I've only tried this a bit.

jdchristensen · 2026-06-19T14:51:45Z

@CharlesCNorton, it would be good to measure the timing of all the files that get rebuilt by this PR. I have included a dump of various methods of timing below, and probably the most relevant part for you is the part about make-pretty-timed-only-diff-tip.sh. Could you try that and post the output here? (Usually, only the top part of the sorted output needs to be posted.)

@Alizter , should I put this info somewhere on the repo website? It would be great if some part of this could be done by the CI, e.g. when triggered by an appropriate message here like happens for Rocq. (It would also be nice if most of this could be done using dune instead of make. E.g. dune's cache could make some of the set-up much faster.) [Edit: fixed incorrect tag of Ali.]

Timing:

It's important to have an idle machine, so stop other processes, including browsers.

Timing also is affected by thermal issues on some machines (particularly laptops).

One could consider using a ram disk, but I don't do so.

It may help to be on A/C power, depending on the machine.

Unless said otherwise, all of the commands should be run from the top-level repo dir, above the theories dir.

To get overall build time, can use:
```
dune clean; make clean > /dev/null 2>&1; sync; sleep 8
time nice -n -10 dune build --cache=disabled --display=quiet
```
It's important to use --display=quiet, as dune itself uses a non-trivial amount of cpu with its default display.
The nice -n -10 might require special privileges. Using a negative number gives extra priority to the job. Can just omit this if not available.

Or, if you want to use make to get overall time, use:

make clean > /dev/null 2>&1; sync; sleep 8
time nice -n -10 make -j8 > /dev/null

If you want several samples:

hyperfine --runs <N> -p 'dune clean; make clean > /dev/null 2>&1; sync; sleep 30' 'nice -n -10 dune build --cache=disabled --display=quiet'

The sleep helps with thermal issues on my machine.

It's often better to get per file timing, as it's easier to see changes that way. The coq-scripts repo can help with this. For some reason, it needs to be within the repo you are timing. I clone it into the top-level dir of the HoTT repo. See coq-scripts/timing/README.md for documentation.

Currently, most fine-grained timing tests have to be done using make instead of dune. See ocaml/dune#11587 for a feature request to add this support to dune.

If new changes already committed and nothing changed/staged, can use the following. Note that "tip" is a misnomer; it compares whatever is currently checked out (even in "detached head" state), to previous commit or PREV_COMMIT.
```
export PREV_COMMIT=<hash>   [defaults to previous commit]
export PREV_COMMIT=master   [etc.]
make -j<num_cores>
nice -n -10 ./coq-scripts/timing/make-pretty-timed-only-diff-tip.sh -j1  [or -jJ]
sort -r -k 12 time-of-build-both.log | less   [biggest changes first]
sort -r -k  1 time-of-build-both.log | less   [slowest files first]
```
With only-diff, it only compares changed files and their dependencies. If you instead use diff, it compares all files.

-j1 gives more precise timing, but takes longer. Again, this depends
partly on thermal issues.

If you are using -j1 and only-diff, run make -j8 first, since it starts by making sure the current tree is up-to-date, and there's no need to use -j1 for that step.

If new changes not committed, stage them, and do:

nice -n -10 ./coq-scripts/timing/make-pretty-timed-only-diff.sh -j1  [or -jJ]
sort -r -k 12 time-of-build-both.log | less

Same comments about only-diff and diff, -j1, etc.

To show the timing for the current working directory (no comparison), e.g. to search for slow files:
```
nice -n -10 ./coq-scripts/timing/make-pretty-timed.sh -j1  [or -jJ]
less time-of-build-pretty.log
```
To get the timing for a single file using hyperfine (which does multiple runs and gives stats), can do this via dune:
```
echo '(theories/WildCat/Equiv.v)' > file_to_bench
dune build @bench
```
To show the time for each line in a file, do:
```
make timing-html/HoTT.Modalities.ReflectiveSubuniverse.html 
```
and then view that file in a browser.
For any Coq project, can do
```
rm time-of-build.log  [optional; gets appended to]
make clean            [optional; depends whether you want to time only changed files]
make pretty-timed
```
to see a nice summary of the user time for each file, sorted. Saved in time-of-build.log and time-of-build-pretty.log. Add TIMING_REAL=1 to see real time instead. Can also compare revisions, etc. See

https://coq.inria.fr/refman/practical-tools/utilities.html#timing-targets-and-performance-testing

To find the slowest lines in the whole library:

make [-jX]
cd theories [or subdir to limit search]
find . -name '*.v.timing' -exec awk '{printf "%-55s %s\n", "{}:", $0}' {} \; | sort -nr -k7 | head -20 | sed 's/.v.timing//'

Locations are indicated by character position with the file. In emacs, can use M-x goto-char NNN RET to find the spot.

Copilot

Pull request overview

This PR adds a full classification result for short exact sequences of abelian groups via pointed maps between Eilenberg–Mac Lane spaces (Christensen–Flaten Thm 2.2.2), and extends the homotopical infrastructure needed to state/prove it in the HoTT Coq library.

Changes:

Introduces Algebra/AbSES/Classification.v, constructing the classifying map AbSES B A -> (K(B,2) ->* K(A,3)), its inverse via fibers, both round trips, the resulting equivalence, essential smallness of AbSES/Ext, and naturality.
Adds functoriality for K(-,n) (em_fmap) and supporting lemmas (identity/composition, connectivity/equivalence/naturality) plus a delooping equivalence on certain EM mapping types.
Strengthens exact-sequence and pointed-fiber infrastructure (naturality/rotation of connecting maps, and supporting lemmas about surjectivity/connectedness/fiber algebra).

Reviewed changes

Copilot reviewed 6 out of 6 changed files in this pull request and generated no comments.

Show a summary per file

File	Description
theories/Truncations/Connectedness.v	Adds a lemma showing maps from merely inhabited types into 0-connected types are surjective.
theories/Pointed/pFiber.v	Extends fiber/loops infrastructure with beta + naturality lemmas for `pfiber2_loops`.
theories/Homotopy/ExactSequence.v	Adds naturality/rotation results for connecting maps, built on new `pfiber2_loops` naturality.
theories/Homotopy/EMSpace.v	Adds `em_fmap` functoriality for `K(-,n)` and delooping-related mapping-type equivalences/lemmas.
theories/Homotopy/ClassifyingSpace.v	Adds contractibility and connectivity results for `B G` under group-level hypotheses.
theories/Algebra/AbSES/Classification.v	New classification theorem file connecting `AbSES` to EM-space mapping types, plus smallness + naturality.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

jdchristensen · 2026-06-19T15:35:07Z

@CharlesCNorton I think we've only scratched the surface, but the comments so far will probably cause enough changes that it would be best to handle them before we review any further.

Add theories/Algebra/Rings/ZBezout.v: integer absolute value and its multiplicativity, the integral-domain instance for cring_Z, the lift of NatBezout to an integer Bézout combination, and the IsBezoutDomain instance. Move rng_divides_plus from FreeModule.v to Bezout.v.

A house-style cleanup over the higher-Ext and rings development. Imports trimmed to what each file uses: - AbInjective.v: drop Modalities.ReflectiveSubuniverse. - Classification.v: drop AbHom. - HigherExtMorphism.v: drop Truncations.Core and AbHom. - HigherExtResolution.v: drop WildCat.Core. - LoopGroup.v: drop AbGroups.Biproduct. - FinitelyPresented.v: drop Types, WildCat.Core, AbGroups.AbelianGroup. - ZBezout.v: drop WildCat.Core, AbGroups.AbelianGroup, AbGroups.Z. Dead definitions removed: - HigherExt.v: ab_biprod_trivial_r. - HigherExtResolution.v: abses_ext_vanish_two, subsumed by abses_ext_vanish_resolution. - FreeModule.v: the unused span layer sm_gen_type, submodule_generated, submodule_generated_in, submodule_generated_rec, and isfreemodule_image_from_contr. - ZBezout.v: rng_divides_neg_r, rng_divides_neg_l, rng_divides_int_abs_l, nat_divides_of_rng_divides. Lemmas relocated to their proper files: - int_abs and its lemmas (int_abs_of_nat, int_abs_neg, int_abs_decomp, int_abs_of_nat_mul, int_abs_mul) move from ZBezout.v to Spaces/Int.v. - nat_mul_is_zero moves from ZBezout.v to Spaces/Nat/Core.v. - rng_divides_negate_r is generalized from cring_Z to any CRing and added to Rings/Bezout.v beside rng_divides_plus; ZBezout.v uses it. Other: - Eliminate the znat synonym, together with znat_mul and znat_add; int_bezout_nat and int_abs_to_var are now stated over Int and int_of_nat directly.

The remaining changes classify short exact sequences by pointed maps of Eilenberg-Mac Lane spaces, in Classification.v and LoopGroup.v, with supporting changes to EMSpace.v, ExactSequence.v, ClassifyingSpace.v, pFiber.v and Connectedness.v.

Reduce the file headers to the title and the result, and trim the multi-sentence docstrings in Classification.v to a single statement each.

The classification in Classification.v does not depend on LoopGroup.v (the computation of Pi 1 (AbSES B A) and the path components as classifying spaces), so it is removed from this PR.

- Remove line breaks from the added comments (STYLE.md). - Move contr_pi_succ_istrunc from EMSpace.v to HomotopyGroup.v. - Generalize pmap_punit_pconst to a contractible codomain (phomotopy_pconst_contr); drop the local copy in EMSpace.v.

Register K(-,n) as an Is0Functor, Is1Functor and IsPointedFunctor from abelian groups to pointed types, with em_fmap as the action on morphisms. em_fmap_const now follows from fmap_zero_morphism and pequiv_em_fmap from emap, removing their bespoke proofs.

CharlesCNorton changed the title ~~Show that each component of AbSES B A is a classifying space~~ Classify short exact sequences by maps of Eilenberg-Mac Lane spaces Jun 11, 2026

jdchristensen marked this pull request as draft June 11, 2026 13:08

jdchristensen reviewed Jun 11, 2026

View reviewed changes

Comment thread theories/Homotopy/ClassifyingSpace.v

Comment thread theories/Homotopy/ClassifyingSpace.v Outdated

Comment thread theories/Homotopy/ClassifyingSpace.v Outdated

Comment thread theories/Homotopy/ClassifyingSpace.v Outdated

CharlesCNorton force-pushed the abses-classification branch 21 times, most recently from ed3b07e to b3c2a65 Compare June 15, 2026 00:55

CharlesCNorton changed the title ~~Classify short exact sequences by maps of Eilenberg-Mac Lane spaces~~ Ext groups: classification, higher Ext, and algebra Jun 15, 2026

CharlesCNorton force-pushed the abses-classification branch 4 times, most recently from 40be009 to 1f130d6 Compare June 15, 2026 13:01

CharlesCNorton changed the title ~~Ext groups: classification, higher Ext, and algebra~~ Classify short exact sequences by maps of Eilenberg-Mac Lane spaces Jun 17, 2026

CharlesCNorton requested a review from jdchristensen June 17, 2026 21:57

jdchristensen reviewed Jun 17, 2026

View reviewed changes

jdchristensen reviewed Jun 18, 2026

View reviewed changes

Comment thread theories/Truncations/Connectedness.v Outdated

jdchristensen mentioned this pull request Jun 18, 2026

Modalities: generalize OO_conn_map_isconnected and other results #2371

Merged

Alizter reviewed Jun 19, 2026

View reviewed changes

jdchristensen requested a review from Copilot June 19, 2026 15:28

Copilot started reviewing on behalf of jdchristensen June 19, 2026 15:29 View session

Copilot AI reviewed Jun 19, 2026

View reviewed changes

CharlesCNorton and others added 7 commits June 20, 2026 08:42

Classify short exact sequences by maps of Eilenberg-Mac Lane spaces

07a0e2f

Shorten comments in Classification.v and LoopGroup.v

006333a

Reduce the file headers to the title and the result, and trim the multi-sentence docstrings in Classification.v to a single statement each.

Remove LoopGroup.v

5e1a5d6

The classification in Classification.v does not depend on LoopGroup.v (the computation of Pi 1 (AbSES B A) and the path components as classifying spaces), so it is removed from this PR.

ClassifyingSpace.v: minor simplification to proof (avoid inverse)

777f889

CharlesCNorton force-pushed the abses-classification branch from 42cbc0b to 777f889 Compare June 20, 2026 12:44

CharlesCNorton added 3 commits June 20, 2026 09:03

Replace issurjection_is0connected with the general isconnmap_isconnected

29de1d8

Reflow comments and relocate two helper lemmas

5d29317

- Remove line breaks from the added comments (STYLE.md). - Move contr_pi_succ_istrunc from EMSpace.v to HomotopyGroup.v. - Generalize pmap_punit_pconst to a contractible codomain (phomotopy_pconst_contr); drop the local copy in EMSpace.v.

		#[export] Instance isequiv_em_fmap (G G' : AbGroup) (n : nat)
		: IsEquiv (fun f : GroupHomomorphism G G' => em_fmap f n.+1).


		Section ClassifyingSpace.

		Local Set Polymorphic Inductive Cumulativity.

Conversation

CharlesCNorton commented Jun 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

New file

Supporting changes

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

jdchristensen commented Jun 11, 2026

Uh oh!

CharlesCNorton commented Jun 17, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

CharlesCNorton commented Jun 17, 2026

Uh oh!

CharlesCNorton commented Jun 17, 2026

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

jdchristensen commented Jun 18, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Alizter commented Jun 19, 2026

Uh oh!

Alizter commented Jun 19, 2026

Uh oh!

jdchristensen commented Jun 19, 2026

Uh oh!

jdchristensen commented Jun 19, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

jdchristensen commented Jun 19, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

CharlesCNorton commented Jun 11, 2026 •

edited

Loading

CharlesCNorton commented Jun 17, 2026 •

edited

Loading

jdchristensen commented Jun 19, 2026 •

edited

Loading