More H-spaces and Cohomology #1875

Alizter · 2024-02-25T11:05:13Z

In this PR we:

Define cohomology and show that the cohomology of the spheres S^n is as expected at degree n.
Define various sorts of H-space like structures: H-monoids, H-groups, H-abgroups etc. together with their "coherent" variants that allow H-structures to be lifted pointwise.

TODO:

Are we happy with the new hierarchy of algebraic structures for H-spaces?
Can we make the operation on cohomology easier to compute?
Clean up proofs with lots of path algebra.
Derive group structure on homotopy group using new structures?

Signed-off-by: Ali Caglayan <[email protected]>

Signed-off-by: Ali Caglayan <[email protected]>

theories/Homotopy/Cohomology.v

jdchristensen

Review is still in progress, but I'm submitting these comments so I don't lose them.

jdchristensen · 2024-02-26T13:38:17Z

theories/Homotopy/HSpace/HGroup.v

+Local Open Scope pointed_scope.
+Local Open Scope mc_mult_scope.
+
+(** A H-monoid is a H-space with an associative binary operation. *)


"an H-space" here and in other places

More generally, "[aA] H" -> "[aA]n H"

I think it depends on how we vocalise reading this in our heads. I don't say "aych" but rather "haych" so it sounds better to me to write "a H-space", but I am happy to change it if you think it is best.

Fascinating. I've always wondered why some people write "a h-space". I've never heard anyone pronounce "h" as "haych". Is it regional?

Do you also write "an historical"? That's another one I've never understood.

I've met a few people from different parts of the world that say "haych" (one from Nova Scotia, others from UK and Australia), but I think that "aych" is much more common, so we should use "an".

I'm not sure if there is a regional difference (within the UK). I think it must be a UK/US difference. I read somewhere that the pronunciation of the sound came and went in English, and sometime in the 19th century it became associated with the upper class. I would assume that is why Americans have a different pronunciation as 18th century English would sound slightly American to British English speakers nowadays. I could also probably understand the class divide as informal English I might speak with my mates would be on the side of "aych".

When I read or speak about something more formal in science or mathematics I tend to do so with a "posher" voice, so pronouncing the "H" seems more proper and formal.

I personally would say "a helicopter", "a hammock", "a hindrance", "a home" and "a hunter". Regarding the letter I would say "an" or "a" depending on how I pronounced "H". So "there's a haych in helicopter" and "there's an aych in helicopter" both work, but depend on the sound I make rather than the actual spelling.

Anyway, I'll change these all to "an" as I've already accepted US English to be the default here.

jdchristensen · 2024-02-26T13:46:09Z

theories/Homotopy/HSpace/Coherent.v

+  associative_iscohassoc_coh : simple_associativity pt pt pt
+      = ap (pt *.) (left_identity pt) @ ap (.* pt) (left_identity pt)^;


Why choose this coherence out of the possible coherences? It favours the left identity, so is not symmetrical. Maybe a more natural coherence would change just the second left_identity to right_identity, so it is always the middle pt that is being absorbed. (And in this case, it generalizes to a * (pt * b) = (a * pt) * b. Why assume it only when a and b are pt?) There are still other coherences when the first or third variable is fixed to be pt and the others are general.

It is quite artificial, but it is literally what is needed to make the pointwise H-space work. I'm not certain it's possible to do without it.

Another way to think about this is using the associativity of smash. If a coherent H-space corresponds to a pointed map A /\ A ->* A then a "coherently" associative H-space should correspond to the pointed equation for A /\ (A /\ A) to A in two different ways agreeing.

I don't think motivating the coherences strictly by what is needed for the pointwise H-space structure to work is necessarily the best guide. Ideally, we would add the coherences that make things match the classical story.

In this particular case, I think you should make the change I suggested, to make things symmetric. When you use this for the pointwise structure, you probably also have IsCohHspace, in which case the two identity laws agree at the basepoint. In addition, with my version of the coherence you can make it more general, which I think makes sense.

jdchristensen · 2024-02-26T13:51:43Z

theories/Homotopy/HSpace/Coherent.v

+(** A coherent H-monoid, also known as a coherent A_3-space, is a coherent H-space that is also coherently associative. *)
+Class IsCohHMonoid (A : pType) := {
+  iscohhspace_iscohhmonoid :: IsCohHSpace A;
+  iscohassoc_cohassochspace :: IsCohAssociative A;
+}.


Are you sure this matches the classical notion of A_3-space? Often the unit laws are taken to be strict, so it is hard to compare. What you have here certainly doesn't match what the n-lab writes, but I'm also doubtful that the n-lab has the correct definition, since it doesn't include that the unitors agree on pt.

I'm not certain about the strictness of the unit laws. I didn't use the nlab to compare the definitions but rather from Adams' book on infinite loop spaces. There A_2 corresponds to H-spaces and A_3 corresponds to a H-space with a associativity homotopy.

