Skip to content
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

Jump to bottom

More H-spaces and Cohomology #1875

Draft
wants to merge 2 commits into
base: master
Choose a base branch
from
Draft

More H-spaces and Cohomology #1875

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
6dae88b
various levels of H-space structure and coherence
Alizter Feb 25, 2024
c9af28b
definition of cohomology groups
Alizter Feb 25, 2024
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
5 changes: 5 additions & 0 deletions theories/Algebra/AbGroups/AbelianGroup.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,11 @@ Record AbGroup := {
Coercion abgroup_group : AbGroup >-> Group.
Global Existing Instance abgroup_commutative.

Definition Build_AbGroup' (G : Type) `(IsAbGroup G) : AbGroup := {|
abgroup_group := Build_Group G _ _ _ _;
abgroup_commutative := _;
|}.

Global Instance isabgroup_abgroup {A : AbGroup} : IsAbGroup A.
Proof.
split; exact _.
Expand Down
51 changes: 51 additions & 0 deletions theories/Homotopy/Cohomology.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,51 @@
Require Import Basics Types Pointed WildCat.Core WildCat.Equiv.
Require Import Truncations.Core.
Require Import Homotopy.EMSpace.
Require Import Homotopy.HSpace.Core Homotopy.HSpace.Pointwise Homotopy.HSpace.HGroup Homotopy.HSpace.Coherent.
Require Import Algebra.AbGroups.AbelianGroup.
Require Import Homotopy.Suspension.
Require Import Spheres HomotopyGroup.

Local Open Scope pointed_scope.

(** * Cohomology groups *)

(** Reduced cohomology groups are defined as the homotopy classes of pointed maps from the space to an Eilenberg-MacLane space. The group structure comes from the H-space structure on [K(G, n)]. *)
Alizter marked this conversation as resolved.
Show resolved Hide resolved
Definition Cohomology `{Univalence} (n : nat) (X : pType) (G : AbGroup) : AbGroup.
Proof.
snrapply Build_AbGroup'.
1: exact (Tr 0 (X ->** K(G, n))).
1-3: shelve.
nrapply isabgroup_ishabgroup_tr.
nrapply ishabgroup_hspace_pmap.
apply iscohhabgroup_em.
Defined.

(** ** Cohomology of suspension *)

(** The (n+1)th cohomology of a suspension is the nth cohomology of the original space. *)
(* TODO: show this preserves the operation somehow and is therefore a group iso *)
Definition cohomology_susp `{Univalence} n (X : pType) G
: Cohomology n.+1 (psusp X) G <~> Cohomology n X G.
Comment on lines +27 to +29
Copy link
Collaborator

Choose a reason for hiding this comment

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

The obvious argument that this is a group iso has a few steps: The operation on the LHS coming from the H-space structure on K(G, n+1) is equal to the operation on the LHS coming from the coH-space structure on the suspension (Eckmann-Hilton). Then, the loop-susp adjunction takes the coH operation to the H operation. Then pequiv_loops_em_em is what we use the define the H-space structure on K(G,n), so it preserves it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I could prepare some of my stuff on co-H-spaces and pointwise H-spaces to allow for this argument, but I was hoping that the operation on cohomology would be easy to work with letting us prove preservation of the operation more directly. I see that isn't actually the case however, as the H-space strucutre we get with the pointwise operation is always going to be tricky to work with. Therefore it might be better just to define the bundled versions of all the algebraic strucutres I introduced, show that they are various induced wildcat's (with H-maps) and then show that 0-truncation is a functor from those wild categories to Group or AbGroup. That way we get this equivalence in a functorial way.

We also have other cohomology axioms that we can directly verify, but I haven't spent the time to work on those just yet until we can agree on how we want the H-strucutres to look.

The wedge axiom for instance, will probably require decidable equality on the indexing type if we want to avoid the axiom of choice. And in most cases we take a wedge, it is over a type with decidable equality.

Copy link
Collaborator

Choose a reason for hiding this comment

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

I think it's best to leave this for a future PR.

Proof.
apply Trunc_functor_equiv.
nrefine (_ oE (loop_susp_adjoint _ _)).
rapply pequiv_pequiv_postcompose.
symmetry.
apply pequiv_loops_em_em.
Defined.

