localisation of rings

Stream: maths

[Kevin Buzzard]

I've had enough of the fascinating localisation topic being hidden within this thread so I'm moving some of it here.

Summary: @Neil Strickland wrote a predicate is_localization A S B f where A and B are rings, S is a submonoid of A, f : A -> B is a ring hom, and the predicate is true iff B is isomorphic to A[1/S] and the triangle involving f commutes. Kenny then Kenny'd it and I think there is still no PR. Neil wrote down an excellent-looking list of tests which as far as I know nobody has yet tried. @Ramon Fernandez Mir did you get as far as seeing whether this ugly part of the schemes project was made any simpler using this approach?

Johan is asking about localisations in #481 and the stuff above might make us rethink the entire approach.

[Johan Commelin]

I was just thinking about this... does S even have to be a submonoid? Or can it be any set?

[Kevin Buzzard]

I talked to Kenny about this, and Neil mentioned something too. Neil pointed out that for log geometry you have a morphism from a monoid into a ring, but there you really do need monoids. I was forever needing stuff like A[1/f][1/g]=A[1/fg] and for that it would have been much easier to have subsets of A. @Kenny Lau then told me that if you don't use all the monoid but instead just the subset then there would be problems with constructiveness or something -- apparently just because you know all the inverses of f(s) for all s in some generating set T doesn't mean you know all the inverses of all the elements of T? I didn't really understand what he was saying but he knows a darn sight more about this sort of stuff than I do.

I talked about this with Ramon and we came up with the idea of leaving the predicate as it is, together with its proof that it satisfies the universal property, but then writing another predicate on top, defining is_localisation' A T B f to be is_localisation A <T> B f or whatever, and working with that. This way we don't completely rip up Neil's interface and then realise that we needed it all along, but we can probably also prove the lemmas which we need about A[1/f][1/g]=A[1/fg] relatively painlessly. Kenny also remarked that A[1/S] was equal to A[1/U] where U is the "saturation" of S, which I quickly discovered did not mean the u such that u^n in S for some n>=1 but the u which divide an element of S.

I think that's everything I know. I've not had a chance to think about this stuff recently. Maybe tomorrow I'll work with Ramon on it.

[Kevin Buzzard]

I guess one big question is: is Neil or Kenny actually going to PR this predicate? It seemed to me that after we had the universal property, which we did have, we had enough to make it worth PR'ing.

[Kevin Buzzard]

Another question is: if [is_ring_hom f] from A to B, then how do I get module A B? Type class inference won't work, right?

[Kevin Buzzard]

Is the instance there?

[Chris Hughes]

The def is there in Kenny's recent algebra PR somewhere.

[Kevin Buzzard]

You mean his localisation PR or another one?

[Chris Hughes]

Another one

[Chris Hughes]

It's merged

[Ramon Fernandez Mir]

@Kevin Buzzard I haven't got there yet. But we can start working on that today, I think that's one of the trickiest bits. I'm glad this has been moved from "cardinality of integers modulo n" haha

[Ramon Fernandez Mir]

Also, the PR which is currently open for localisation stuff has nothing to do with @Neil Strickland 's code right?

[Johan Commelin]

Yes, that's right. It's an older PR by Kenny.

[Johan Commelin]

Probably somewhat orthogonal. But I think the entire file would need a refactor if we implement Neil's approach.

[Kevin Buzzard]

Probably somewhat orthogonal. But I think the entire file would need a refactor if we implement Neil's approach.

That is not so clear. Neil's approach gives what is hopefully a simple way of checking to see if a ring that we have lying around already happens to be the localisation of A at S. You still have to actually construct the localisation as in the PR if you don't have one lying around already.

The difficulty comes when you have a lemma about A[1/f][1/g] (built using Kenny's explicit construction) and you want to apply it to A[1/fg] (built using Kenny's explicit construction). In the schemes project I had to prove that A[1/f][1/g] had the universal property which classified A[1/fg] and could from that build a map from A[1/f][1/g] to A[1/fg] and prove that it was the unique A-algebra morphism, again using the universal property. With Neil's approach the hope (although nobody has checked yet, as far as I know, however this might change today) is that I can instead show that A[1/f][1/g] satisfies Neil's predicate for A and <fg>, which looks much much easier to do, and then get the equiv + uniqueness for free all from the API.

[Kevin Buzzard]

Kenny's PR is a refactoring based on a more mature understanding of definitional equality. He wrote his localisation code when he was very much a Lean beginner -- over a year ago. Now he's fixing it up, that's the PR (removing lam <x,y> and replacing with lam a, and then changing x to a.1 etc)

[Kenny Lau]

