flattening lemma for Coeq, Pushout and improvements to Hopf #1857
Conversation
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
Signed-off-by: Ali Caglayan <[email protected]>
0c343b8 to
911b027
Compare
|
This sounds great! I'll take a look at it tomorrow, I hope. You are on a roll, and it's a full time job keeping up! |
|
This is the last of what I have that's finished for now. It will probably be some time before I manage another sprint. |
|
Is it ok if I make some commits to simplify a bit of path algebra? |
|
Do you think that Colimit_Flattening.v will also follow fairly easily from flattening for coequalizers? |
|
@jdchristensen feel free to push to this PR. I think flattening for colimits will follow easily too, however I don't have a need for it just yet. |
|
Ok, I'm working on this, so don't push anything for a while. |
It seems like when defining a type foo in terms of bar, it works out better to define the recursion principle for bar directly in terms of the recursion principle for foo, rather than via the induction principle for bar, which uses the induction principle for foo.
|
@Alizter I just pushed two commits, but I'll have more later, so please don't push anything. The first commit just contains minor simplifications to the path algebra in Coeq.v. The second one simplifies things a lot in Pushout.v. I noticed that if we define Pushout_rec using Coeq_rec (instead of defining it using Pushout_ind which uses Coeq_ind), the first equivalence you had becomes a definitional equality. Then, to make the Hopf proof go through, I needed to make the parallel change to Susp_rec. |
|
Ok, I'm done, and this LGTM. Nice work. My last commit just adjusts a few comments. |
|
Great! |
The first two commits in this PR are about deriving the flattening lemma for Coeq from the flattening lemma for GraphQuotient, and then the flattening lemma for Pushout out of the one for Coeq.
An immediate application is that the flattening lemma is now computable in reasonable time allowing us to improve the equivalence for the total space of the Hopf fibration.
I also delete PushoutFlattening.v as this was really about deriving the flattening lemma from the (slow) colimits library. Now that we have a more direct result, things are simpler.
There is the question of splitting things up as discussed in #1855, however I will leave this to a future PR so this one can more easily be reviewed.