adding to someone else's PR

Stream: general

[Kevin Buzzard]

I have proved that the structure sheaf on an affine scheme is a sheaf of sets. I now need to prove it's a sheaf of commutative rings and we will have our first examples of schemes. However I need a little more transport of structure. In particular I need that the direct limit of commutative rings is a commutative ring. I asked Kenny if he'd done this and he said that he did a big direct limit PR recently but he only did rings, not commutative rings.

[Kenny Lau]

you can PR my PR

[Kevin Buzzard]

I can probably figure out how to add commutative rings myself, but this PR has not yet been accepted by mathlib and rather than having to wait for Mario twice

[Kevin Buzzard]

it seemed sensible just to add it now

[Kevin Buzzard]

How do I PR a PR?

[Kevin Buzzard]

Oh I see -- I send _you_ the PR?

[Kevin Buzzard]

So I fork your mathlib?

[Kenny Lau]

right

[Kevin Buzzard]

OK thanks

[Sebastian Ullrich]

You can directly push to PR branches of repositories you have push access to https://help.github.com/articles/committing-changes-to-a-pull-request-branch-created-from-a-fork/

[Kevin Buzzard]

I'm not sure I have push access to either mathlib or Kenny's fork of it

[Kevin Buzzard]

I can't fork Kenny's mathlib, github complains that I already have some other fork of mathlib

[Kevin Buzzard]

Kenny I've made my edits, I will just email them to you

[Kenny Lau]

ok

[Kevin Buzzard]

I added commutative rings