Sure, A_3 is associativity, but with appropriate coherences. Classically A_2 corresponds not to IsHSpace but to IsCohHSpace. So the question here would be what coherences are needed to make this match A_3. I don't know the answer, so I suggest removing the comment unless this is worked out.

OK I see what you mean now. I'll remove the comment as a "coherent A_3" space is already a bit fictional.

jdchristensen · 2024-02-26T13:53:45Z

theories/Homotopy/HSpace/Coherent.v

+Definition iscohhmonoid_equiv_cohmonoid {X Y : pType} `{IsCohHMonoid Y} (f : X <~>* Y)
+  : IsCohHMonoid X.


Maybe each of the properties should be shown to be preserved by equivalences (as separate results)? Would it help to use pointed_reduce_pmap f at the start?

It did not help to use pointed_reduce_pmap at the start as the goal has to be well-defined after path inducting on point_eq. I basically had to wrangle to goal and get rid of any f^-1 to make this work before using pelim. It might be possible to do this earlier, I'll have to try it out.

jdchristensen · 2024-02-26T13:55:19Z

theories/Homotopy/HSpace/Coherent.v

+Class IsCohCommutative (X : pType) `{IsHSpace X} := {
+  commutative_iscohcommutative :: Commutative (.*.);
+  iscohcommutative : commutativity pt pt = 1;
+}.


Again, why this choice of coherence? One would naturally also want that a * pt = pt * a respects the two unit laws.

jdchristensen · 2024-02-26T13:58:42Z

theories/Homotopy/HSpace/Coherent.v

