Zulip Chat Archive

Stream: maths

Topic: defining ideals


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 08:35):

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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 08:41):

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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 21 2019 at 08:46):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Feb 21 2019 at 08:48):

Or you can use span

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 21 2019 at 09:52):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Feb 21 2019 at 09:58):

Or do you have something else in mind?

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:00):

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

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:00):

But the point is that the user never finds that out

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:01):

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

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:01):

I'm talking about the definition of a valuation class

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:02):

val_class or wherever we want to call it

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:02):

We don't use quotients at all

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:03):

But we write all the API for quotients ourselves

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:03):

I'm on a phone

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:03):

But I'll try

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:06):

Sure

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:07):

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

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:07):

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

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:09):

Oh so it is.

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:09):

Bit it has more structure

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:09):

It has a topology etc

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 10:10):

So it might be a different thing

view this post on Zulip Johan Commelin (Feb 21 2019 at 10:11):

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

view this post on Zulip Kevin Buzzard (Feb 21 2019 at 15:07):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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