defining ideals

Stream: maths

[Johan Commelin]

I've got a definition valuation.supp v : ideal R (and a proof that it is a prime ideal). There is also Spv R which is defined as

definition Spv := {ineq : R → R → Prop // ∃ (v : Valuation R), ∀ r s : R, v r ≤ v s ↔ ineq r s}

Now I can define Spv.supp ineq : ideal R as having carrier := {r | r ≤[v] 0}. I would then like to conclude that this is an ideal (and even prime) by saying that this is the same carrier as that of valuation.supp v where v is any valuation that I can choose out of the ∃ (v : ....) in the definition of Spv.

I think we currently don't really have an interface for this, is that right? So the cheapest way is to just reprove the properties zero, add, and smul. Or is there something I missed?

[Mario Carneiro]

IIRC, the reason Spv looks like that is to build a quotient over something that's hard to quotient

[Mario Carneiro]

so it should have the lemmas of a quotient, in this case quotient.ind

[Mario Carneiro]

Oh wait, you are defining a function Spv -> ideal R. That's a quotient lift

[Mario Carneiro]

You lift the function valuation.supp : valuation R -> ideal R, and prove that two valuations give the same ideal using ideal.ext

[Johan Commelin]

Yes, but I need supp before I can define the "canonical" lift.

[Johan Commelin]

In general, I think it makes sense that there is some sort of buddy to ideal.ext that allows you to prove that a set is an ideal if it is the same as the carrier of an existing ideal.

[Mario Carneiro]

One way you can construct this ideal is by taking the intersection of all ideals for various choices of v

[Mario Carneiro]

Or you can use span

[Mario Carneiro]

prove that a set is an ideal if it is the same as the carrier of an existing ideal

You don't "prove that a set is an ideal". You construct an ideal with the same carrier as the set. But if you do that, then you will notice that the new ideal is equal to the ideal you started with, so it was a pointless endeavor, unless you care about defeq

[Kevin Buzzard]

Johan, my thoughts on this are that we need to make a completely new file valuation_class.lean containing the API for an equivalence class of valuations, and writing all of the definitions for quotients for this class, and I know how to do this. We should do all of this first before even thinking about Spv. I would do it but I'm travelling right now, I'm preaching the gospel in Portugal at an undergraduate computer science conference.

[Kevin Buzzard]

But this new definition and its API are the next thing to do in the perfectoid project

[Kevin Buzzard]

Look at finset.lean. This is a weird definition, at first glance. No user ever wants to prove anything about finsets by starting with the line unfold finset -- it would be a disaster. You just use all the definitions in the 1700 line API and never even think about how a finset is actually implemented internally. We have to do just the same thing with equivalence classes of valuations first before we can get anywhere. Our internal implementation is as an inequality but we have to make it so that the user never has to think about this or even know this. Then we'll be ready for Spv

[Johan Commelin]

@Kevin Buzzard Yes, I agree. I'm slowly moving towards that goal.

[Kevin Buzzard]

So I think the answer to your question is that we need to write the analogues of quotient.lift and quotient.out etc etc and then use these general tools to define the functions you want. At least I think that's the answer

[Johan Commelin]

Ok, so one question: what is the definition of valuation_class? Is it an honest Lean quotient (with the disadvantage that it lives an a universe that is to big). And then afterwards, we build an equiv with Spv that lives in the right universe but is a fake quotient.

[Johan Commelin]

Or do you have something else in mind?

[Kevin Buzzard]

The definition is that it's an inequality coming from a valuation

[Kevin Buzzard]

But the point is that the user never finds that out

[Kevin Buzzard]

And by "the user" I mean "the person writing Spv.lean"

[Kevin Buzzard]

I'm talking about the definition of a valuation class

[Kevin Buzzard]

val_class or wherever we want to call it

[Kevin Buzzard]

We don't use quotients at all

[Johan Commelin]

Ok, I'm confused. I know you are busy. But could you give me about 4 lines of Lean code.
The definition of val_class R, and the definition of Spv R.

[Kevin Buzzard]

But we write all the API for quotients ourselves

[Kevin Buzzard]

I'm on a phone

[Kevin Buzzard]

But I'll try

[Kevin Buzzard]

A term of type valclass R is a relation ineq plus a proof that there exists a valuation taking values in a group in the same universe as R such that blah

[Kevin Buzzard]

The mk function takes a valuation taking values in any universe and gives a term of type valclass

[Johan Commelin]

Sure

[Kevin Buzzard]

Because we want the user to not know what's going on

[Johan Commelin]

And what is Spv R? (Because currently it has exactly the definition you just gave.)

[Kevin Buzzard]

Oh so it is.

[Kevin Buzzard]

Bit it has more structure

[Kevin Buzzard]

It has a topology etc

[Kevin Buzzard]

So it might be a different thing

[Johan Commelin]

Yeah, but we can bolt on the topology afterwards... that's just a type class instance

[Kevin Buzzard]

Is that the right way to think about it? I'm not sure

[Kevin Buzzard]

I guess I was envisaging defining Spv R to be the type of equivalence classes of valuations on R, and putting the topology on Spv R. Maybe that's insane? I don't know. We have option X and with_zero X right?

[Kevin Buzzard]

If you want to make Spv the inequalities (which is what we have now) then you will want to look at all the functions with prefix quot and make versions of them all in the Spv namespace. Then you'll have an answer to the ideal question

[Kevin Buzzard]

But I was envisaging making them all part of the val_class namespace and then building Spv with its topology on top