+Definition iscohcommutative_equiv_cohcommutative {X Y : pType} `{IsCohCommutative Y} (f : X <~>* Y)
+  : @IsCohCommutative X (ishspace_equiv_hspace f).
+Proof.


Here and in other results about preservation along equivalences, another possibility is to use equiv_intro at the start. Not sure if it will work.

The only downside is that requires Funext which isn't strictly required here. It also extracting the operation out more difficult as we now have a path that must be reduced. So a direct equivalence might be better. We don't yet reason about this path however, but we might in the future if we decide to define an "associatively truncated E_n space" for some n.

Does equiv_intro require Funext? I don't see that, but maybe I'm missing something. I thought that equiv_intro produces proof terms that compute. But maybe they aren't as good as what you wrote?

Sorry you are correct, it does not require funext. I seem to be confused. It produces a transport which I think should be good enough here.

jdchristensen · 2024-02-26T14:14:49Z

theories/Homotopy/HSpace/Coherent.v

+  left_inverse_coh : left_inverse pt = ap (.* pt) negate_coh @ hspace_left_identity pt;
+  right_inverse_cohhgroup :: RightInverse (.*.) negate_cohhgroup pt;
+  right_inverse_coh : right_inverse pt = ap (pt *.) negate_coh @ hspace_left_identity pt;


I think all definitions should be symmetric in left and right. So one of the hspace_left_identitys should be changed to hspace_right_identity. Probably the first one. (Also, if dropping the hspace_ part works, we should do that for consistency.)

Actually, thinking about it more, negate_coh is provable: negate pt = (negate pt) * pt = pt, using the right identity and the left inverse. It's also provable in the symmetric way. If we assume that the commutativity respects the identity laws (as mentioned above) and that it also respect the two inverse laws, then these two proofs of negate pt = pt would be equal. So I think respecting commutativity should be taken as the basic laws, and negate pt = pt should be proven. (But this is just off the top of my head. The space of possible coherence laws is large, and I'm not sure it makes sense to just take guesses here.)

Sorry, I just realized that we aren't in the commutative situation here. Still, the three coherences above could possibly be replaced with a single coherence saying that the two proofs of negate pt = pt are equal. Not sure.

That would be neat if we could reduce the number of coherences. As I said before, the reason we have them at all is to get the pointwise proof to go through. Using the heuristic of "one property one coherence" it made sense to have 3 coherences here. This structure could of course be split up with left-invertible, right-invertible and negatable H-spaces, but I didn't see the point in doing that. I also tried thinking about if these properties arise from H-space multiplication being invertible, but I couldn't work out how to prove it so I'm not sure.

I don't think "one property one coherence" is a good guiding principle. Currently, a certain path type x = y has two proofs, and you are adding one more as data. That means you probably want to have two coherences that say that the new data is equal to the two existing proofs. But that's the same as simply saying that the two existing proofs are equal (and not providing a new proof).

In JAMES, I. M. (1960). ON H-SPACES AND THEIR HOMOTOPY GROUPS. There is an argument showing that an associative H-space X gives a group structure on [Y,X]. I'll need to think about it some more, but it gives me hope that Y ->** X can be made into a H-group without the need of these coherent structures for inverses.

I think I saw somewhere else that unpointed maps into a H-space are equivalent to pointed maps.

Pointed maps Unit ->* Circle are different from unpointed maps Unit -> Circle. Maybe you are thinking of the fact that two pointed maps into an H-space are pointed homotopic iff they are unpointed homotopic? This is hspace_phomotopy_from_homotopy.

I found what I was talking about but it was about homotopy classes of maps rather than the mapping space. https://www.math.uni-bielefeld.de/~tcutler/pdf/Week%205%20-%20Pointed%20vs%20Unpointed%20Homotopy.pdf (ex 1.5 here, which also works for H-spaces no just top groups). I don't think this is helpful for us however.

Oh, right. When the codomain is a connected H-space, homotopy classes do agree, and that actually follows from hspace_phomotopy_from_homotopy.

What confused me is that the circle is connected right? So why doesn't that work?

As you said, it is homotopy classes of maps that agree, so it does work. hspace_phomotopy_from_homotopy only gives a logical equivalence between pointed homotopies and unpointed homotopies, so we only get an equivalence after 0-truncating the mapping space.

jdchristensen · 2024-02-26T14:18:10Z

theories/Homotopy/HSpace/Coherent.v

+Class IsCohHAbGroup (A : pType) := {
+  iscohgroup_cohabgroup :: IsCohHGroup A;
+  commutative_cohabgroup :: IsCohCommutative A;


It feels like the commutativity should be assumed to respect the two inverse laws.

It wasn't needed for the pointwise strucutres, but presumably at a higher level that would come into play.

Yes, probably. It's hard to know exactly what to assume, but this seems pretty natural, and (as I mentioned before) I don't think that the pointwise structures should be the only guiding principle.

jdchristensen · 2024-02-26T14:21:50Z

theories/Homotopy/HSpace/HGroup.v

+}.
+
+(** A H-group is a H-space with an associative binary operation an inversion. *)
+Class IsHGroup (X : pType) := {


CohHGroup was defined in the other file. I feel like the heirarchy should be kept close together. Or at least all of the stuff about H-groups should be together. And do we need the non-coherent versions of everything? We end up with so many variations.

We have a lot of variations I agree. It all comes down to which properties the pointwise "H-structures" have. I wasn't able to show that Y ->** X is a coherent version (I didn't try very hard), but I also didn't need to show it as it doesn't matter when truncating. For showing cohomology is a group, this isn't needed. We need to think a bit harder about which properties we would like to keep. We could even consider redefining H-space and requiring it to be coherent, but I haven't thought about that too much.

jdchristensen · 2024-02-26T14:22:58Z

theories/Homotopy/HSpace/HGroup.v

+(** A H-commutative monoid is a H-space with an associative and commutative binary operation. *)
+Class IsHCommutativeMonoid (X : pType) := {


"A commutative H-monoid"? IsCommutativeHMonoid?

I'll change that. My way makes sense if you think of H- as modifying the algebraic structure that comes after it, but in the AT literature this definitely isn't written that way.

jdchristensen · 2024-02-26T14:23:39Z

theories/Homotopy/HSpace/HGroup.v

+(** A H-abelian group is a H-space with an associative and commutative binary operation and invertible left and right multiplication. *)
+Class IsHAbGroup (X : pType) := {


"An abelian H-group"? ("an H-space") IsAbHGroup?

Using abelian here is a bit of terminological abuse, I might just replace it with commutative, however it is easier to write Ab.

jdchristensen · 2024-02-26T14:25:10Z

theories/Homotopy/HSpace/HGroup.v

+  exact (- x).
+Defined.
+
+(** The 0-truncation of a H-group is a group. *)


Can some things in HomotopyGroup.v now be replaced with facts from this file?

Yes! In fact, the entire group and abelian group structure can come from this. Before I do that however, I would like to clear up the H-structure hierarchy.

jdchristensen · 2024-02-26T14:29:03Z

theories/Homotopy/HSpace/Pointwise.v

@@ -109,3 +108,102 @@ Proof.
      refine (whiskerL _ iscoherent @ _).
      exact (concat_A1p right_identity (point_eq f)).
 Defined.
+
+(** If the H-space structure on [X] is right-invertible, so is the one induced on [Y ->** X]. *)


There's an operation on H-space structures that swaps the order of the multiplication:

(** We can twist H-space structures by swapping the arguments. *) Definition ishspace_twist {X : pType} : IsHSpace X -> IsHSpace X. Proof. intros [mu mu_lid mu_rid]. exact (Build_IsHSpace X (fun x y => mu y x) mu_rid mu_lid). Defined. (** [ishspace_twist] is definitionally involutive *) (* Check idpath : ishspace_twist o ishspace_twist = idmap. *) Local Notation "m ^T" := (ishspace_twist m) (at level 5).

This can be used (like op in the wildcat library) to avoid reproving symmetrical results. (And this is one reason why it is important for the definitions to be symmetric.)

Yes, I suspected that might be true since the same happens for groups.

Right, I noticed that some symmetrical arguments for groups are duplicated. The "twist" trick could help there as well.

It also depends on if we need to reason about these paths for higher A_n/E_n structures. Presumably having a symmetric proof and not one that uses a trick makes those proofs easier. We don't have this problem for regular groups as we don't actually care what the proof of an equality is due to being a hprop.

The trick of using the twisted structure should definitionally produce the same proof that is written out by hand a second time, so I don't think it will cause any issues.

jdchristensen · 2024-02-26T14:30:15Z

theories/Homotopy/HSpace/Pointwise.v

+    apply associative_iscohassoc_coh.
+Defined.
+
+(** If the H-space structure on [X] is a coherent H-space, then the H-space structure on [Y ->** X] is a H-monoid. *)


"If [X] is a coherent H-monoid"

jdchristensen · 2024-02-26T14:30:37Z

theories/Homotopy/HSpace/Pointwise.v

+Global Instance ishmonoid_hspace_pmap `{Funext} (X Y : pType) `{IsCohHMonoid X}
+  : IsHMonoid (Y ->** X) := {}.
+
+(** If the H-space structure on [X] is a coherent H-group, then the H-space structure on [Y ->** X] is a H-group. *)


"If [X] is a coherent H-group, then".

Same for next one below.

jdchristensen · 2024-02-26T14:32:01Z

theories/Homotopy/HSpace/HGroup.v

+Local Open Scope pointed_scope.
+Local Open Scope mc_mult_scope.
+
+(** A H-monoid is a H-space with an associative binary operation. *)


More generally, "[aA] H" -> "[aA]n H"

jdchristensen

@Alizter Ok, I'm done a pass through this. I'll look again after you respond and/or make changes.

theories/Homotopy/Cohomology.v

jdchristensen · 2024-02-26T14:43:22Z

theories/Homotopy/Cohomology.v

+(* 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.


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.

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.

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

jdchristensen · 2024-02-26T14:46:31Z

theories/Homotopy/Cohomology.v

+  nrefine (_ oE (equiv_tr 0 _)^-1).
+  1: refine ?[goal1].
+  2: { rapply istrunc_equiv_istrunc. symmetry. apply ?goal1. }


I think istrunc_pmap should also solve goal 2.

jdchristensen · 2024-02-26T14:46:44Z

theories/Homotopy/Cohomology.v

+
+(* 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.


Can we change n.+1 to n?

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

jdchristensen · 2024-02-26T14:50:14Z

theories/Homotopy/EMSpace.v

+    nrapply iscohhabgroup_equiv_cohhabgroup.
+    2: apply pequiv_loops_em_em.
+    nrapply iscohhabgroup_equiv_cohhabgroup.
+    2: exact (emap loops (pequiv_loops_em_em _ _)).


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

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.

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.

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.

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

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

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

Alizter added 2 commits February 25, 2024 11:06

various levels of H-space structure and coherence

6dae88b

Signed-off-by: Ali Caglayan <[email protected]>

definition of cohomology groups

c9af28b

Signed-off-by: Ali Caglayan <[email protected]>

Alizter force-pushed the cohomology branch from 568f170 to c9af28b Compare February 25, 2024 11:06

Alizter commented Feb 25, 2024

View reviewed changes

theories/Homotopy/Cohomology.v Show resolved Hide resolved

jdchristensen reviewed Feb 26, 2024

View reviewed changes

		associative_iscohassoc_coh : simple_associativity pt pt pt
		= ap (pt .) (left_identity pt) @ ap (. pt) (left_identity pt)^;

		Definition iscohhmonoid_equiv_cohmonoid {X Y : pType} `{IsCohHMonoid Y} (f : X <~>* Y)
		: IsCohHMonoid X.

		(** A H-commutative monoid is a H-space with an associative and commutative binary operation. *)
		Class IsHCommutativeMonoid (X : pType) := {

		(** A H-abelian group is a H-space with an associative and commutative binary operation and invertible left and right multiplication. *)
		Class IsHAbGroup (X : pType) := {

More H-spaces and Cohomology #1875

Are you sure you want to change the base?

More H-spaces and Cohomology #1875

Conversation

Alizter commented Feb 25, 2024 • edited Loading

jdchristensen left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jdchristensen Feb 26, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jdchristensen Feb 26, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Alizter Feb 28, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Alizter Feb 29, 2024 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jdchristensen left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Alizter commented Feb 25, 2024 •

edited

Loading

jdchristensen Feb 26, 2024 •

edited

Loading

jdchristensen Feb 26, 2024 •

edited

Loading

Alizter Feb 28, 2024 •

edited

Loading

Alizter Feb 29, 2024 •

edited

Loading