πₙ(Sⁿ) = Z, and other cleanups #1800
Conversation
| (** The nth homotopy group is in fact a functor. We now give the type this functor ought to have. For n = 0, this will simply be a pointed map, for n >= 1 this should be a group homomorphism. *) | ||
| Definition pi_functor_type (n : nat) (X Y : pType) : Type | ||
| := match n with | ||
| | 0 => pTr 0 X ->* pTr 0 Y | ||
| | n.+1 => GroupHomomorphism (Pi n.+1 X) (Pi n.+1 Y) | ||
| end. | ||
|
|
||
| (* Every such map is, in particular, a pointed map. *) | ||
| Definition pi_functor_type_pmap {n X Y} | ||
| : pi_functor_type n X Y -> Pi n X ->* Pi n Y | ||
| := match n return pi_functor_type n X Y -> (Pi n X ->* Pi n Y) with | ||
| | 0 => fun f => f | ||
| (* This works because [pmap_GroupHomomorphism] is already a coercion. *) | ||
| | n.+1 => fun f => f | ||
| end. | ||
| Coercion pi_functor_type_pmap : pi_functor_type >-> pForall. |
There was a problem hiding this comment.
These lines were removed because this Coercion didn't work. The problem is that pi_functor_type isn't syntactically the same as the output type of fmap (Pi n) f, so the coercion wouldn't kick it. I tried a few things and concluded that it's probably not possible. That's why I introduced pPi as a functor directly landing in pointed types.
There was a problem hiding this comment.
(The coercion did work for fmap (Pi n.+1) f, but in that case the existing coercion from groups to pointed types also works.)
There was a problem hiding this comment.
I think this is more trouble to get working than it is worth in the end. I think if you really want to be precise with this functor in practice, its better to use an explicit version anyway. I think your solution is good going fowrad.
| @@ -251,6 +251,19 @@ Proof. | |||
| exact (equiv_path_prod (fst f _, snd f _) (dpoint P, dpoint Q)). | |||
| Defined. | |||
|
|
|||
| Definition functor_pprod {A A' B B' : pType} (f : A ->* A') (g : B ->* B') | |||
There was a problem hiding this comment.
We have a notion of bifunctor, but I'm not sure if it would be useful to use here.
|
@jdchristensen Feel free to push your renaming commit, I'm happy with the changes. It's good to have this result finally. Hopefully Pi3S2 is also doable since we should have most of the tools in place. |
|
I added two commits with minor changes, and then a third that renamed Pi1S1.v. |
There are three commits and it's probably best to look at them separately. The library builds after each commit.
Proves that πₙ(Sⁿ) = Z. It turns out that very little was needed to prove this, since the n = 2 case follows from the
licata_finsterlemma we already had, since S¹ is a coherent H-space. The higher cases follow from Freudenthal.Improves
pi_prodin HomotopyGroup.v in a few independent ways. First, it is now proven for all n, not just n > 0. Second, the map underlying the equivalence is now the natural one, so there is no need to manually prove that it is a group homomorphism for n > 0. Third, the proof is much faster. (TheDefined.line used to be a bit slow.)This commit contains lots of minor cleanups to things I read while working on the first two. It also adds some lemmas that I didn't end up using, but which are probably worth having. But it's definitely better to review this separately, since it touches a lot.
After review, I'll push one more commit that renames Pi1S1.v to PinSn.v, but I've left that out for now to make it easier to review. That's the only reason this is marked as a draft.