[Merged by Bors] - feat: projectivity of Stonean in CompHaus #5808
[Merged by Bors] - feat: projectivity of Stonean in CompHaus #5808dagurtomas wants to merge 32 commits intomasterfrom
Stonean in CompHaus #5808Conversation
Stonean in CompHaus
|
|
||
| /-- The morphism from `presentation X` to `X`. -/ | ||
| noncomputable | ||
| def presentationπ (X : CompHaus) : X.presentation.compHaus ⟶ X := |
There was a problem hiding this comment.
What do you think of chopping the name into an extra namespace part?
| def presentationπ (X : CompHaus) : X.presentation.compHaus ⟶ X := | |
| def presentation.π (X : CompHaus) : X.presentation.compHaus ⟶ X := |
There was a problem hiding this comment.
I agree that looks nicer
There was a problem hiding this comment.
When I change to presentation.π, I can't write X.presentation.π in the instance below anymore. It complains that "the environment does not contain Stonean.π, presentation X has type Stonean".
There was a problem hiding this comment.
No permutation of parentheses fixes the problem
There was a problem hiding this comment.
We could go with presentation_π and presentation_epi_π which I think is still nicer than the old names.
Or we can still go with your suggestion and then write the instance below as
instance presentation.epi_π (X : CompHaus) : Epi (π X)
What do you think?
There was a problem hiding this comment.
I've pushed your suggestion, but I'm happy with whatever
There was a problem hiding this comment.
Let's try it out like this. We can rename again later if we are unhappy.
|
|
||
| /-- The morphism from `presentation X` to `X` is an epimorphism. -/ | ||
| noncomputable | ||
| instance epiPresentπ (X : CompHaus) : Epi X.presentationπ := |
There was a problem hiding this comment.
If you agree with the above suggestion, then this might become
| instance epiPresentπ (X : CompHaus) : Epi X.presentationπ := | |
| instance presentation.epi_π (X : CompHaus) : Epi X.presentationπ := |
|
Thanks 🎉 bors merge |
Co-authored-by: Filippo A E Nuccio [filippo.nuccio@univ-st-etienne.fr](mailto:filippo.nuccio@univ-st-etienne.fr) Co-authored-by: Nikolas Kuhn [nikolaskuhn@gmx.de](mailto:nikolaskuhn@gmx.de) Co-authored-by: Adam Topaz [topaz@ualberta.ca](mailto:topaz@ualberta.ca) - [x] depends on: #5634 - [x] depends on: #5761 This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed. Co-authored-by: David Kurniadi Angdinata <dka31@cantab.ac.uk>
|
Pull request successfully merged into master. Build succeeded! The publicly hosted instance of bors-ng is deprecated and will go away soon. If you want to self-host your own instance, instructions are here. If you want to switch to GitHub's built-in merge queue, visit their help page. |
Stonean in CompHaus Stonean in CompHaus
Co-authored-by: Jon Eugster @joneugster Co-authored-by: Boris Bolvig Kjær <bbk@math.ku.dk> @bbolvig Co-authored-by: Sina Hazratpour <sinahazratpour@gmail.com> @sinhp Co-authored-by: Nima Rasekh <rasekh@mpim-bonn.mpg.de> @nimarasekh - [x] depends on: #5808 We give a characterisation of effective epimorphic families in `Stonean` and deduce that `Stonean` is a precoherent category. This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.
Co-authored-by: Filippo A E Nuccio filippo.nuccio@univ-st-etienne.fr
Co-authored-by: Nikolas Kuhn nikolaskuhn@gmx.de
Co-authored-by: Adam Topaz topaz@ualberta.ca
This work was done during the 2023 Copenhagen masterclass on formalisation of condensed mathematics. Numerous participants contributed.