PRs forgotten for 2+ weeks

Stream: PR reviews

[Junyan Xu]

Let me :ping_pong: maintainers for the following PRs:

algebraic geometry:
#15934 : skyscraper presheaf and calculation of stalks (extensively reviewed by me)
#16083 : lemmas about rings graded by canonically ordered monoids (self-assigned to @Eric Wieser)
#15259 : the function from Spec to Proj restricted to basic open set (extensively reviewed by me, contains #16083)

topology:
#16210 (awaiting review) : split a pi type into a binary product at a coordinate, necessary for the homotopy (comm_)group PR (#15681, pending cleanup)

[Andrew Yang]

I also reviewed #15934 and it looks good to me as well.

[Kevin Buzzard]

Heh, we might be suffering from the CPP deadline! Which is on 21st Sept this year, my birthday. Good Lean things happen every year on my birthday -- this year I already know what it is, it's "maintainers stop being bogged down by having to write papers" :-)

[Kevin Buzzard]

Many thanks for flagging these PRs Junyan. It's great to see alg geom moving forwards (and thank you to both of you and @Jujian Zhang for moving it forwards!). I am running an undergraduate workshop next week and I was going to set alg geom as a possible project but I chickened out because I figured it was just too advanced for UGs.