(** ** Cohomology of spheres *)

(* TODO: improve this to a group isomorphism once cohomology can be easily checked to be op preserving. *)
Definition cohomology_sn `{Univalence} (n : nat) (G : AbGroup)
: Cohomology n.+1 (psphere n.+1) G <~> G.
Copy link
Collaborator

Choose a reason for hiding this comment

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

Can we change n.+1 to n?

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, I didn't want to special case n=0, but it should be simple to do. I'll improve that.

Proof.
nrefine (_ oE (equiv_tr 0 _)^-1).
1: refine ?[goal1].
2: { rapply istrunc_equiv_istrunc. symmetry. apply ?goal1. }
Comment on lines +44 to +46
Copy link
Collaborator

Choose a reason for hiding this comment

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

I think istrunc_pmap should also solve goal 2.

nrefine (_ oE pmap_from_psphere_iterated_loops _ _).
symmetry.
rapply pequiv_loops_em_g.
Defined.

10 changes: 10 additions & 0 deletions theories/Homotopy/EMSpace.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -103,5 +103,15 @@ Section EilenbergMacLane.
2: apply pequiv_loops_em_em.
apply iscohhspace_loops.
Defined.

Definition iscohhabgroup_em {G : AbGroup} (n : nat)
: IsCohHAbGroup K(G, n).
Proof.
nrapply iscohhabgroup_equiv_cohhabgroup.
2: apply pequiv_loops_em_em.
nrapply iscohhabgroup_equiv_cohhabgroup.
2: exact (emap loops (pequiv_loops_em_em _ _)).
Comment on lines +110 to +113
Copy link
Collaborator

Choose a reason for hiding this comment

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

One use of iscohhabgroup_equiv_cohhabgroup should be enough, with a composite equivalence. Maybe this will speed things up a bit?

(BTW, one can also define the H-space structure on K(G,n) using that the addition map G x G -> G is a homomorphism when G is abelian, so we get K(G,n) x K(G,n) <~> K(G x G, n) -> K(G, n) using functoriality. This doesn't need the delooping at all, but will instead require checking all of the axioms.)

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

In this case, the commutativity of the H-space structure should follow from G being abelian. However, here I am using the fact that loops o loops produce abelian H-groups.

I'll have a think about making the H-space structure on K(G,n) more direct. On the other hand, how often do we need to compare this H-space structure to one given by loops? I'll have to think about it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

I guess since all H-space structures on K(G,n) are equivalent in the appropriate sense, it only makes sense to put a good H-space structure on it.

Copy link
Collaborator

Choose a reason for hiding this comment

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

My main comment was that you only need to use iscohhabgroup_equiv_cohhabgroup once:

    nrapply iscohhabgroup_equiv_cohhabgroup.
    2: exact (emap loops (pequiv_loops_em_em G n.+1) o*E pequiv_loops_em_em G n).
    apply iscohhabgroup_loops_loops.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Suggested change
nrapply iscohhabgroup_equiv_cohhabgroup.
2: apply pequiv_loops_em_em.
nrapply iscohhabgroup_equiv_cohhabgroup.
2: exact (emap loops (pequiv_loops_em_em _ _)).
nrapply iscohhabgroup_equiv_cohhabgroup.
2: exact (emap loops (pequiv_loops_em_em G n.+1) o*E pequiv_loops_em_em G n).

Copy link
Collaborator Author

Choose a reason for hiding this comment

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

Yes, I've tried this but it is still quite slow. I'll experiment a bit with the direct definition.

Copy link
Collaborator

Choose a reason for hiding this comment

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

Can you remind me what is slow? The specific definition we're discussing is fast for me.

apply iscohhabgroup_loops_loops.
Defined.

End EilenbergMacLane.
2 changes: 2 additions & 0 deletions theories/Homotopy/HSpace.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,3 +2,5 @@ Require Export HSpace.Core.
Require Export HSpace.Coherent.
Require Export HSpace.Pointwise.
Require Export HSpace.Moduli.
Require Export HSpace.HGroup.

Loading
Loading