Christian Merten

Results 23 comments of Christian Merten

feat: the equational criterion for flatness

> Hello, I managed to make `Algebra/Module/FinitePresentation.lean` fully universe polymorphic. This had the side effect of somehow breaking `RingTheory/Flat/EquationalCriterion.lean`, even though I didn't even touch that file. I think this...

feat: the equational criterion for flatness

> Hi, I'm sorry about the way I worded my comment earlier. I shouldn't be so dismissive about universe polymorphism; I now see it could very plausibly matter at some...

feat: the equational criterion for flatness

Apart from one open question above, I think this is good to go. Since the universe generalizations depend on #13149, we can merge this one as is and generalize after...

feat(CategoryTheory/Action): category of continuous actions

Thanks for the suggestions, I adapted them in the last commit.

feat(CategoryTheory/Action): category of continuous actions

> This design seems better to me as compared to #12878 I closed #12878 and adapted your suggestions.

feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups

bors r+

feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups

Thanks for the review @joelriou !

feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups

bors r+

feat(AlgebraicGeometry/Morphisms): stalkwise constructor and more API

> Please merge master, thanks. Done.

feat(CategoryTheory/Comma): limit properties of subcategories defined by morphism properties

Thanks for the reviews!