Andrew Yang

Results 88 comments of Andrew Yang

chore(Category/TopCat): cleanup

I removed the comments in `Topology/Sheaves/*` as the file is designed to have this instance on.

feat(AlgebraicGeometry/Limits): Coproducts of Schemes

I'll try out the approach Johan mentioned. `GlueData.mk₂` is definitely useful, but I don't think we should introduce `if then else` everywhere.

feat(AlgebraicGeometry/Limits): Coproducts of Schemes

After some more thought, I think `GlueData'` is only useful when `i = j` and `i =/= j` need different approaches, so maybe adding `i ≠ j` in the data...

Feat: add `PowerBasis.exists_sModEq`

Thanks! maintainer merge

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

Please merge master, thanks.

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

Thanks! maintainer merge

feat(RingTheory/Localization): localization of algebra maps and commutation with kernels

Sorry forgot about this PR. Please merge master in case the localization refactor causes some conflicts.

feat(RingTheory/Localization): localization of algebra maps and commutation with kernels

Thanks! maintainer merge

feat(CategoryTheory): localization of pretriangulated categories

Thanks! maintainer merge

feat(Algebra): define `PrimitiveIdempotents`

And I think (also judging from the "large-import" tag) this belongs to `Mathlib.Algebra.DirectSum.Idempotents` or something similar. Also please update the PR title so that it matches with the content.