example {R : Type*} [comm_ring R] (e : R) (he : e * e = e) : localization_alt.is_localization (powers e) (ideal.quotient.mk (ideal.span {1-e})) :=
begin
  have H1 : ideal.quotient.mk (ideal.span {1 - e}) e = 1,
  { exact eq.symm (ideal.quotient.eq.2 $ ideal.subset_span $ or.inl rfl) },
  have H2 : (1 - e) * e = 0,
  { rw [sub_mul, he, one_mul, sub_self] },
  refine ⟨_, _, _⟩,
  { rintros ⟨_, n, rfl⟩, use 1,
    change ideal.quotient.mk _ (e^n * 1) = _,
    rw [mul_one, is_semiring_hom.map_pow (ideal.quotient.mk (ideal.span {1-e})) e n, H1, one_pow] },
  { rintro ⟨x⟩, use (1,x), exact one_mul _ },
  { ext x, split; intro hx,
    { replace hx := ideal.quotient.eq_zero_iff_mem.1 hx,
      replace hx := ideal.mem_span_singleton'.1 hx,
      refine ⟨⟨(x, ⟨e, 1, pow_one e⟩), _⟩, rfl⟩,
      cases hx with y hx, change x * e = 0, rw [← hx, mul_assoc, H2, mul_zero] },
    { rcases hx with ⟨⟨⟨x, ⟨_, n, rfl⟩⟩, hx⟩, rfl⟩, change x * e^n = 0 at hx,
      apply ideal.quotient.eq_zero_iff_mem.2,
      apply ideal.mem_span_singleton'.2,
      change ∃ a, a * (1-e) = x, induction n with n ih generalizing x,
      { rw [pow_zero, mul_one] at hx, subst hx, use 0, rw zero_mul },
      rw [pow_succ, ← mul_assoc] at hx, cases ih _ hx with y hy,
      use x + y, rw [add_mul, hy, ← mul_add, sub_add_cancel, mul_one] } },
end

[Kenny Lau]

unit test of localization_alt @Neil Strickland

[Kenny Lau]

A[1/e] = A/(1-e)

[Kevin Buzzard]

@Ramon Fernandez Mir just posted me his proof that A[1/f][1/g] has the universal property of A[1/fg]. Ramon -- post it here!

@Neil Strickland -- are you going to PR your predicate? @Johan Commelin was complaining yesterday that some work we're doing in the perfectoid project was clunky because our localisation API was not as good as it could be. I think both your predicate and Kenny's #481 (@Chris Hughes did you see that Kenny fixed the issues with all the @s?) would be of much use to us; we will shortly be moving on to defining the presheaf on an adic space and this is a localisation followed by a completion so we will be stress testing both the localisation API and Patrick's work on completions of topological rings.

[Chris Hughes]

Are you planning on doing the data containing version of is_localisation, or are you making everything noncomputable.

[Kevin Buzzard]

I cannot make any coherent response to this comment myself.

[Kevin Buzzard]

@Kenny Lau do you have a reason for choosing one way or another which would convince me?

[Kenny Lau]

no

[Johan Commelin]

I don't think it's a bad idea to carry data around.

[Johan Commelin]

I think typically in these "categorical" situations it makes life easier.

[Kevin Buzzard]

I would trust Johan's judgement -- we will be seriously using this stuff soon enough and perhaps things will be clearer then, but Johan has already started to use it.

[Ramon Fernandez Mir]

Here's what I have done: https://gist.github.com/ramonfmir/976ce8abd823a08a63560393d538f5d6

[Ramon Fernandez Mir]

The idea is to prove is_localisation R[1/a][1/b] <ab>, where R[1/a][1/b] is the explicit construction.

[Neil Strickland]

I am happy to PR anything that people think is worthwhile. However, I am not really up to speed on either the whole git framework or the specific conventions of mathlib. I know that https://github.com/leanprover-community/mathlib/blob/master/docs/howto-contribute.md exists but have not digested it yet. If someone wants to make a more specific suggestion about exactly what I should do, then I am happy to follow it. (But I probably won't be able to respond to anything until this evening or tomorrow.)

[Kevin Buzzard]

Would you be offended if someone else PR'ed your work?

[Kevin Buzzard]

(after getting it into the required state for mathlib?)

[Kevin Buzzard]

As you can see, the community has done 2/3 of your challenge tests. Just the Z[1/p] one to go. And Reid Barton suggested another test -- localisation of localisation is localisation (for more general monoids, not just <f> and <g>)

[Reid Barton]

@Kenny Lau do you have a reason for choosing one way or another which would not convince @Kevin Buzzard?

[Kevin Buzzard]

I'm super-motivated because I think that the perfectoid project is almost at the stage where we want to really push the localisation API and I am sure, based on my experience with schemes, that your predicate will play a valuable role.

[Neil Strickland]

That's fine by me. I hope that things will be left in a state where I can easily see how I could have done it myself.

[Kenny Lau]

@Kenny Lau do you have a reason for choosing one way or another which would not convince @Kevin Buzzard?

no

[Kevin Buzzard]

This surprises me