Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
CharlesCNorton wants to merge 12 commits into
base: master
Choose a base branch
from
Open

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
12 commits
Select commit Hold shift + click to select a range
07a0e2f
Classify short exact sequences by maps of Eilenberg-Mac Lane spaces
CharlesCNorton Jun 14, 2026
4788873
Prove the integers form a Bézout domain
CharlesCNorton Jun 15, 2026
02fed61
Lean imports, remove dead definitions, relocate lemmas to home files
CharlesCNorton Jun 15, 2026
6c6a30c
Remove the higher Ext development, keeping the EM-space classification
CharlesCNorton Jun 17, 2026
006333a
Shorten comments in Classification.v and LoopGroup.v
CharlesCNorton Jun 17, 2026
5e1a5d6
Remove LoopGroup.v
CharlesCNorton Jun 17, 2026
777f889
ClassifyingSpace.v: minor simplification to proof (avoid inverse)
jdchristensen Jun 18, 2026
29de1d8
Replace issurjection_is0connected with the general isconnmap_isconnected
CharlesCNorton Jun 20, 2026
5d29317
Reflow comments and relocate two helper lemmas
CharlesCNorton Jun 20, 2026
232829f
EMSpace: make K(-,n) a wild category functor
CharlesCNorton Jun 21, 2026
c265350
EMSpace: generalize the delooping equivalence to all levels
CharlesCNorton Jun 21, 2026
ebd0d35
pFiber: build functor_pfiber's basepoint path with path_sigma'
CharlesCNorton Jun 21, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1,125 changes: 1,125 additions & 0 deletions theories/Algebra/AbSES/Classification.v
View file
Open in desktop

Large diffs are not rendered by default.

32 changes: 32 additions & 0 deletions theories/Homotopy/ClassifyingSpace.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -29,6 +29,8 @@ Module Export ClassifyingSpace.

Section ClassifyingSpace.

Local Set Polymorphic Inductive Cumulativity.

@Alizter Alizter Jun 19, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.

@jdchristensen jdchristensen Jun 19, 2026

Copy link
Copy Markdown
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

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.")


Private Inductive ClassifyingSpace (G : Group) :=
| bbase : ClassifyingSpace G.

Expand Down Expand Up @@ -404,6 +406,16 @@ Section HSpace_bg.

End HSpace_bg.

(** The classifying space of a contractible group is contractible. *)
Instance contr_pclassifyingspace `{Univalence} (G : Group) `{Contr G}
: Contr (B G).
Comment thread
CharlesCNorton marked this conversation as resolved.
Proof.
rapply (contr_equiv' pUnit (Build_Equiv _ _ pconst _)).
(* The map from [pUnit] is an equivalence, since it is one on loops, as both have contractible loop spaces. *)
pose proof (contr_equiv' G equiv_g_loops_bg).
rapply isequiv_is0connected_isequiv_loops.
Defined.

(** Functoriality of B(-) *)

Instance is0functor_pclassifyingspace : Is0Functor B.
Expand Down Expand Up @@ -442,6 +454,26 @@ Proof.
apply pbloop_natural.
Defined.

(** [fmap B] of a surjective group homomorphism is a 0-connected map. *)
Instance isconnmap_fmap_pclassifyingspace `{Univalence} {G K : Group}
(f : GroupHomomorphism G K) `{!IsSurjection f}
: IsConnMap 0 (fmap B f).
Proof.
(* By [isconnmap_isconnmap_ap_surj] it suffices to show that [fmap B f] and its [ap]s are surjective; both follow from surjectivity of [f]. *)
snapply isconnmap_isconnmap_ap_surj.
- rapply (isconnmap_isconnected (-1)).
- rapply (conn_point_elim (-1) (A:=B G)).
rapply (conn_point_elim (-1) (A:=B G)).
srapply (equiv_ind equiv_g_loops_bg).
intro h.
rapply contr_inhabited_hprop.
pose proof (m := center (Tr (-1) (hfiber f h))).
strip_truncations.
destruct m as [g p].
exact (tr (bloop g;
ClassifyingSpace_rec_beta_bloop _ _ _ _ g @ ap bloop p)).
Defined.

Instance is1functor_pclassifyingspace : Is1Functor B.
Proof.
apply Build_Is1Functor.
Expand Down
Loading
Loading