## Stream: maths

### Topic: defining ideals

#### Johan Commelin (Feb 21 2019 at 08:32):

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 (Feb 21 2019 at 08:34):

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

#### Mario Carneiro (Feb 21 2019 at 08:35):

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

#### Mario Carneiro (Feb 21 2019 at 08:41):

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

#### Mario Carneiro (Feb 21 2019 at 08:43):

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

#### Johan Commelin (Feb 21 2019 at 08:46):

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

#### Johan Commelin (Feb 21 2019 at 08:47):

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 (Feb 21 2019 at 08:48):

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

#### Mario Carneiro (Feb 21 2019 at 08:48):

Or you can use span

#### Mario Carneiro (Feb 21 2019 at 08:50):

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 (Feb 21 2019 at 09:04):

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 (Feb 21 2019 at 09:05):

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

#### Kevin Buzzard (Feb 21 2019 at 09:10):

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 (Feb 21 2019 at 09:52):

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

#### Kevin Buzzard (Feb 21 2019 at 09:57):

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 (Feb 21 2019 at 09:58):

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 (Feb 21 2019 at 09:58):

Or do you have something else in mind?

#### Kevin Buzzard (Feb 21 2019 at 10:00):

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

#### Kevin Buzzard (Feb 21 2019 at 10:00):

But the point is that the user never finds that out

#### Kevin Buzzard (Feb 21 2019 at 10:01):

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

#### Kevin Buzzard (Feb 21 2019 at 10:01):

I'm talking about the definition of a valuation class

#### Kevin Buzzard (Feb 21 2019 at 10:02):

val_class or wherever we want to call it

#### Kevin Buzzard (Feb 21 2019 at 10:02):

We don't use quotients at all

#### Johan Commelin (Feb 21 2019 at 10:03):

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 (Feb 21 2019 at 10:03):

But we write all the API for quotients ourselves

I'm on a phone

But I'll try

#### Kevin Buzzard (Feb 21 2019 at 10:06):

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 (Feb 21 2019 at 10:06):

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

Sure

#### Kevin Buzzard (Feb 21 2019 at 10:07):

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

#### Johan Commelin (Feb 21 2019 at 10:07):

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

Oh so it is.

#### Kevin Buzzard (Feb 21 2019 at 10:09):

Bit it has more structure

#### Kevin Buzzard (Feb 21 2019 at 10:09):

It has a topology etc

#### Kevin Buzzard (Feb 21 2019 at 10:10):

So it might be a different thing

#### Johan Commelin (Feb 21 2019 at 10:11):

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

#### Kevin Buzzard (Feb 21 2019 at 15:07):

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

#### Kevin Buzzard (Feb 21 2019 at 15:14):

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 (Feb 21 2019 at 15:17):

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 (Feb 21 2019 at 15:18):

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

Last updated: May 12 2021 at 07:17 UTC