Zulip Chat Archive

Stream: maths

Topic: DVRs


view this post on Zulip Kevin Buzzard (Feb 13 2020 at 19:42):

class discrete_valuation_ring (R : Type*) extends principal_ideal_domain R :=
(unique_nonzero_max_ideal : ∃! P : ideal R, P.is_prime  P  0)

@Johan Commelin what do you think?

view this post on Zulip Johan Commelin (Feb 13 2020 at 19:46):

Well, we already have local_ring

view this post on Zulip Johan Commelin (Feb 13 2020 at 19:46):

So maybe you should extend that

view this post on Zulip Johan Commelin (Feb 13 2020 at 19:46):

and then add one extra condition saying that it's not a field

view this post on Zulip Kevin Buzzard (Feb 13 2020 at 19:48):

but a general local ring isn't a PID so I need to add that somehow, right?

view this post on Zulip Johan Commelin (Feb 13 2020 at 19:49):

You are already extending that, right?

view this post on Zulip Johan Commelin (Feb 13 2020 at 19:49):

I meant, in addition, extend local ring

view this post on Zulip Johan Commelin (Feb 13 2020 at 19:51):

I wonder whether we'll be happy with [dvr R] and [pid R], etc... Or that we'd rather have [comm_ring R] [is_dvr R] and [comm_ring R] [is_pid R] etc...

view this post on Zulip Johan Commelin (Feb 13 2020 at 19:51):

The first version has more chances to lead to diamonds, I think

view this post on Zulip Kevin Buzzard (Feb 13 2020 at 19:52):

I never know if I'm allowed to extend PID and local ring because perhaps I just defined two different multiplications or something? I really have no understanding of this stuff and don't know a place where it's all written up coherently. I occasionally half-understand it for a while and then I just forget it all again.

view this post on Zulip Johan Commelin (Feb 13 2020 at 19:54):

Aha, I think it's fine, but maybe you need to switch on the old_structure_cmd

view this post on Zulip Kevin Buzzard (Feb 13 2020 at 20:10):

set_option old_structure_cmd true

class discrete_valuation_ring (R : Type*) extends principal_ideal_domain R,
  local_ring R :=
(pseudouniformiser :  a : R, a  0  ¬ is_unit a)

view this post on Zulip Johan Commelin (Feb 13 2020 at 20:16):

Yeah, that seems fine. Although I would maybe not call the condition pseudouniformiser

view this post on Zulip Johan Commelin (Feb 13 2020 at 20:16):

exists_nonzero_nonunit?

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 12:56):

Thinking about the proof that given a DVR you actually get a valuation, there's a slight stumbling block: I want to use enat and then do something like R →*+ enat which should be a map from the DVR R to enat which is a map of monoids, but the problem is that I want to think of R as a multiplicative monoid and enat as an additive monoid: it doesn't seem like →*+ exists. One other option is to use multiplicative valuations landing in R0\mathbb{R}_{\geq 0} but then it's not really clear where a uniformizer is supposed to go: there are infinitely many choices, none of which really stand out in general.

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 13:02):

Is there some systematic way to add in things like →*+?

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 13:38):

Alternatively, \bbZ and \bbN have has_le, but multiplicative \bbZ doesn't seem to preserve this, and I'm not sure whether with_zero defines a new ordering...

view this post on Zulip Kenny Lau (Apr 26 2020 at 13:39):

@Ashwin Iyengar they used valuations in the perfectoid project which you might find helpful

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 13:44):

Yeah I guess what I want to use is linear_ordered_comm_group_with_zero.lean then: @Kevin Buzzard is this destined for mathlib?

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 13:45):

But maybe this should be rewritten replacing 0 with to avoid confusion with 0 in the integers?

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 13:58):

I guess I can achieve what I want if I have linear_ordered_comm_group_with_zero.lean, and some way to distinguish between the natural number 0 and the adjoined 0

view this post on Zulip Johan Commelin (Apr 26 2020 at 14:57):

Ashwin Iyengar said:

Yeah I guess what I want to use is linear_ordered_comm_group_with_zero.lean then: Kevin Buzzard is this destined for mathlib?

I think this can be PR'd. All prerequisites are now in mathlib, if I'm not mistaken. Note that it only works in a multiplicative setting though... so it doesn't yet solve your problem.

I think there are two questions that need to be answered:

  1. Should DVR's use multiplicative or additive valuations?

  2. What ever the answer is to (1): what should the target type be of discrete valuations?

Note that we could also opt for a "heretical" approach, in which we take a discrete additive valuation with target type the integers, and we require val 0 = 0, instead of val 0 = infty. This would create it's own problems, but it also solves a lot...

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 15:27):

Additive is what is usually done, but if we want to do multiplicative instead, one option for the target would be to just use a free group on one generator (written multiplicatively), define the obvious ordering on it, and then use your

/-- Adjoining a zero element to a linearly ordered commutative group
gives a linearly ordered commutative group with zero.-/
instance (α : Type*) [linear_ordered_comm_group α] [decidable_eq α] :
  linear_ordered_comm_group_with_zero (with_zero α) :=```

I'll try this for now.

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 16:25):

Later on it might be convenient to have valuations taking values in a discrete subgroup of the rationals

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 16:26):

I think Johan is the expert in valuations now, there has been lot of movement since that valuation file was originally written, especially with group_with_zero

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 16:29):

We could do something like

def to_discrete_valuation (R : Type u) [discrete_valuation_ring R]
(G : Type v) [comm_group G] (g : G) (cyclic : G = span {g}) :
discrete_valuation R G g :=

maybe, and have the discrete valuation take values in an arbitrary infinite cyclic group... oh but I'm missing a proof that it's infinite

view this post on Zulip Johan Commelin (Apr 26 2020 at 16:33):

An alternative is to use the general valuations as found in the perfectoid project, and define a predicate on those, saying that the valuation is discrete.

view this post on Zulip Johan Commelin (Apr 26 2020 at 16:34):

Do you want discrete_valuation_ring R to be a Prop or will it record data (say a distinguished uniformiser...)?

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 16:47):

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R :=
(prime_ideal' : ideal R)
(primality : prime_ideal'.is_prime)
(is_nonzero : prime_ideal'  )
(unique_nonzero_prime_ideal :  P : ideal R, P.is_prime  P =   P = prime_ideal')

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 16:47):

so it records some data

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 16:48):

a PID with a unique nonzero prime ideal

view this post on Zulip Johan Commelin (Apr 26 2020 at 16:50):

Ok, I see. But it is a subsingleton. That seems like a fine definition

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 16:50):

Then we construct a valuation basically by using the UFD structure and the fact that prime elements are uniformizers

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:01):

In the perfectoid project we also had the notion of a valued_ring, which was a class that registered a (multiplicative) valuation on the ring.

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:02):

One could have an is_discrete predicate on a valuation in the sense of Huber and a construction which goes from this to the Z-valued valuation. But I don't think it matters that traditionally the group law on Z with 0 is addition -- why not use multiplicative Z with 0?

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:02):

We might want to have two classes discrete_valuation_ring R, like you propose, and discretely_valued_ring R, for rings like Z_p that have a canonical valuation.

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:03):

What structure do people use on Z with +infinity? Add, max, probably never multiplication, but external multiplication by Z yes. But we have all this on a group with 0

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:03):

I'm still upset that it seems really painful to move back and forth between multiplicative and additive valuations...

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:03):

So why not just bite the bullet and never use additive valuations?

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:04):

It's either that or make add_group_with_zero

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:04):

Because sometimes it's really nice and intuitive to reason about int

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:04):

Or with infinity or whatever

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:04):

Kevin Buzzard said:

It's either that or make add_group_with_zero

add_group_with_infty

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:04):

But I don't think the to_additive machinery is built with such translations in mind...

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:05):

But I don't think the target Z really is a Z. It's certainly not the ring Z. It's the additive group Z with an occasional infinity

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:05):

And an action of Z which is either a smul or a gpow

view this post on Zulip Kevin Buzzard (Apr 26 2020 at 17:07):

I don't see why we need to introduce the concept of an additive valuation at all. Just because it's in maths in some superficial way doesn't mean we need it. Or we could have it in this one off case. What did Rob use for p-adics?

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:07):

norms...

view this post on Zulip Ashwin Iyengar (Apr 26 2020 at 17:08):

I would be happy with multiplicative Z\mathbb{Z} with an added 0 element, but won't this cause notational trouble because you have the integer 0 and then the added 0?

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:09):

There are ways around that.

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:10):

We could define free_group, or something like that.

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:10):

As in, don't actually use int, but use a different type.

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:12):

Johan Commelin said:

As in, don't actually use int, but use a different type.

If you want, we could give it some names like discrete_valuation.target_type, or something fancier...

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:14):

But it would be best to already include the extra 0 element in the definition of this type. You don't want to work with with_zero foo all the time, even though in "normal" maths we keep up that facade.

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:14):

We did that for a long time in the perfectoid project, but it just became too painful.

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:15):

Still, I wonder if you should settle on 1 target type. It might be better to characterise what it means to be a discrete valuation, as I proposed above.

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:15):

Because otherwise you will regret it once you get a DVR with a different target type.

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:16):

(Say some subset of the reals)

view this post on Zulip Johan Commelin (Apr 26 2020 at 17:16):

We should really work to get the definition of a general valuation into mathlib

view this post on Zulip Johan Commelin (Apr 27 2020 at 05:45):

@Kevin Buzzard I think that sometimes it's useful to view padic_val_int as an actual integer, don't you think? But nevertheless we can probably get away with using multiplicative valuations as the default.

@Ashwin Iyengar I'm starting to think that we should just hurry up with PR'ing the basics of valuations from the perfectoid project. Stuff like equivalence of valuations etc would also be useful to you. And it would be silly to have to do all of that again.

Maybe we need a class like normed_valued_ring R that can be used for examples like Z_p, and will register both a norm and a valuation, and an axiom that claims the two are the same thing.

view this post on Zulip Ashwin Iyengar (Apr 27 2020 at 06:55):

Yeah if i have access to the perfectoid project stuff then I'm sure I can just go from there, but no rush

view this post on Zulip Johan Commelin (Apr 27 2020 at 07:45):

I'll try to prioritise these PRs

view this post on Zulip Ashvni Narayanan (Jun 11 2020 at 12:11):

I am trying to state the following lemma

variables (R : Type u) [discrete_valuation_ring R ]
open discrete_valuation_ring
def uniformizers : set R := { π | ideal.span ({π} :set R ) = local_ring.nonunits_ideal R }

lemma element_of_dvr {r π : R} (nonzero: r  0) (unif: π  uniformizers) : ∃! n :  , associated r π^n :=

and I get two errors :

failed to synthesize type class instance for
R : Type u,
_inst_1 : discrete_valuation_ring R,
r π : R,
nonzero : r  0
 has_mem R (Π (R : Type ?) [_inst_1 : discrete_valuation_ring R], set R)  -- regarding the uniformizer

failed to synthesize type class instance for
R : Type u,
_inst_1 : discrete_valuation_ring R,
r π : R,
nonzero : r  0,
unif : π  uniformizers,
n : 
 has_pow Prop   -- regarding \pi ^n

I understand why the second error occurs, but don't know the right has_pow code to fix it. I don't know what causes the first error. Any help is appreciated, thanks!

view this post on Zulip Johan Commelin (Jun 11 2020 at 12:19):

@Ashvni Narayanan I think it might be better to write def is_uniformizer (\pi : R) := ...

view this post on Zulip Johan Commelin (Jun 11 2020 at 12:20):

You usually don't want to reason about the set of all uniformizers, just about one uniformizer.

view this post on Zulip Johan Commelin (Jun 11 2020 at 12:20):

For the second error: it's trying to raise associated r \pi to the power n. That's not what you mean. So put parens around \pi ^ n :wink:

view this post on Zulip Ashvni Narayanan (Jun 11 2020 at 13:59):

I see! That makes sense.

def is_uniformizer (π : R) := ideal.span ({π} :set R ) = local_ring.nonunits_ideal R

lemma element_of_dvr {r π : R} (nonzero: r  0) (unif : is_uniformizer π ) : ∃! n :  , associated r (π^n) :=

shows the error

type mismatch at application
  is_uniformizer π
term
  π
has type
  R : Type u
but is expected to have type
  Type ? : Type (?+1)

Did I end up defining is_uniformizer as a function which gives output \pi?

view this post on Zulip Johan Commelin (Jun 11 2020 at 14:00):

No, I guess that you have variable (R : Type*) somewhere above this definition.

view this post on Zulip Johan Commelin (Jun 11 2020 at 14:00):

That makes R an explicit variable of is_uniformizer.

view this post on Zulip Johan Commelin (Jun 11 2020 at 14:01):

So you have to type is_uniformizer R \pi, or you have to change it to variable {R : Type*}

view this post on Zulip Johan Commelin (Jun 11 2020 at 14:02):

@Ashvni Narayanan Btw, about element_of_dvr... this is of course a useful statement. But don't you want the slightly stronger statement that says that there is also a unique unit such that x = u * pi ^ n

view this post on Zulip Ashvni Narayanan (Jun 11 2020 at 14:09):

Yes, it might be needed for the well-definedness of the associated valuation. I will add it, thank you!

view this post on Zulip Ashvni Narayanan (Jun 13 2020 at 11:41):

class discrete_valuation_ring (R : Type u) extends local_ring R :=
(non_field : local_ring.nonunits_ideal R   )
(principal :  (S : ideal R), S.is_principal)

structure discrete_valuation_ring.discrete_valuation (R : Type u) [discrete_valuation_ring R] extends R →*  :=

(map_top' : to_fun 0 = 1)

(map_add_leq' :  x y, to_fun (x + y)  max (to_fun x) (to_fun y))

variables {R : Type u} [discrete_valuation_ring R ]
open discrete_valuation_ring
def is_uniformizer (π : R) := ideal.span ({π} :set R ) = local_ring.nonunits_ideal R

lemma element_of_dvr {r π : R} (nonzero: r  0) (non_unit : r  local_ring.nonunits_ideal R) (unif : is_uniformizer π ) : ∃! n :  , associated r (π^n) :=

begin
rw submodule.is_principal.mem_iff_generator_dvd at non_unit,

The last line gives me the error,

invalid rewrite tactic, failed to synthesize type class instance

I realise why the rw statement is problematic, how can I fix it?

view this post on Zulip Johan Commelin (Jun 13 2020 at 11:43):

@Ashvni Narayanan There is already principal_ideal_domain R, you can also extend that. (That way, every DVR is automatically a PID in lean)

view this post on Zulip Johan Commelin (Jun 13 2020 at 11:46):

also, your definition of discrete valuation seems to mix the additive and multiplicative points of view.

view this post on Zulip Ashvni Narayanan (Jun 13 2020 at 11:46):

I had tried that earlier,

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R, local_ring R :=
(non_field : local_ring.nonunits_ideal R   )

gives the error

invalid 'structure' header, field 'add' from 'local_ring' has already been declared

view this post on Zulip Johan Commelin (Jun 13 2020 at 11:47):

Aah... right. The solution is

set_option old_structure_cmd true

That will merge the duplicate fields

view this post on Zulip Ashvni Narayanan (Jun 13 2020 at 12:00):

That does it! The invalid rewrite tactic error stays, though..

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:13):

@Chris Hughes Should submodule.is_prinicipal be a class?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:16):

type mismatch at application
  principal_ideal_domain.principal (nonunits_ideal R)
term
  nonunits_ideal R
has type
  @ideal R (@to_comm_ring R (@to_local_ring R _inst_1))
but is expected to have type
  @ideal R
    (@integral_domain.to_comm_ring R
       (@principal_ideal_domain.to_integral_domain R (@to_principal_ideal_domain R _inst_1)))

With the following code

import ring_theory.principal_ideal_domain

set_option old_structure_cmd true

universe variable u

class discrete_valuation_ring (R : Type u) extends local_ring R, principal_ideal_domain R :=
(non_field : local_ring.nonunits_ideal R  )

variables {R : Type u} [discrete_valuation_ring R]
open discrete_valuation_ring
open local_ring

def is_uniformizer (π : R) := ideal.span ({π} :set R ) = local_ring.nonunits_ideal R

lemma element_of_dvr {r π : R} (nonzero: r  0)
  (non_unit : r  nonunits_ideal R) (unif : is_uniformizer π) :
  ∃! n :  , associated r (π^n) :=
begin
  have := @principal_ideal_domain.principal R _ (nonunits_ideal R), -- error is here
  rw submodule.is_principal.mem_iff_generator_dvd (nonunits_ideal R) at non_unit,
end

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:16):

This is not nice

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 12:17):

structure discrete_valuation_ring.discrete_valuation (R : Type*) [discrete_valuation_ring R] extends R →*  :=
(map_top' : to_fun 0 = 1)
(map_add_leq' :  x y, to_fun (x + y)  max (to_fun x) (to_fun y))

This doesn't look right. Are we supposed to be modelling the p-adic valuation or the p-adic norm? If the valuation then the valuation of 0 should be +infty. If the norm then the norm of pi will be between 0 and 1, and so which integer will you use?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:17):

I think we should ignore that code for now...

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:17):

But I agree with the point

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:18):

I've never really used [principal_ideal_domain R] before... I'm not sure if it's in optimal form.

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:23):

@Mario Carneiro what's going on here?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:24):

I'm starting to think more and more that we should just go for

variables {R : Type} [comm_ring R] [is_local_ring R]
-- or
variables {R : Type} [comm_ring R] [is_integral_domain R]
-- or
variables {R : Type} [comm_ring R] [is_principal_ideal_domain R]
-- etc

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:28):

what's the question?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:29):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/DVRs/near/200763565

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:29):

Is it about unbundling ring classes into mixins?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:29):

It's about inferred instances not being defeq

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:30):

aha, this came up not too long ago

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:31):

ooh, is this the "bug" that Kenny found?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:31):

With alternating old and new structures?

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:31):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/old_structure_cmd/near/199101684

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:32):

It's actually a kind of fundamental problem

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:33):

One solution would be to always explode all instances into their constructors (which I think happens behind the scenes a lot anyway) but this seems pretty expensive

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:34):

it also doesn't work for instances that are variables

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:36):

So... how should we turn this into working code?

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:38):

I suspect that sprinkling some old structures around will fix the problem

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:39):

But new structure were introduced for a reason, right?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:39):

It seems like now everything has to become an old structure...

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:39):

And the hierarchy is far from finished.

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:40):

complete_discrete_valuation_ring will throw some topology into the mix, etc...

view this post on Zulip Sebastien Gouezel (Jun 13 2020 at 12:41):

Would it be really bad to have a spine for the hierarchy which wouldn't be too big (I mean, semigroup -> monoid -> group -> ring -> comm_ring -> field, add or subtract a few things) and mixins for additional properties like we do for topological spaces?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:41):

I think that would be a good idea.

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:44):

This is one reason why I would like to have an interactive graph of the hierarchy...

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:44):

Oh wait, discrete_valuation_ring is actually broken

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:44):

check out the constructor:

discrete_valuation_ring.mk : Π {R : Type u} [_to_comm_ring : comm_ring R] [_to_nonzero : nonzero R]
(is_local :  (a : R), is_unit a  is_unit (1 - a)) [_to_integral_domain : integral_domain R],
  ( (S : ideal R), submodule.is_principal S)  nonunits_ideal R    discrete_valuation_ring R

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:45):

note the separate appearance of comm_ring R and integral_domain R

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:45):

the unification problem fails because it's actually false

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:46):

Mario Carneiro said:

note the separate appearance of comm_ring R and integral_domain R

How did that happen?

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:46):

the double extends

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:47):

Shouldn't old_structure_cmd take care of that?

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:47):

As was noted previously, old_structure_cmd was not written with extensions of new structures in mind

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 12:47):

Which structure isn't old?

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:47):

Both, I think

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:48):

local_ring and principal_ideal_domain are both new structures

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:48):

you can tell because if you #print them you don't get a mile long list of fields

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:49):

Which of course they shouldn't have been, because they extend old structures, and they aren't the top of the hierarchy

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:49):

I think this could be addressed by fixing old structures extending new structures

view this post on Zulip Mario Carneiro (Jun 13 2020 at 12:49):

the compilation here is pretty unquestionably wrong

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 12:54):

What is the Lean 3 idiomatic way to proceed?

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 12:55):

Is there any harm in just making them old structures?

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:56):

I think that was bad for performance... hence new structures were introduced.

view this post on Zulip Johan Commelin (Jun 13 2020 at 12:56):

Mario wants to fix lean instead.

view this post on Zulip Mario Carneiro (Jun 13 2020 at 13:00):

I am not convinced by the performance argument that was the original motivation for new structures. The performance in question is the time it takes to elaborate a structure definition, which is not the bottleneck in mathlib at all

view this post on Zulip Mario Carneiro (Jun 13 2020 at 13:01):

possibly also structure literals are affected

view this post on Zulip Mario Carneiro (Jun 13 2020 at 13:02):

I just tried making local_ring an old structure and I got some odd errors. It may not be a drop in replacement

view this post on Zulip Mario Carneiro (Jun 13 2020 at 13:03):

the old structure command doesn't like to extend things in a dependent sequence

view this post on Zulip Mario Carneiro (Jun 13 2020 at 13:04):

that is, class foo X extends bar X, @baz X <typeclass problem involving _inst_bar_X> fails

view this post on Zulip Kevin Buzzard (Jun 13 2020 at 14:33):

So what do we do?

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 23:53):

I want a working definition of discrete_valuation_ring (DVR) and now I'm entering a period in my life where I should have a lot more time for Lean; it would be nice to get this moving again. Recall that the issue is that the definition should be this:

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R, local_ring R :=
(non_field : local_ring.nonunits_ideal R   )

but principal_ideal_domain (PID) and local_ring have overlapping fields, and the obvious fix of using the old structure command doesn't work because neither PID or local_ring were made with the old structure command.

Approach 1: make PID and local ring old structures and then pick up the pieces.
Approach 2: make DVR by just extending comm_ring, adding in all the fields, and then defining the projections to PID and local ring manually.
Approach 3: some other idea

I would like a definition of DVR and am prepared to work for it. What should I do? Any advice?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 00:16):

Mario tried making local_ring an old structure so I thought I'd try PID. I stuck set_option old_structure_cmd true near the top of ring_theory/principal_ideal_domain. I am getting errors in gaussian_int.lean:

ambiguous overload, possible interpretations
    add_comm
    principal_ideal_domain.add_comm

Does that mean I've done something wrong? I can fix everything by changing it to _root_.add_comm.

Apparently special functions and a bunch of calculus uses principal ideal domains. How do I look at the import graph?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 00:35):

#3085 . Let me know if I'm doing the wrong thing.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 01:21):

Mario's comment above refers to the following issue:

set_option old_structure_cmd true
class local_ring (α : Type u) extends comm_ring α, nonzero α :=
(is_local :  (a : α), (is_unit a)  (is_unit (1 - a)))

->

type mismatch at application
  @comm_ring.to_ring α mul_comm
term
  mul_comm
has type
  ∀ (a b : α), a * b = b * a
but is expected to have type
  comm_ring α

Can I solve this by not extending nonzero \a and instead just adding the zero_ne_one field and a projection from local_ring to nonzero?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 01:22):

I have literally epsilon understanding of this structure command stuff. Yes I know there's a wiki page about it. I just don't understand the underlying issues properly enough for the page to help.

view this post on Zulip Scott Morrison (Jun 16 2020 at 01:49):

What about the suggestion to not bundle any operations at all for PID, since it is just a property. That is, introduce is_PID.

view this post on Zulip Scott Morrison (Jun 16 2020 at 01:50):

Similarly for is_local

view this post on Zulip Adam Topaz (Jun 16 2020 at 02:10):

What are your thoughts about using some definition like this:

import ring_theory.principal_ideal_domain

class DVR (A : Type*) extends principal_ideal_domain A  :=
(val_cond :  x y : A,  z : A, x * z = y  y * z = x) -- i.e. A is a valuation ring
(nonfield :  u : A,  v : A, u * v  1) -- or some other formulation

Any valuation ring which is a PID is a DVR. Actually, any valuation ring which is Noetherian is a DVR!

Proving the local ring instance is simple enough.... here's a working gist:
https://gist.github.com/adamtopaz/7e573ec60777001ace5a3479608f992e

view this post on Zulip Kenny Lau (Jun 16 2020 at 02:24):

Kevin Buzzard said:

Can I solve this by not extending nonzero \a and instead just adding the zero_ne_one field and a projection from local_ring to nonzero?

That's what I did for the algebraic hierarchy (e.g. domain)

view this post on Zulip Bhavik Mehta (Jun 16 2020 at 02:31):

TIL what a local ring is, that's not as scary as I feared

view this post on Zulip Kenny Lau (Jun 16 2020 at 02:36):

maybe you're confused with local field, which is slightly scarier

view this post on Zulip Johan Commelin (Jun 16 2020 at 05:02):

Scott Morrison said:

Similarly for is_local

is_local_ring already exists. I'm all in favour of trying to add is_pid, is_dvr, is_noetherian, is_integrally_closed, etc...

view this post on Zulip Kenny Lau (Jun 16 2020 at 05:03):

how about is_ring and is_comm_ring predicated on semirings

view this post on Zulip Kenny Lau (Jun 16 2020 at 05:05):

oh wait that doesn't work because you need negation which isn't Prop

view this post on Zulip Kenny Lau (Jun 16 2020 at 05:06):

but if you have is_integral_domain then normalization_domain will be a pain in the bottom

view this post on Zulip Johan Commelin (Jun 16 2020 at 07:00):

Why?

view this post on Zulip Adam Topaz (Jun 16 2020 at 15:15):

Mathlib doesn't have general valuation rings right? Would it make sense for you to define a DVR like this?

import ring_theory.noetherian

class valuation_ring (A : Type*) extends integral_domain A :=
(val_cond :  a b : A, a  b  b  a)

class discrete_valuation_ring (A : Type*) extends valuation_ring A :=
(is_noetherian : is_noetherian_ring A)
(nonfield : ... )

Presumably most things one might prove about DVRs actually hold for arbitrary valuation rings.

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:16):

General valuations (but not general valuation rings) are around the corner. I think we can have them in one or two weeks, depending on the review process...

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:18):

But this valuation_ring (or maybe is_valuation_ring) seems like a useful gadget anyhow.

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:18):

(Zariski–Riemann spaces are coming to mathlib, lol.)

view this post on Zulip Adam Topaz (Jun 16 2020 at 15:19):

(deleted)

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:19):

I guess we'll want to have 13 constructors of is_DVR. There isn't 1 true definition.

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:19):

I was thinking of valuations as in adic spaces...

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:19):

We are currently considering not making them a class at all, and instead making them a predicate on commutative rings

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:21):

So still a class, but taking (comm_)ring R as assumption, instead of extending it.

view this post on Zulip Adam Topaz (Jun 16 2020 at 15:21):

I see. Presumably you would want to phrase things like the valuative criteria from AG. So valuation rings could be useful for that.

view this post on Zulip Kenny Lau (Jun 16 2020 at 15:21):

I guess we would want CDVRs as well

view this post on Zulip Kenny Lau (Jun 16 2020 at 15:22):

and a proof that they are henselian

view this post on Zulip Adam Topaz (Jun 16 2020 at 15:22):

What does CDVR stand for?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:22):

CDVR could also be a predicate

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:22):

complete DVR

view this post on Zulip Adam Topaz (Jun 16 2020 at 15:22):

ah ok.

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:22):

variables {R : Type*} [comm_ring R] [topological_space R]
    [topological_ring R] [complete_space R] [is_discrete_valuation_ring R]

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:22):

because it doesn't involve choosing some auxiliary ideal or a topology, the phrase always means "complete with respect to the topology defined by the max ideal"

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:23):

We're only missing the last class on that line.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:23):

Johan that's bad, because then you'd want the topology to be the maximal-ideal-adic one

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:23):

i.e. there's still something missing

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:23):

Ooh, right, we need another compatibility class.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:24):

distrib++

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:24):

I guess we could add is_cdvr which extends complete_space and is_dvr

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:24):

Just don't bother asking for the topology at all, would be another option

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:24):

Nope...

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:24):

Because Z_p

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:24):

"complete with respect to the topology generated by the max ideal"

view this post on Zulip Ashvni Narayanan (Jun 16 2020 at 15:25):

Maybe this is a bad question - what if we started with a Dedekind domain and used it to define a DVR?

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:25):

Will that play nice with the rest of the topology?

view this post on Zulip Adam Topaz (Jun 16 2020 at 15:25):

You can define a dedekind domain after you define DVRs :)

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:25):

We could define DVR's via Dededkind domains, but my gut feeling is that DVRs are conceptually simpler

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:26):

@Ashvni Narayanan I think we just want 10 equivalent definitions, in the end.

view this post on Zulip Ashvni Narayanan (Jun 16 2020 at 15:26):

10 equivalent definitions for DVRs?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:26):

But ideally we don't want 10 choose 2 theorems,

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:26):

Yes, there are 10 definitions of DVR on Wikipedia

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:27):

I will spend some time on this tomorrow; I'll try and get a definition of DVR into mathlib. I'm going for local PID which isn't a field as the "canonical" definition, and then there are 9 theorems to prove

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:28):

Kevin Buzzard said:

But ideally we don't want 10 choose 2 theorems,

No, just 10 constructors.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:29):

It's not going to be a structure so surely it's 9 theorems?

view this post on Zulip Ashvni Narayanan (Jun 16 2020 at 15:29):

I was trying to do a PID with a unique prime ideal, and showing that the prime ideal is maximal.

import ring_theory.ideals

import ring_theory.principal_ideal_domain

universe u

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R :=

(prime_ideal' : ideal R)

(primality : prime_ideal'.is_prime)

(is_nonzero : prime_ideal'  )

(unique_nonzero_prime_ideal :  P : ideal R, P.is_prime  P =   P = prime_ideal')


def discrete_valuation_ring.prime_ideal (R : Type u) [discrete_valuation_ring R] : ideal R :=
discrete_valuation_ring.prime_ideal'

variables {R : Type u} [discrete_valuation_ring R]
open principal_ideal_domain
open discrete_valuation_ring

lemma prime_ideal_is_maximal : (prime_ideal R).is_maximal :=
begin
have f : prime_ideal R  ,
sorry,
apply is_prime.to_maximal_ideal,
end

view this post on Zulip Ashvni Narayanan (Jun 16 2020 at 15:30):

The last line gives me an error,

invalid apply tactic, failed to synthesize type class instance
state:
R : Type u,
_inst_1 : discrete_valuation_ring R,
f : prime_ideal R  
 (prime_ideal R).is_maximal

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:30):

All these definitions should work, but my experience in the past has been that if you just choose a random definition and then formalise some stuff, you might find it's hard to get it into mathlib, and I know now that it's a grave mistake not to have mathlib in mind from the very start

view this post on Zulip Ashvni Narayanan (Jun 16 2020 at 15:33):

What does getting it into mathlib mean? Isn't it sufficient to pass the Lean checker test?

view this post on Zulip Johan Commelin (Jun 16 2020 at 15:33):

@Kevin Buzzard It's going to be a class right? With fields, etc... so it's a souped up structure, so constructors?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:33):

Wait -- I thought we had just established that is_DVR was going to be a non-class predicate on comm_rings?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:34):

is_local_ring isn't a class

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:35):

I thought the plan was is_principal_ideal_domain and is_discrete_valuation_domain both being Props on...actually integral_domain is a class so how about predicates on integral domains?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:37):

Ashvni Narayanan said:

What does getting it into mathlib mean? Isn't it sufficient to pass the Lean checker test?

No. Mathlib only accepts code which satisfies certain very high standards. I'm not bothered about our general DVR project being of this standard but for the definition itself I think we should engage with the hard question of deciding exactly which implementation we will use for the specification of DVR's.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:37):

Once we have this, we can forget about all this nonsense and just prove some theorems

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:37):

and the theorems can be refactored and cleaned up later. But if we get the definition wrong then the clean-up process is much much harder

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:38):

This is why there is currently such a fuss about the definition of a DVR. It has turned into a discussion of whether classes such as principal_ideal_domain should even exist

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:38):

@Johan Commelin can you clarify your comments about is_DVR being a class?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:43):

@Ashvni Narayanan

import ring_theory.ideals

import ring_theory.principal_ideal_domain

universe u

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R :=

(prime_ideal' : ideal R)

(primality : prime_ideal'.is_prime)

(is_nonzero : prime_ideal'  )

(unique_nonzero_prime_ideal :  P : ideal R, P.is_prime  P =   P = prime_ideal')

namespace discrete_valuation_ring

def prime_ideal (R : Type u) [discrete_valuation_ring R] : ideal R :=
discrete_valuation_ring.prime_ideal'

instance is_prime (R : Type*) [discrete_valuation_ring R] : (prime_ideal R).is_prime :=
primality

variables {R : Type u} [discrete_valuation_ring R]
open principal_ideal_domain
open discrete_valuation_ring

lemma prime_ideal_is_maximal : (prime_ideal R).is_maximal :=
begin
  have f : prime_ideal R  ,
  { apply discrete_valuation_ring.is_nonzero },
  apply is_prime.to_maximal_ideal,
  sorry,
end

end discrete_valuation_ring

The fact that the prime ideal was prime was not in Lean's type class inference system.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 15:48):

The problem with your code (and Lean did a very poor job of pointing this out) was that the inputs to the is_prime.to_maximal_ideal function look like this:

#check @is_prime.to_maximal_ideal
/-
is_prime.to_maximal_ideal :
  ∀ {R : Type u_1} [_inst_1 : principal_ideal_domain R] {S : ideal R}
  [hpi : S.is_prime], S ≠ ⊥ → S.is_maximal
-/

(the @ means "show me even the inputs which Lean is supposed to guess!). One of the inputs is hpi : S.is_prime and because that input is in square brackets it means that a system called type class inference is supposed to be used to magic up the proof that the ideal S is prime. In your case, S is prime_ideal R but just because it's called that doesn't mean that the type class inference system knows it's prime :-) The instance line which I added to your code tells the type class inference system that the prime ideal is prime, and then the error goes away.

Note also that I moved into the discrete_valuation_ring namespace, meaning that I don't have to type discrete_valuation_ring in front of everything.

view this post on Zulip Ashvni Narayanan (Jun 16 2020 at 15:58):

Ah, now I understand! In the definition of prime_ideal, I took it to be prime_ideal', but that does not include the primality condition. Thank you!

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 16:04):

Right -- the instance means "feed this proof into the type class inference machine" but the proof was primality

view this post on Zulip Johan Commelin (Jun 16 2020 at 16:13):

Kevin Buzzard said:

Johan Commelin can you clarify your comments about is_DVR being a class?

@Kevin Buzzard I would like to have automation (in this case, the type class system) to take care of "every DVR is a PID", and not supply those proofs explicitly.

view this post on Zulip Johan Commelin (Jun 16 2020 at 16:13):

Just like topological_ring R is a class that assumes ring R and topological_space R

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 16:15):

How is what you're proposing different to the current definition of PID?

view this post on Zulip Johan Commelin (Jun 16 2020 at 16:16):

The difference is that zero and add etc are no longer fields of that class

view this post on Zulip Johan Commelin (Jun 16 2020 at 16:16):

So the class lives in Prop instead of Type*

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 16:17):

So the change is that were not extending integral_domain but instead asking for it as a typeclass on our type?

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 16:22):

import ring_theory.principal_ideal_domain

class is_principal_ideal_domain (R : Type*) [integral_domain R] : Prop :=
(principal :  (S : ideal R), S.is_principal)

class is_PID_fail (R : Type*) [integral_domain R] :=
(principal :  (S : ideal R), S.is_principal)

#check is_PID_fail -- Π ..., Type

You think is_principal_ideal_domain is the way to go? I am slightly surprised I had to explicitly tell Lean that it was a Prop.

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 16:24):

PS it does seem absurd that UFD contains all that data. The analogue would be choosing a generator for each ideal.

view this post on Zulip Reid Barton (Jun 16 2020 at 16:25):

Yeah, structure/class never defaults to Prop for some reason and it is weird.

view this post on Zulip Reid Barton (Jun 16 2020 at 16:26):

I think some of the separation classes like t2_space used to accidentally not be Props.

view this post on Zulip Johan Commelin (Jun 16 2020 at 16:50):

@Kevin Buzzard Yes, but I would assume [comm_ring R], and in applications we can assume [integral_domain R].

view this post on Zulip Johan Commelin (Jun 16 2020 at 16:51):

This way we get principal ideal rings and principal ideal domains in one go (a slight hint of the flexibility I'm hoping this refactor will achieve).

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 17:06):

So do you want is_PIR and is_PID?

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:08):

No, only is_PIR

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:08):

Because it covers everything

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:09):

I guess we'll end up with "principal ideal semirings" (-;

view this post on Zulip Kevin Buzzard (Jun 16 2020 at 17:09):

and we'll also end up with mathematicians asking "where are PIDs?" and we'll have to say "oh you use ID and PIR" and they'll say "why no PID?"

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:10):

Similarly, we'll probably define "discrete valuation semiring". But all theorems will assume integral_domain.

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:10):

Kevin Buzzard said:

and we'll also end up with mathematicians asking "where are PIDs?" and we'll have to say "oh you use ID and PIR" and they'll say "why no PID?"

Because it means proving things twice?

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:15):

Maybe we could at some point have some syntactic sugar to make things look nicer.

view this post on Zulip Johan Commelin (Jun 16 2020 at 17:15):

But at the moment I would go for maximum flexibility.

view this post on Zulip Ashvni Narayanan (Jun 17 2020 at 15:19):

I am trying to prove that a local PID that is not a field is a DVR, using the definition that a DVR is a PID with a unique nonzero prime ideal (doing it to get comfortable with Lean).

class discrete_valuation_ring (R : Type u) extends principal_ideal_domain R :=

(prime_ideal' : ideal R)

(primality : prime_ideal'.is_prime)

(is_nonzero : prime_ideal'  )

(unique_nonzero_prime_ideal :  P : ideal R, P.is_prime  P =   P = prime_ideal')

open principal_ideal_domain
open local_ring

lemma local_pid_dvr {S : Type u} (is_local : local_ring S) (pid: principal_ideal_domain S) (non_field : local_ring.nonunits_ideal S   ) : discrete_valuation_ring S :=
begin
use local_ring.nonunits_ideal S,
rw zero_mem_nonunits S,
sorry,
end

The first line of the proof gives me 6 goals, 5 of which are basically properties of ideals. Since S is a local ring, why do I need to reprove it? Also, the second line gives me an error

function expected at
  zero_mem_nonunits
term has type
  0  nonunits ?m_1  0  1

view this post on Zulip Scott Morrison (Jun 17 2020 at 15:25):

A #mwe needs imports!

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 15:30):

@Ashvni Narayanan the way you have set up a DVR, it contains data (the choice of a prime ideal) so you don't want to use lemma -- this is a construction, the way you've set it up, so it's a definition. The way to make terms of a structure is like this:

def local_pid_dvr {S : Type u} (is_local : local_ring S) (pid: principal_ideal_domain S) (non_field : local_ring.nonunits_ideal S   ) :
  discrete_valuation_ring S :=
  { prime_ideal' := _,
  primality := _,
  is_nonzero := _,
  unique_nonzero_prime_ideal := _,
  ..pid}

but principal_ideal_domain is a class so you should be using [] brackets (and local_ring too)

view this post on Zulip Ashvni Narayanan (Jun 17 2020 at 16:18):

Thank you, that was very helpful. But I am back with the type mismatch errors, I am guessing it is the new/old structure problem cropping up?

def local_pid_dvr {S : Type u} [is_local : local_ring S] [pid: principal_ideal_domain S] (non_field : local_ring.nonunits_ideal S   ) :
  discrete_valuation_ring S :=
  { prime_ideal' := (nonunits_ideal S),
  primality := (nonunits_ideal S).is_prime,
  is_nonzero := _,
  unique_nonzero_prime_ideal := _,
  ..pid}

I get the error

type mismatch at field 'prime_ideal''
  nonunits_ideal S
has type
  @ideal S (@to_comm_ring S is_local)
but is expected to have type
  @ideal S
    (@integral_domain.to_comm_ring S
       (@to_integral_domain S (@principal_ideal_domain.mk S (@to_integral_domain S pid) _)))

view this post on Zulip Johan Commelin (Jun 17 2020 at 16:24):

@Ashvni Narayanan Yes, that looks like it is getting the wrong ring structure again.

view this post on Zulip Johan Commelin (Jun 17 2020 at 16:24):

We really need to fix this... but I won't have time for such a project the next few days :sad:

view this post on Zulip Ashvni Narayanan (Jun 17 2020 at 16:28):

Oh, no worries, I am just trying to see how far I can go, and just get comfortable with the language.

view this post on Zulip Kevin Buzzard (Jun 17 2020 at 18:07):

I will fix it the moment I am done with all this work admin (which has a deadline of Thurs).

view this post on Zulip Ashvni Narayanan (Jun 18 2020 at 23:37):

I am trying to define a discrete valuation field :

class discrete_valuation_field (K : Type u) (h : field K) :=
(discrete_valuation : v : K ->   )
(mul :  (x y : K) v(x*y) = v(x) + v(y) )
(add : v(x + y)  min{v(x), v(y)} )
(non_zero :  (x : K), v(x) =   x = 0 )

I get the error

unknown identifier 'v'

How can I fix this? Thanks!

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:38):

the second line has two binders

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:39):

Is ℤ ∨ ∞ a type? if not, maybe you mean with_top

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:40):

class discrete_valuation_field (K : Type u) (h : field K) :=
(v : K -> with_top  )
(mul :  x y, v(x*y) = v(x) + v(y) )
(add :  x y, v(x + y)  min{v(x), v(y)} )
(non_zero :  (x : K), v(x) = \top  x = 0 )

view this post on Zulip Reid Barton (Jun 18 2020 at 23:41):

Always look at the first error

view this post on Zulip Ashvni Narayanan (Jun 18 2020 at 23:41):

Thank you!

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:45):

The following does not throw errors on my machine

import tactic

noncomputable theory
open_locale classical

class discrete_valuation_field (K : Type*) [field K] :=
(v : K -> with_top )
(mul :  (x y : K), v(x * y) = v(x) + v(y) )
(add :  x y, v (x + y)  min (v x) (v y) )
(non_zero :  (x : K), v(x) =   x = 0 )

view this post on Zulip Ashvni Narayanan (Jun 18 2020 at 23:46):

what does open_locale classical do?

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:47):

it tells lean to not worry about stuff like the law of excluded middle

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:47):

before I added it, it wanted me to supply a decidable linear order on K

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:49):

(important edit to the previous post)

view this post on Zulip Ashvni Narayanan (Jun 18 2020 at 23:52):

Thank you!

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:55):

most of the errors lean gives you are easy to understand. When I first put in

universe u

class discrete_valuation_field (K : Type u) (h : field K) :=
(discrete_valuation : v : K ->   )

I got unknown identifier v. If you look near the first appearance of the identifier v, there are two binders. So Lean read the first one and was expecting an expression that defines a type; instead it got v which it has never heard of before

view this post on Zulip Reid Barton (Jun 18 2020 at 23:58):

Oh I didn't even notice the bad syntax on the first line, I assumed the error was later.

view this post on Zulip Jalex Stark (Jun 18 2020 at 23:59):

Next I try this

universe u

class discrete_valuation_field (K : Type u) (h : field K) :=
( v : K ->   )

and I get unknown identifier field, which means I haven't imported enough of mathlib to get fields

view this post on Zulip Adam Topaz (Jun 19 2020 at 00:01):

I think this definition is missing a nontriviality assumption. E.g. you can ensure v is surjective (or at least nontrivial). Otherwise, this definition will include the trivial valuation.

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:01):

Next I try this

import tactic

universe u

class discrete_valuation_field (K : Type u) (h : field K) :=
( v : K ->   )

and field gets recognized. Next I get unexpected token. The two unicode characters that pop out at me are and . I know I've seen before, but I don't know about the other one. To confirm, I try the following and it works

import tactic

universe u

class discrete_valuation_field (K : Type u) (h : field K) :=
( v : K ->   )

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:05):

Now I add the rest

class discrete_valuation_field (K : Type u) (h : field K) :=
( v : K -> with_top )
(mul :  (x y : K) v(x*y) = v(x) + v(y) )
(add : v(x + y)  min{v(x), v(y)} )
(non_zero :  (x : K), v(x) =   x = 0 )

and get multiple unknown identifiers for x and y. x and y appear a lot of times, sometimes with a forall and sometimes not. I add some quantifiers and those errors go away

class discrete_valuation_field (K : Type u) (h : field K) :=
( v : K -> with_top )
(mul :  (x y : K), v(x*y) = v(x) + v(y) )
(add :  x y, v(x + y)  min{v(x), v(y)} )
(non_zero :  (x : K), v(x) =   x = 0 )

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:05):

Now I have a much longer error

type mismatch at application
  v (x + y)  min {v x, v y}
term
  min {v x, v y}
has type
  ?m_1  ?m_1 : Type ?
but is expected to have type
  with_top  : Type

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:06):

Maybe the question marks look scary, but just treat ?m_1 as a variable.

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:06):

It says that a certain expression is supposed to have type with_top ℤ, which is the image of the valuation map. Mathematically, I agree that's the right type.

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:08):

next I do #check min and lean tells me its type is min : ?M_1 → ?M_1 → ?M_1. That means it's a function of two arguments. In Lean, a function of two arguments is written like min (v x) (v y), with only spaces separating the function and arguments.

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:09):

I can also do #check @min to see min : Π {α : Type u_1} [_inst_1 : decidable_linear_order α], α → α → α
this means that min only applies to types which are known to be decidable_linear_orders

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:09):

where by "known to be" I mean "known by the typeclass-inference systems"

view this post on Zulip Jalex Stark (Jun 19 2020 at 00:11):

apparently lean stops complaining at this point, although I thought before lean had complained about inferring the order and the field operations on K

view this post on Zulip Ashvni Narayanan (Jun 19 2020 at 00:16):

I see. That was very useful, thanks a lot! I didn't know about #check @... , will keep it in mind.

view this post on Zulip Ashvni Narayanan (Jun 19 2020 at 15:29):

I am trying to define discrete valuations via discrete valuation fields :

noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(val : K -> with_top  )
(mul :  (x y : K), val(x*y) = val(x) + val(y) )
(add :  (x y : K), val(x + y)  min (val(x)) (val(y)) )
(non_zero :  (x : K), val(x) =   x = 0 )
(non_trivial : val(1)  0)

namespace discrete_valuation_field

instance discrete_valuation_field.valuation (K : Type*) [ discrete_valuation_field K ] : K -> with_top  := discrete_valuation_field.val

The last definition gives the error:

failed to synthesize type class instance for
K : Type ?,
_inst_1 : discrete_valuation_field K
 field K

I don't know why there is a type class instance error here. Help is appreciated. Thanks!

view this post on Zulip Kenny Lau (Jun 19 2020 at 15:30):

instance discrete_valuation_field.valuation (K : Type*) [field K] [ discrete_valuation_field K ]

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:31):

i.e. insert the fact that K is a field -- this is what Lean is telling you that it can't figure out.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:33):

oh and it's a def not an instance.

view this post on Zulip Kevin Buzzard (Jun 19 2020 at 15:34):

You use instance for a definition which you want to teach to the type class inference system (the stuff in square brackets which you want Lean to fill in).

view this post on Zulip Adam Topaz (Jun 19 2020 at 15:36):

The units of the valuation are the preimage of 00. And 11 is a unit. So the "non_trivial" assumption is not correct here...

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 17:44):

Trying to show that the valuation ring coming from a discrete valuation field is an integral domain.

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

universe u

noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(val : K -> with_top  )
(mul :  (x y : K), val(x*y) = val(x) + val(y) )
(add :  (x y : K), val(x + y)  min (val(x)) (val(y)) )
(non_zero :  (x : K), val(x) =   x = 0 )

namespace discrete_valuation_field

definition discrete_valuation_field.valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top  := discrete_valuation_field.val

variables {K : Type*} [field K] [discrete_valuation_field K]

lemma is_integral_domain (S : Type*) (K:Type*) [field K] [discrete_valuation_field K]  (h : S = {x : K | val(x)  0}) : integral_domain S :=
begin
   split,
  rintros,
   {apply mul_comm},
    {
      rintros,
      have g : val (a*b) = val(0:K),
sorry,
end

The g part gives an error

failed to synthesize type class instance for
S K : Type u_1,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K,
h : S = {x : K | val x  0},
P : set K := {x : K | val x > 0},
a b : S,
a_1 : a * b = 0
 has_mul S

It seems like Lean sees a and b as elements of S, instead of K. But why was that not an issue for the first goal? Also, how do I show that it is in K? I tried

have a:K

but this seems to create a new variable a in K.
Any help is appreciated. Thank you!

view this post on Zulip Yakov Pechersky (Jun 24 2020 at 18:00):

(Is it normal that it's taking me 10 min to get the Lean server to even import the files listed here?)

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 18:07):

No, it is not normal. The server has been going up and down for a while now.

view this post on Zulip Adam Topaz (Jun 24 2020 at 18:12):

Would it be better to try something like this?

instance is_integral_domain (K:Type*) [field K] [discrete_valuation_field K] : integral_domain {x : K | val(x)  0} := sorry

view this post on Zulip Alex J. Best (Jun 24 2020 at 18:16):

I would say also that its better to use {x : K // 0 ≤ val x}, the // means subtype rather than subset, so there isn't this weird , you have the type of all elements satisfying the prop directly. Also less or equal rather than greater or equal as the mathlib setup is to almost always use less than statements (by swapping sides if needed) so it might be easier to find and apply lemmas relating to less than.

view this post on Zulip Adam Topaz (Jun 24 2020 at 18:17):

Also, mathlib has this:
https://leanprover-community.github.io/mathlib_docs/ring_theory/subring.html#subring.domain
So if you can prove a subring instance for the valuation ring, then lean should be able to deduce the fact that it's a domain from the fact that any field is a domain.

view this post on Zulip Alex J. Best (Jun 24 2020 at 18:18):

If you do what adam says then you should ignore the first thing I said, looks like that lemma is set up as a set rather than a subtype!

view this post on Zulip Johan Commelin (Jun 24 2020 at 20:39):

@Alex J. Best Or do what you said + fix mathlib :wink:

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 20:42):

Adam Topaz said:

Also, mathlib has this:
https://leanprover-community.github.io/mathlib_docs/ring_theory/subring.html#subring.domain
So if you can prove a subring instance for the valuation ring, then lean should be able to deduce the fact that it's a domain from the fact that any field is a domain.

I don't know how to work with is_subring, how do I split it into goals? split does not seem to work out

view this post on Zulip Johan Commelin (Jun 24 2020 at 20:50):

constructor?

view this post on Zulip Johan Commelin (Jun 24 2020 at 20:50):

Or refine { zero_mem := _, etc....}

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 20:57):

Oh, ok. Thank you!

view this post on Zulip Jalex Stark (Jun 24 2020 at 21:12):

suggest will find you the refine block that Johan suggested, possibly along with lemmas that let you do the construction with fewer fields

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 22:30):

Trying to prove that the valuation ring coming from a discrete valuation field is an integral domain.

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

universe u
noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(val : K -> with_top  )
(mul :  (x y : K), val(x*y) = val(x) + val(y) )
(add :  (x y : K), val(x + y)  min (val(x)) (val(y)) )
(non_zero :  (x : K), val(x) =   x = 0 )

namespace discrete_valuation_field

definition discrete_valuation_field.valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top  := discrete_valuation_field.val

variables {K : Type*} [field K] [discrete_valuation_field K]

lemma val_zero : val(0:K) =  :=
begin
rw non_zero,
end

instance is_integral_domain (K:Type*) [field K] [discrete_valuation_field K] : integral_domain {x : K | 0  val(x) } :=
begin
  let P := {x : K | val(x) > 0},
  constructor,
  rintros,
    {apply mul_comm},
    {
      rintros,
      have g : val ((a:K)*(b:K)) = val(0:K),
        {
          sorry,
        },
      rw mul at g,
      rw val_zero at g,
      rw with_top.add_eq_top at g,
      cases g,
        {rw non_zero at g,
        left,
        rw <-with_top.coe_eq_zero,
        rw g,
        },
    },
sorry,
end

I get the error:

rewrite tactic failed, did not find instance of the pattern in the target expression
  a
state:
K : Type ?,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K,
P : set K := {x : K | val x > 0},
a b : {x : K | 0  val x},
a_1 : a * b = 0,
g : a = 0
 a = 0

Any help is appreciated. Thank you!

view this post on Zulip Alex J. Best (Jun 24 2020 at 22:34):

Which line gives you an error? I get a different error on the line exact g

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 22:35):

The exact g line gives the error..

view this post on Zulip Alex J. Best (Jun 24 2020 at 22:36):

Hmm but the error you pasted is talking about rewrite, is that the right one?

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 22:37):

Oh, apologies, I edited the code.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:38):

wow that is some error

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 22:38):

Yeah, that is why i changed it to rewrite, atleast it is shorter.

view this post on Zulip Alex J. Best (Jun 24 2020 at 22:38):

Ok, the problem is that the little up arrow means different things in your hypothesis and goal, if you want to see what its doing you can do unfold_coes at * to unfold the coercions.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:40):

You're missing an end discrete_valuation_field.

The whole point of namespaces is precisely so you don't have to write definition discrete_valuation_field.valuation after the namespace command -- you can just write definition valuation .... See section 6.3 of #tpil

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 22:41):

Also, the server has stopped working several times today. Is that the case only for me?

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:41):

It's a server running on your computer

view this post on Zulip Alex J. Best (Jun 24 2020 at 22:42):

In this case it tells us that g is saying a.val is zero, as a is really a pair, an element of K and a proof that it has nonnegative valuation. So you can use rw subtype.ext to change the goal to be of that form.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:47):

I think the problem here is that Lean might not know what the multiplication on the integral domain is?

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:48):

instance is_integral_domain (K:Type*) [field K] [discrete_valuation_field K] : integral_domain {x : K | 0  val(x) } :=
{ add := _,
  add_assoc := _,
  zero := _,
  zero_add := _,
  add_zero := _,
  neg := _,
  add_left_neg := _,
  add_comm := _,
  mul := _,
  mul_assoc := _,
  one := _,
  one_mul := _,
  mul_one := _,
  left_distrib := _,
  right_distrib := _,
  mul_comm := _,
  eq_zero_or_eq_zero_of_mul_eq_zero := _,
  zero_ne_one := _ }

This is the job you have to do here. I'm not sure where Lean got the ring structure on P from.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:49):

But the definition of add and mul must at the very least contain proofs that if 0<=v(a) and 0<=v(b) then 0<=v(a+b) resp v(a*b) and I don't see them in your set-up.

view this post on Zulip Jalex Stark (Jun 24 2020 at 22:49):

Alex J. Best said:

Ok, the problem is that the little up arrow means different things in your hypothesis and goal, if you want to see what its doing you can do unfold_coes at * to unfold the coercions.

wow! I have been doing a lot more work than that to figure out what my mystery coercions are, and I'm grateful that unfold_coes exists

view this post on Zulip Patrick Massot (Jun 24 2020 at 22:50):

Ashvni Narayanan said:

Also, the server has stopped working several times today. Is that the case only for me?

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/crashes/near/201856564

view this post on Zulip Jalex Stark (Jun 24 2020 at 22:51):

Kevin Buzzard said:

But the definition of add and mul must at the very least contain proofs that if 0<=v(a) and 0<=v(b) then 0<=v(a+b) resp v(a*b) and I don't see them in your set-up.

These follow pretty easily from discrete_valuation_field.mul and discrete_valuation_field.add

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:52):

Sure, but the fact that they're not in the original code makes me skeptical that the original code has got the right definition of multiplication. That's why the earlier sorry is there, I think the result is unprovable

view this post on Zulip Ashvni Narayanan (Jun 24 2020 at 22:53):

I just assumed that Lean would ask for it in the proof, because in the definition, the valuation ring is just a set with no structure

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:54):

The way I'm setting it up it will ask you when you define add and mul.

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:57):

The definition of add in discrete_valuation_field should be rewritten so it uses <= not >=

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:58):

sorry, I need to go. I didn't finish the job:

instance is_integral_domain (K:Type*) [field K] [discrete_valuation_field K] : integral_domain {x : K | 0  val(x) } :=
{ add := λ a b, a.1 + b.1, begin
    change (0 : with_top )  val (a.1 + b.1),
      have h := add a.1 b.1,
      have ha : 0  val (a.1) := a.2,
      have hb : 0  val (b.1) := b.2,
      sorry
  end,
  add_assoc := _,

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 22:59):

It's very confusing that a.val = a.1, and val is something else too. Maybe change the DVF val to v?

view this post on Zulip Kevin Buzzard (Jun 24 2020 at 23:25):

An alternative approach is to make a term of type subring K. This will involve having to check far fewer axioms

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 09:07):

Here's a far less painful way to make that subset into a ring:

instance (K:Type*) [field K] [discrete_valuation_field K] : is_add_subgroup {x : K | 0  val(x) } :=
{ zero_mem := sorry,
  add_mem := sorry,
  neg_mem := sorry }

instance (K:Type*) [field K] [discrete_valuation_field K] : is_submonoid {x : K | 0  val(x) } :=
{ one_mem := sorry,
  mul_mem := sorry }

instance (K:Type*) [field K] [discrete_valuation_field K] : is_subring {x : K | 0  val(x) } :=
{..is_add_subgroup, ..is_submonoid}

view this post on Zulip Ashvni Narayanan (Jun 25 2020 at 12:24):

What does the .. do?

view this post on Zulip Patrick Massot (Jun 25 2020 at 12:28):

https://leanprover.github.io/reference/declarations.html#structures-and-records

view this post on Zulip Patrick Massot (Jun 25 2020 at 12:28):

Or the more friendly https://leanprover.github.io/theorem_proving_in_lean/structures_and_records.html#objects

view this post on Zulip Ashvni Narayanan (Jun 25 2020 at 12:30):

Thank you!

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 12:31):

All of the sorrys are Propositions, so you can replace them with begin ... end and then fill in the proofs.

view this post on Zulip Ashvni Narayanan (Jun 25 2020 at 12:41):

The last one (is_subring K) gives me an error

invalid structure notation source, not a structure
  is_add_subgroup
which has type
  set ?m_1  Prop

view this post on Zulip Johan Commelin (Jun 25 2020 at 12:42):

It takes an argument

view this post on Zulip Ashvni Narayanan (Jun 25 2020 at 12:42):

Also, why do both is_add_subgroup and add_subgroup exist?

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 12:43):

One of them will be removed one day (is_add_subgroup will be the one which goes)

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 12:44):

It seemed to me that subring doesn't exist so it seemed simpler to show you a unified approach. The is_ stuff might disappear one day, but you don't have to worry about this right now.

view this post on Zulip Ashvni Narayanan (Jun 25 2020 at 12:49):

(deleted)

view this post on Zulip Kevin Buzzard (Jun 25 2020 at 13:48):

Which version of lean and mathlib are you using

view this post on Zulip Alex J. Best (Jun 25 2020 at 13:53):

I get similar problems with the latest lean + mathlib about is_add_subgroup not being a structure?
I tried

instance (K:Type*) [field K] [discrete_valuation_field K] : is_subring {x : K | 0  val(x) } :=
begin
 refine is_subring.mk,
end

and it looks like it worked?

view this post on Zulip Ashvni Narayanan (Jun 25 2020 at 14:24):

Oh nice! This seems to work. Thank you!

view this post on Zulip Ashvni Narayanan (Jun 26 2020 at 16:51):

I am trying to define S := {x : K | 0 ≤ v(x) } , the valuation ring.

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

import tactic

universe u

noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(v : K -> with_top  )
(mul :  (x y : K), v(x*y) = v(x) + v(y) )
(add :  (x y : K), min (v(x)) (v(y))  v(x + y)  )
(non_zero :  (x : K), v(x) =   x = 0 )

namespace discrete_valuation_field

definition valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top  := v

variables {K : Type*} [field K] [discrete_valuation_field K]

definition valuation_ring {S:Type*} [K:Type*] [field K] [discrete_valuation_field K] := {x : K | 0  v(x) }
variables {S: Type*} [S = {x : K | 0  v(x) } ]

end discrete_valuation_field

I can't use the valuation_ring definition because it has no variables. I don't know how to put in a variable S there. The variables line gives me an error:

type mismatch at application
  S = is_subring {x : K | 0  v x}
term
  is_subring {x : K | 0  v x}
has type
  Prop : Type
but is expected to have type
  Type u_2 : Type (u_2+1)

It would simplify my life a great deal if I had this variable S. Any help is appreciated. Thank you!

view this post on Zulip Johan Commelin (Jun 26 2020 at 17:01):

I'm confused about what you want to do with this S.

view this post on Zulip Johan Commelin (Jun 26 2020 at 17:01):

In definition valuation_ring you are not using S at all, so you can just delete it.

view this post on Zulip Johan Commelin (Jun 26 2020 at 17:02):

[S = {x : K | 0 ≤ v(x) } ] will not make any sense to lean at all.
If you have [blabla] then lean will try to add something to the type class system. That's what [] do. (For example [ring R].)

view this post on Zulip Johan Commelin (Jun 26 2020 at 17:03):

It means that you tell lean: "Hey, you know this R that I told you about earlier. Give it the structure of a ring."

view this post on Zulip Ashvni Narayanan (Jun 26 2020 at 17:04):

This is just for notation purposes, it would be easier to use S instead of {x : K | 0 ≤ v(x) }

view this post on Zulip Johan Commelin (Jun 26 2020 at 17:04):

Maybe you want notation?

notation `S` := valuation_ring K

view this post on Zulip Johan Commelin (Jun 26 2020 at 17:04):

You shouldn't use {x : K | 0 ≤ v(x) } either, because you have made a definition.

view this post on Zulip Johan Commelin (Jun 26 2020 at 17:05):

You want to prove things about that definition instead

view this post on Zulip Johan Commelin (Jun 26 2020 at 17:08):

Johan Commelin said:

Maybe you want notation?

notation `S` := valuation_ring K

If this is what you want, it might be better to use local notation instead of notation, so that it is only notation in this file, and not everything that will import this file (in the future).

view this post on Zulip Ashvni Narayanan (Jun 26 2020 at 17:10):

Johan Commelin said:

Maybe you want notation?

notation `S` := valuation_ring K

Yes! This is what I was looking for! Thanks a ton!

view this post on Zulip Ashvni Narayanan (Jun 27 2020 at 15:11):

Ashvni Narayanan said:

I am trying to define S := {x : K | 0 ≤ v(x) } , the valuation ring.

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

import tactic

universe u

noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(v : K -> with_top  )
(mul :  (x y : K), v(x*y) = v(x) + v(y) )
(add :  (x y : K), min (v(x)) (v(y))  v(x + y)  )
(non_zero :  (x : K), v(x) =   x = 0 )

namespace discrete_valuation_field

definition valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top  := v

variables {K : Type*} [field K] [discrete_valuation_field K]

definition valuation_ring {S:Type*} [K:Type*] [field K] [discrete_valuation_field K] := {x : K | 0  v(x) }
variables {S: Type*} [S = {x : K | 0  v(x) } ]

end discrete_valuation_field

I can't use the valuation_ring definition because it has no variables. I don't know how to put in a variable S there. The variables line gives me an error:

type mismatch at application
  S = is_subring {x : K | 0  v x}
term
  is_subring {x : K | 0  v x}
has type
  Prop : Type
but is expected to have type
  Type u_2 : Type (u_2+1)

It would simplify my life a great deal if I had this variable S. Any help is appreciated. Thank you!

In this example, I have defined valuation_ring. I am now trying to prove 0 is in the ring. The goal is :

0  val_ring K

How can I change it to

0  { x : K | 0  v x }

I guess the general question is, how do I unravel a definition?

Any help is appreciated. Thank you!

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:13):

unfold val_ring?

view this post on Zulip Ashvni Narayanan (Jun 27 2020 at 15:14):

Oh, great! Thank you!

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:15):

you should also be able to manipulate it without unfolding it, try erw non_zero

view this post on Zulip Ashvni Narayanan (Jun 27 2020 at 15:16):

Gives the error

rewrite tactic failed, did not find instance of the pattern in the target expression
  v ?m_4 = 
state:
K : Type ?,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K
 0  val_ring K

view this post on Zulip Jalex Stark (Jun 27 2020 at 15:30):

ah, that's because we tried the wrong direction. does erw ← non_zero work there? erw means something like "rw, but do some definitional unfolding first"

view this post on Zulip Ashvni Narayanan (Jun 27 2020 at 15:42):

Gives this error :

rewrite tactic failed, did not find instance of the pattern in the target expression
  ?m_2 = 0
state:
K : Type ?,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K
 0  val_ring K

I am not sure rw would work here, because first it needs to be got from

 0  {x : K | 0  v x}

to

 0  v 0

which is done by simp. Unless erw also tries simp?

view this post on Zulip Jalex Stark (Jun 27 2020 at 16:01):

there's a simp_rw which might work (i'm assuming you've gotten around this on your own and the current conversation is academic; is that right?)

view this post on Zulip Ashvni Narayanan (Jun 27 2020 at 16:02):

Yes, I constructed a lemma that showed v(0) = \top, and then used that.

view this post on Zulip Jalex Stark (Jun 27 2020 at 16:15):

hopefully the proof of that lemma was just rw non_zero?

view this post on Zulip Ashvni Narayanan (Jun 27 2020 at 16:16):

Yes

view this post on Zulip Ashvni Narayanan (Jun 29 2020 at 10:46):

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

import tactic

universe u

noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(v : K -> with_top  )
(mul :  (x y : K), v(x*y) = v(x) + v(y) )
(add :  (x y : K), min (v(x)) (v(y))  v(x + y)  )
(non_zero :  (x : K), v(x) =   x = 0 )

namespace discrete_valuation_field

definition valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top  := v

variables {K : Type*} [field K] [discrete_valuation_field K]

lemma with_top.cases (a : with_top ) : a =    n : , a = n :=
begin
  cases a with n,
  { -- a = ⊤ case
    left,
    refl, -- true by definition
  },
  { -- ℤ case
    right,
    use n,
    refl, -- true by definition
  }
end


lemma val_one_eq_zero : v(1 : K) = 0 :=
begin
have f : (1:K)*(1:K) = (1 : K),
simp,
have g : v(1 : K) = v((1 : K)*(1 : K)),
simp,
have k : v((1 : K)*(1 : K)) = v(1 : K) + v(1 : K),
{apply mul},
rw k at g,
rw g,
cases (with_top.cases (v(1:K))) with h1 h2,
{
rw h1,
rw h1 at g,
rw <-g,
rw non_zero at h1,
exfalso,
exact one_ne_zero h1,
},
cases h2 with n h2,
{
rw h2,
rw sum_zero_iff_zero,
rw h2 at g,
norm_cast at g,
simp,
linarith,
},
end

def val_ring (K : Type*) [field K] [discrete_valuation_field K] := { x : K | 0  v x }

lemma unit_iff_val_zero (K:Type*) [field K] [discrete_valuation_field K] [α : (val_ring K)] : v (α : K) = 0  is_unit α :=
begin
split,
{
  rintros,
  rw is_unit_iff_exists_inv,
  use α⁻¹,
  {
    unfold val_ring,
    simp,
    have f : v((α : K) * (α⁻¹ : K)) = 0,
    {
      rw mul_inv_cancel,
      {
        rw val_one_is_zero,
      },
      {
        from λ h,
        by
        {
          rw [<-non_zero, a] at h,
          cases h,
        },
      },
    },
  rw mul at f,
  rw a at f,
  simp at f,
  rw f,
  norm_num,
  },
  {
    sorry,
  },
},
{
sorry,
},

end discrete_valuation_field

I don't understand the goal for the second to last sorry:

K : Type u_1,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K,
α : (val_ring K),
a : v α = 0
 α * (α)⁻¹, _⟩ = 1

Any help is appreciated. Thank you!

view this post on Zulip Scott Morrison (Jun 29 2020 at 11:17):

It looks like α has been coerced to somewhere (you should work out where), then you've taken the inverse, and then you've put it back in ↥(val_ring K) by providing a proof which just appears as _.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:17):

Your code doesn't compile for me -- I get an error at rw sum_zero_iff_zero

view this post on Zulip Scott Morrison (Jun 29 2020 at 11:18):

Were you hoping to see ⊢ α * α⁻¹ = 1?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:19):

and I get an error on is_unit alpha in the statement of unit_iff_val_zero

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:22):

@Ashvni Narayanan If you want to treat val_ring K as a type then it would be better to define it as the subtype { x : K // 0 ≤ v x } (which is a type) rather than the subset { x : K | 0 ≤ v x } (which is only a term and not a type, and keeps having to be promoted to a type with a confusing little up-arrow)

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:22):

This can be summarised as "if you want to treat it as a set, don't define it as a subset"

view this post on Zulip Ashvni Narayanan (Jun 29 2020 at 11:23):

Scott Morrison said:

Were you hoping to see ⊢ α * α⁻¹ = 1?

Yes

view this post on Zulip Ashvni Narayanan (Jun 29 2020 at 11:25):

Kevin Buzzard said:

Ashvni Narayanan If you want to treat val_ring K as a type then it would be better to define it as the subtype { x : K // 0 ≤ v x } (which is a type) rather than the subset { x : K | 0 ≤ v x } (which is only a term and not a type, and keeps having to be promoted to a type with a confusing little up-arrow)

This gives me a lot of type mismatch errors, for example,

type mismatch at application
  is_add_subgroup (val_ring K)
term
  val_ring K
has type
  Type ? : Type (max 1 (?+1))
but is expected to have type
  set ?m_1 : Type ?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:26):

Yes, it will do.

view this post on Zulip Ashvni Narayanan (Jun 29 2020 at 11:26):

Ah, is this because it must not be treated as a subgroup, but as a group?

view this post on Zulip Ashvni Narayanan (Jun 29 2020 at 11:27):

Scott Morrison said:

It looks like α has been coerced to somewhere (you should work out where), then you've taken the inverse, and then you've put it back in ↥(val_ring K) by providing a proof which just appears as _.

I think it should be coerced to the field K, because that is where the inverse exists.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:29):

It seems to me that you are treating val_ring as an independent thing, rather than a subthing of a thing. Don't you have an error on is_unit alpha in the statement of your theorem? What's the first error in your file?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:29):

Not the one which confuses you, but the first one.

view this post on Zulip Ashvni Narayanan (Jun 29 2020 at 11:30):

Kevin Buzzard said:

It seems to me that you are treating val_ring as an independent thing, rather than a subthing of a thing. Don't you have an error on is_unit alpha in the statement of your theorem? What's the first error in your file?

I don't have any errors..

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:31):

Are you using the latest mathlib?

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:31):

I can't work with your file right now. If I cut and paste literally what you posted, I have errors.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:31):

If you cut and paste literally what you posted, do you get errors too?

view this post on Zulip Ashvni Narayanan (Jun 29 2020 at 11:33):

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

import tactic

universe u
noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(v : K -> with_top  )
(mul :  (x y : K), v(x*y) = v(x) + v(y) )
(add :  (x y : K), min (v(x)) (v(y))  v(x + y)  )
(non_zero :  (x : K), v(x) =   x = 0 )

namespace discrete_valuation_field

definition valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top  := v

variables {K : Type*} [field K] [discrete_valuation_field K]

lemma with_top.cases (a : with_top ) : a =    n : , a = n :=
begin
  cases a with n,
  { -- a = ⊤ case
    left,
    refl, -- true by definition
  },
  { -- ℤ case
    right,
    use n,
    refl, -- true by definition
  }
end

lemma sum_zero_iff_zero (a : with_top ) : a + a = 0  a = 0 :=
begin
  split,
  { -- the hard way
    intro h, -- h is a proof of a+a=0
    -- split into cases
    cases (with_top.cases a) with htop hn,
    { -- a = ⊤
      rw htop at h,
      -- h is false
      cases h,
      -- no cases!
    },
    { -- a = n
      cases hn with n hn,
      rw hn at h ,
      -- now h says n+n=0 and our goal is n=0
      -- but these are equalities in `with_top ℤ
      -- so we need to get them into ℤ
      -- A tactic called `norm_cast` does this
     norm_cast at h ,
      -- we finally have a hypothesis n + n = 0
      -- and a goal n = 0
      -- and everything is an integer
      rw add_self_eq_zero at h,
      assumption
    }
  },
   { -- the easy way
    intro ha,
    rw ha,
    simp
  }
end
 --Thanks Kevin!

lemma val_one_eq_zero : v(1 : K) = 0 :=
begin
have f : (1:K)*(1:K) = (1 : K),
simp,
have g : v(1 : K) = v((1 : K)*(1 : K)),
simp,
have k : v((1 : K)*(1 : K)) = v(1 : K) + v(1 : K),
{apply mul},
rw k at g,
rw g,
cases (with_top.cases (v(1:K))) with h1 h2,
{
rw h1,
rw h1 at g,
rw <-g,
rw non_zero at h1,
exfalso,
exact one_ne_zero h1,
},
cases h2 with n h2,
{
rw h2,
rw sum_zero_iff_zero,
rw h2 at g,
norm_cast at g,
simp,
linarith,
},
end

lemma val_minus_one_is_zero : v(-1 : K) = 0 :=
begin
have f : (-1:K)*(-1:K) = (1 : K),
simp,
have g : v((-1 : K)*(-1 : K)) = v(1 : K),
simp,
have k : v((-1 : K)*(-1 : K)) = v(-1 : K) + v(-1 : K),
{
  apply mul,
},
rw k at g,
rw val_one_eq_zero at g,
rw <-sum_zero_iff_zero,
exact g,
end

lemma val_zero : v(0:K) =  :=
begin
rw non_zero,
end


lemma with_top.transitivity (a b c : with_top  ) : a  b -> b  c -> a  c :=
begin
rintros,
cases(with_top.cases c) with h1 h2,
  {
    rw h1,
    simp,
  },
  {
    cases h2 with n h2,
    cases(with_top.cases a) with k1 k2,
    {
      rw [k1, h2],
      rw k1 at a_1,
      rw h2 at a_2,
      cases(with_top.cases b) with l1 l2,
      {
        rw l1 at a_2,
        exact a_2,
      },
      {
        cases l2 with m l2,
        rw l2 at a_1,
        exfalso,
        apply with_top.not_top_le_coe m,
        exact a_1,
      },
    },
    {
      cases k2 with m k2,
      cases(with_top.cases b) with l1 l2,
      {
        rw [l1,h2] at a_2,
        exfalso,
        apply with_top.not_top_le_coe n,
        exact a_2,
      },
      {
        cases l2 with k l2,
        rw [k2,l2] at a_1,
        rw [l2,h2] at a_2,
        rw [k2,h2],
        rw with_top.coe_le_coe,
        rw with_top.coe_le_coe at a_1,
        rw with_top.coe_le_coe at a_2,
        transitivity k,
        exact a_1,
        exact a_2,
      },
    },
  },
end

def val_ring (K : Type*) [field K] [discrete_valuation_field K] := { x : K | 0  v x }

instance (K : Type*) [field K] [discrete_valuation_field K] : is_add_subgroup (val_ring K) :=
{
  zero_mem := begin
              unfold val_ring,
              simp,
              rw val_zero,
              simp,
              end,
  add_mem := begin
            unfold val_ring,
            simp,
            rintros,
            have g : min (v(a)) (v(b))  v(a + b),
            {
              apply add,
            },
            rw min_le_iff at g,
            cases g,
            {
              apply with_top.transitivity,
              exact a_1,
              exact g,
            },
            {
              apply with_top.transitivity,
              exact a_2,
              exact g,
            },
            end,
  neg_mem := begin
            unfold val_ring,
            rintros,
            simp,
            simp at a_1,
            have f : -a = a * (-1 : K),
            {
              simp,
            },
            rw f,
            rw mul,
            rw val_minus_one_is_zero,
            simp,
            assumption,
            end,
}

instance (K:Type*) [field K] [discrete_valuation_field K] : is_submonoid (val_ring K) :=
{ one_mem := begin
            unfold val_ring,
            simp,
            rw val_one_eq_zero,
            norm_num,
            end,
  mul_mem := begin
            unfold val_ring,
            rintros,
            simp,
            simp at a_1,
            simp at a_2,
            rw mul,
            apply add_le_add' a_1 a_2,
            end, }

instance valuation_ring (K:Type*) [field K] [discrete_valuation_field K] : is_subring (val_ring K) :=
begin
refine is_subring.mk,
end

instance is_domain (K:Type*) [field K] [discrete_valuation_field K] : integral_domain (val_ring K) :=
begin
apply subring.domain (val_ring K),
end

lemma unit_iff_val_zero (K:Type*) [field K] [discrete_valuation_field K] [α : (val_ring K)] : v (α : K) = 0  is_unit α :=
begin
split,
{
  rintros,
  rw is_unit_iff_exists_inv,
  use α⁻¹,
  {
    unfold val_ring,
    simp,
    have f : v((α : K) * (α⁻¹ : K)) = 0,
    {
      rw mul_inv_cancel,
      {
        rw val_one_eq_zero,
      },
      {
        from λ h,
        by
        {
          rw [<-non_zero, a] at h,
          cases h,
        },
      },
    },
  rw mul at f,
  rw a at f,
  simp at f,
  rw f,
  norm_num,
  },
  {
    sorry,
  },
},
{
  rintros,
  rw is_unit_iff_exists_inv at a,
  cases a with b a,
  have f : v((α:K)*(b:K)) = v(1:K),
  {
    norm_cast,
    rw a,
    simp,
  },
  rw mul at f,
  rw val_one_eq_zero at f,
  rw add_eq_zero_iff' at f,
  {
    cases f,
    exact f_left,
  },
  {
    exact α.2,
  },
  {
    exact b.2,
  },
}
end
end discrete_valuation_field

This might help. It is the entire file.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 11:34):

I still get errors. You are probably using a different mathlib to me.

view this post on Zulip Ashvni Narayanan (Jun 30 2020 at 11:55):

I am trying to show that the valuation of a uniformiser is 1.

import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization
import tactic
universe u
noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(v : K -> with_top  )
(mul :  (x y : K), v(x*y) = v(x) + v(y) )
(add :  (x y : K), min (v(x)) (v(y))  v(x + y)  )
(non_zero :  (x : K), v(x) =   x = 0 )

namespace discrete_valuation_field

definition valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top  := v

variables {K : Type*} [field K] [discrete_valuation_field K]

def unif (K:Type*) [field K] [discrete_valuation_field K] : set K := { π | v π = 1 }

variables (π : K) ( : π  unif K)

lemma val_unif_eq_one : v(π) = 1 :=
begin
unfold unif at ,
end
end discrete_valuation_field

I get an error

get_local tactic failed, unknown 'hπ' local
state:
K : Type u_1,
_inst_4 : field K,
_inst_5 : discrete_valuation_field K,
π : K
 v π = 1

How can I rectify this? Any help is appreciated, thank you!

view this post on Zulip Johan Commelin (Jun 30 2020 at 12:16):

Put h\pi in the lemma statement, instead of variables

view this post on Zulip Johan Commelin (Jun 30 2020 at 12:16):

@Ashvni Narayanan If you introduce something with variables, then Lean will only use it if you mention it in the statement.

view this post on Zulip Johan Commelin (Jun 30 2020 at 12:17):

That's why it picks up \pi, but not h\pi.

view this post on Zulip Johan Commelin (Jun 30 2020 at 12:17):

Variables usually work well for types, and terms of types, but not for assumptions like h\pi. Those are better stated directly in the statement of the lemma

view this post on Zulip Ashvni Narayanan (Jun 30 2020 at 12:25):

Oh, I see. Thank you!

view this post on Zulip Reid Barton (Jun 30 2020 at 12:45):

Actually a variable will be included if it is used in the body too, but not inside a tactic block. (Because Lean doesn't know which tokens inside the tactic block are names until it's too late.)
You can also use include to force a variable to be included in subsequent top-level definitions, but beware of accidentally includeing it in lemmas where you don't want it!

view this post on Zulip Ashvni Narayanan (Jun 30 2020 at 16:01):

Oh ok, thank you!

view this post on Zulip Ashvni Narayanan (Jun 30 2020 at 16:21):

I am trying to prove that for n a natural number, ↑n ≠ ⊤ :

import order.bounded_lattice

universe u

lemma nat_neq_top (n :) : (n:with_top )   :=
begin
intro,
apply with_top.coe_ne_top,
rw <-a,
sorry,
end

I have the goals:

2 goals
n : ,
a : n = 
 ↑?m_1 = n

n : ,
a : n = 
 

I don't know how to proceed from here, I think it means that I need to show n is an integer, which can possibly be done by int.coe_nat_eq , but that does not work out.
Any help is appreciated. Thank you!

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:22):

Does with_top.coe_ne_top take an argument? If so, you could try to pass it n.

view this post on Zulip Ashvni Narayanan (Jun 30 2020 at 16:35):

lemma nat_neq_top (n :) : (n:with_top )   :=
begin
intro,
apply with_top.coe_ne_top n,
exact ,
exact n,
split,
intro,
rw <-a,
rw int.coe_nat_eq,
sorry,
end

This is as far as I can get..

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:39):

lemma nat_neq_top (n :) : (n : with_top )   :=
begin
  have := @with_top.coe_ne_top  n,
  convert this using 1,

end

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:39):

Unfortunately there don't seem to be lemmas for \u \u n = \u n.

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:39):

Which is a hole in the with_top API that should be fixed first.

view this post on Zulip Bryan Gin-ge Chen (Jun 30 2020 at 16:41):

Doesn't this just work?

import order.bounded_lattice

lemma nat_neq_top (n :) : (n:with_top )   :=
with_top.coe_ne_top

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:42):

Unfortunately not.

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:42):

It would if n : int of course

view this post on Zulip Bryan Gin-ge Chen (Jun 30 2020 at 16:43):

Strange, I don't see any errors in my Lean.

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:43):

type mismatch, term
  with_top.coe_ne_top
has type
  ↑?m_2  
but is expected to have type
  n  

view this post on Zulip Ashvni Narayanan (Jun 30 2020 at 16:44):

Yeah, I get the same error

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:44):

This is on a mathlib that is more than 3 hours old, I admit

view this post on Zulip Bryan Gin-ge Chen (Jun 30 2020 at 16:44):

Did I copy and paste something wrong? I don't see any errors in the web editor either.

view this post on Zulip Ashvni Narayanan (Jun 30 2020 at 16:45):

Or maybe, I could possibly avoid this if I could work with \pi^n, with n \in \Z.
Is that possible?

view this post on Zulip Bryan Gin-ge Chen (Jun 30 2020 at 16:45):

My "playground" project is apparently on commit 35fbfe0a40395e6ea394f05b1c56a2fbcf4b33ce from 2 days ago.

view this post on Zulip Bryan Gin-ge Chen (Jun 30 2020 at 16:45):

The web editor is on this commit from 14 hours ago.

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:48):

Crazy :confused:

view this post on Zulip Bryan Gin-ge Chen (Jun 30 2020 at 16:52):

#3132 (merged 7 days ago) looks related, possibly?

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:54):

commit 9acf5903f385e2c017cde4b93d2323d59232707a (origin/master, origin/HEAD, master)
Author: Yakov Pechersky <yakov@pechersky.us>
Date:   Mon Jun 29 03:57:10 2020 +0000

    feat(data/matrix/notation): smul matrix lemmas (#3208)

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:54):

That's from yesterday

view this post on Zulip Bryan Gin-ge Chen (Jun 30 2020 at 16:55):

I think maybe it's #3157?

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:57):

Aha, that makes sense

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:57):

@Ashvni Narayanan Please try updating mathlib. It might solve your problem (-;

view this post on Zulip Adam Topaz (Jun 30 2020 at 16:57):

This also works:

lemma nat_neq_top (n :ℕ) : (n : with_top ℤ) ≠ ⊤ := by apply with_top.coe_ne_top

view this post on Zulip Johan Commelin (Jun 30 2020 at 16:58):

That's what Bryan already wrote. But it depends on having today's mathlib, not yesterdays.

view this post on Zulip Adam Topaz (Jun 30 2020 at 16:58):

Oh sorry :)

view this post on Zulip Ashvni Narayanan (Jun 30 2020 at 17:23):

Oh ok, I will do that. Thank you!

view this post on Zulip Ashvni Narayanan (Jul 02 2020 at 15:22):

https://github.com/laughinggas/DVR/blob/cc3a8e881c914fa17f9bde07fbcead8850f9152f/src/Test.lean#L598

I am trying to prove Line 598. Line 608 gives me an error, I don't know how to use the lemma val_int_power then.
Any help is appreciated. Thank you!

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 20:36):

α⁻¹ is notation for has_inv.inv α. And α ^(-1) is notation for has_pow.pow α (-1). They're not the same, so this is why the rewrite failed.

view this post on Zulip Kevin Buzzard (Jul 02 2020 at 20:40):

After unfold val_ring you can do

      suffices : 0  v (α ^ (-1 : )),
        simpa,

and then your rewrite will work

view this post on Zulip Ashvni Narayanan (Jul 03 2020 at 00:10):

Thank you!

view this post on Zulip Ashvni Narayanan (Jul 04 2020 at 01:52):

import ring_theory.ideals
import ring_theory.principal_ideal_domain
import ring_theory.localization
import tactic
import order.bounded_lattice
import algebra.field_power
universe u

noncomputable theory
open_locale classical
class discrete_valuation_field (K : Type*) [field K] :=
(v : K -> with_top  )
(mul :  (x y : K), v(x*y) = v(x) + v(y) )
(add :  (x y : K), min (v(x)) (v(y))  v(x + y)  )
(non_zero :  (x : K), v(x) =   x = 0 )

namespace discrete_valuation_field

definition valuation (K : Type*) [field K] [ discrete_valuation_field K ] : K -> with_top  := v
variables {K : Type*} [field K] [discrete_valuation_field K]
def val_ring (K : Type*) [field K] [discrete_valuation_field K] := { x : K | 0  v x }

lemma ideal_is_unif_power (S : ideal (val_ring K)) (x  S) :  n : , (n : with_top )  v(x : K) :=
begin
sorry,
end

lemma ideal_is_unique_unif_power (S : ideal (val_ring K)) (x  S) : ∃! n : , (n : with_top )  v(x : K) :=
begin
split,
{
  cases ideal_is_unif_power S x H with m g,
  simp,
  split,
  {
sorry,
},
sorry,
},
end

The goal is:

K : Type u_1,
_inst_4 : field K,
_inst_5 : discrete_valuation_field K,
S : ideal (val_ring K),
x : (val_ring K),
H : x  S,
m : ,
g : m  v x
 ↑?m_1  v x

I want to use g, but apply does not seem to work out. Any help is appreciated. Thank you!


view this post on Zulip Adam Topaz (Jul 04 2020 at 02:18):

Does exact g work?

view this post on Zulip Adam Topaz (Jul 04 2020 at 02:21):

Wait, isn't your lemma false? Why should n be unique?

view this post on Zulip Mario Carneiro (Jul 04 2020 at 02:23):

The problem is that m is out of scope of the metavariable

view this post on Zulip Mario Carneiro (Jul 04 2020 at 02:23):

You tried to intro the exists before you have m available

view this post on Zulip Mario Carneiro (Jul 04 2020 at 02:24):

If you move the cases line to the beginning then exact g works

view this post on Zulip Ashvni Narayanan (Jul 04 2020 at 02:25):

Thank you!

view this post on Zulip Ashvni Narayanan (Jul 04 2020 at 02:26):

Adam Topaz said:

Wait, isn't your lemma false? Why should n be unique?

Thanks for pointing this out, you are correct, I forgot to put in additional conditions.

view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 22:16):

I am trying to state the following lemma , for a discrete valuation field K, and a uniformiser π in K :

lemma contains_unif_power ( : π  unif K) (S : ideal(val_ring K)) :  n : , (π^n)  S :=

This statement gives me the error:

failed to synthesize type class instance for
K : Type u_1,
_inst_4 : field K,
_inst_5 : discrete_valuation_field K,
π : K,
 : π  unif K,
S : ideal (val_ring K),
n : 
 has_mem K (ideal (val_ring K))

Is this because S is not realised as a subset of K? If so, is there any way around this?
Any help is appreciated, thank you!

view this post on Zulip Adam Topaz (Jul 06 2020 at 22:31):

You would need to either map S back to K using something like set.image, or use a proof that \pi^n is in the valuation ring. (Also, the lemma is false for the trivial ideal.)

view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 22:47):

Thanks! How can I put in the nontrivial condition?

view this post on Zulip Kevin Buzzard (Jul 06 2020 at 22:48):

Ideals are a lattice, so I \ne \bot is the preferred way to say I isn't the zero ideal.

view this post on Zulip Adam Topaz (Jul 06 2020 at 22:48):

Add an assumption S ≠ ⊥

view this post on Zulip Adam Topaz (Jul 06 2020 at 22:49):

And as for the membership issue: ∃ n : ℕ, π^n ∈ set.range (λ s : S, (s : K))

view this post on Zulip Adam Topaz (Jul 06 2020 at 22:50):

That at least typechecks. There are other possibilities as well.

view this post on Zulip Ashvni Narayanan (Jul 06 2020 at 22:57):

Yeah, I guess an equivalent lemma would be to show the ideal spanned by \pi^n lies inside S, which would involve showing \pi^n is in val_ring K.

view this post on Zulip Ashvni Narayanan (Jul 08 2020 at 00:22):

Is there a way to change S ≠ ⊥ to ∃ x ∈ S, x ≠ 0 ?
I only see exists_mem_ne_zero_of_ne_bot, but this does not work. I am trying to prove,

K: Type u_1
_inst_4: field K
_inst_5: discrete_valuation_field K
π: K
: π  unif K
S: ideal (val_ring K)
Q: set  := {n :  |  (x : (val_ring K)) (H : x  S), n = v x}
h: S  
 Q.nonempty

view this post on Zulip Reid Barton (Jul 08 2020 at 00:24):

What doesn't work and what is the error message

view this post on Zulip Adam Topaz (Jul 08 2020 at 00:28):

Does exists_mem_ne_zero_of_ne_bot assume that the ring is a field?

view this post on Zulip Adam Topaz (Jul 08 2020 at 00:28):

That may be the issue.

view this post on Zulip Ashvni Narayanan (Jul 08 2020 at 00:28):

have f : exists_mem_ne_zero_of_ne_bot h,

does not work.
exists_mem_ne_zero_of_ne_bot does not work, but I cannot expect it to work, because it is for fields, and I am not dealing with fields. I get the error :

type mismatch at application
  exists_mem_ne_zero_of_ne_bot h
term
  h
has type
  S  
but is expected to have type
  ?m_6  

which is understandable. Is there any other way to get from S ≠ ⊥ to ∃ x ∈ S, x ≠ 0 ?
Thank you!

view this post on Zulip Bhavik Mehta (Jul 08 2020 at 00:30):

It looks like there ought to be a lemma saying an ideal is bot iff all its elements are 0

view this post on Zulip Adam Topaz (Jul 08 2020 at 00:31):

The lemma exists_mem_ne_zero_of_ne_bot should be true for submoddules of any module over a ring in which 101 \neq 0, but it's done in mathlib for vector spaces.

view this post on Zulip Reid Barton (Jul 08 2020 at 00:31):

It should even be true for the zero ring right? because then there is no ideal other than bot

view this post on Zulip Adam Topaz (Jul 08 2020 at 00:32):

yeah true.

view this post on Zulip Adam Topaz (Jul 08 2020 at 00:32):

in that case everything is bot :)

view this post on Zulip Adam Topaz (Jul 08 2020 at 00:35):

The same exact proof works in general:

import algebra
import linear_algebra

variables {R : Type*} [ring R]
variables {M : Type*} [add_comm_group M] [module R M]

lemma exists_mem_ne_zero_of_ne_bot {s : submodule R M} (h : s  ) :  b : M, b  s  b  0 :=
begin
  classical,
  by_contradiction hex,
  have : xs, (x:M) = 0, { simpa only [not_exists, not_and, not_not, ne.def] using hex },
  exact (h $ bot_unique $ assume s hs, (submodule.mem_bot R).2 $ this s hs)
end

view this post on Zulip Mario Carneiro (Jul 08 2020 at 00:41):

I think contrapose! should do this pretty easily

view this post on Zulip Adam Topaz (Jul 08 2020 at 00:42):

I just copied the proof from mathlib :)

view this post on Zulip Adam Topaz (Jul 08 2020 at 00:42):

Except I changed the field to a ring

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:19):

I am trying to apply a transitivity argument :

K: Type u_1
_inst_4: field K
_inst_5: discrete_valuation_field K
π: K
: π  unif K
S: ideal (val_ring K)
h: ¬S = 
Q: set  := {n :  |  (x : (val_ring K)) (H : x  S), n = v x}
g: v (π ^ Inf Q) = (Inf Q)
nz: π ^ Inf Q  0
x: (val_ring K)
z: (val_ring K)
f_right: v z = v (π ^ Inf Q)
f_left: submodule.span (val_ring K) {z}  S
l: submodule.span (val_ring K) {π ^ Inf Q}  submodule.span (val_ring K) {z}
 submodule.span (val_ring K) {π ^ Inf Q, _⟩}  S

Using

transitivity submodule.span (val_ring K) {z},

gives me an error

invalid apply tactic, failed to unify
  submodule.span (val_ring K) {π ^ Inf Q, _⟩}  S
with
  ?m_3  ?m_4  ?m_4  ?m_5  ?m_3  ?m_5

Any help is appreciated, thank you!

view this post on Zulip Reid Barton (Jul 09 2020 at 14:22):

Looks like the apply bug again

view this post on Zulip Reid Barton (Jul 09 2020 at 14:23):

I would just build the term manually: refine le_trans l _

view this post on Zulip Reid Barton (Jul 09 2020 at 14:23):

oh, you have both parts already

view this post on Zulip Jalex Stark (Jul 09 2020 at 14:28):

does linarith close it?

view this post on Zulip Reid Barton (Jul 09 2020 at 14:28):

exact le_trans l f_left

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:29):

Reid Barton said:

exact le_trans l f_left

This gives me the error:

type mismatch at application
  le_trans l
term
  l
has type
  submodule.span (val_ring K) {π ^ Inf Q}  submodule.span (val_ring K) {z}
but is expected to have type
  submodule.span (val_ring K) {π ^ Inf Q, _⟩}  ?m_1

view this post on Zulip Reid Barton (Jul 09 2020 at 14:29):

OK, well I don't know what this is but then you need to fix this anyways.

view this post on Zulip Reid Barton (Jul 09 2020 at 14:29):

You can try convert instead of exact.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:30):

Jalex Stark said:

does linarith close it?

No, this gives the error,

invalid type ascription, term has type
  ?m_3  ?m_4
but is expected to have type
  submodule.span (val_ring K) {π ^ Inf Q, _⟩}  S

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:34):

Reid Barton said:

You can try convert instead of exact.

This gives me a goal :

 (val_ring K) = K

view this post on Zulip Johan Commelin (Jul 09 2020 at 14:34):

Which is false... so you need to backtrack.

view this post on Zulip Adam Topaz (Jul 09 2020 at 14:36):

It looks like a subtype thing again... π ^ Inf Q vs ⟨π ^ Inf Q, _⟩

view this post on Zulip Johan Commelin (Jul 09 2020 at 14:36):

Yup. Can you convert (some stuff) using 1

view this post on Zulip Johan Commelin (Jul 09 2020 at 14:36):

The using 1 will make it less aggresive.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:51):

Is there a way to apply

using 1

to a goal of the form

 {π ^ Inf Q, _⟩}  S

?

view this post on Zulip Johan Commelin (Jul 09 2020 at 14:53):

I don't know what that means.

view this post on Zulip Johan Commelin (Jul 09 2020 at 14:53):

What did your goal look like after the convert .... using 1?

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:55):

I actually managed to get it down to

K: Type u_1
_inst_4: field K
_inst_5: discrete_valuation_field K
π: K
: π  unif K
S: ideal (val_ring K)
h: ¬S = 
Q: set  := {n :  |  (x : (val_ring K)) (H : x  S), n = v x}
g: v (π ^ Inf Q) = (Inf Q)
nz: π ^ Inf Q  0
x: (val_ring K)
a: {π ^ Inf Q, _⟩}  S  x  S
z: (val_ring K)
f_left: z  S
w: K
f_1: w  val_ring K
f_2: v w = 0
f_3: z * w = π ^ Inf Q
 {π ^ Inf Q, _⟩}  S

which seems like an easier thing to show.

view this post on Zulip Johan Commelin (Jul 09 2020 at 14:57):

There must be a lemma singleton_subset or singleton_subset_iff

view this post on Zulip Johan Commelin (Jul 09 2020 at 14:57):

Does simp help you here?

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:57):

Johan Commelin said:

What did your goal look like after the convert .... using 1?

 submodule.span (val_ring K) {π ^ Inf Q, _⟩} = submodule.span (val_ring K) {π ^ Inf Q}

view this post on Zulip Johan Commelin (Jul 09 2020 at 14:59):

Aha, and with using 2?

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 14:59):

Johan Commelin said:

Does simp help you here?

No

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 15:04):

Johan Commelin said:

What did your goal look like after the convert .... using 1?

This also gives 2 more goals:

 has_singleton K (set (val_ring K))

view this post on Zulip Johan Commelin (Jul 09 2020 at 15:05):

Aha, we clearly don't want that.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 15:05):

using 2 gives

 {π ^ Inf Q, _⟩} = {π ^ Inf Q}

plus

 has_singleton K (set (val_ring K))

twice.

view this post on Zulip Johan Commelin (Jul 09 2020 at 15:05):

So let's move back to the inclusion that you had reduced the goal to.

view this post on Zulip Kenny Lau (Jul 09 2020 at 15:14):

if you livestream in discord then we can compete to tell you the tactic you need!

view this post on Zulip Adam Topaz (Jul 09 2020 at 15:15):

Something strange must have happened, since submodule.span ↥(val_ring K) {π ^ Inf Q} shouldn't even make sense! π ^ Inf Q is a term of type K, that's why it's asking for the has_singleton instance.

view this post on Zulip Adam Topaz (Jul 09 2020 at 15:16):

Where did your assumption l come from?

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 15:23):

I had not solved l, just put a sorry. :(

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 15:24):

Ashvni Narayanan said:

I actually managed to get it down to

K: Type u_1
_inst_4: field K
_inst_5: discrete_valuation_field K
π: K
: π  unif K
S: ideal (val_ring K)
h: ¬S = 
Q: set  := {n :  |  (x : (val_ring K)) (H : x  S), n = v x}
g: v (π ^ Inf Q) = (Inf Q)
nz: π ^ Inf Q  0
x: (val_ring K)
a: {π ^ Inf Q, _⟩}  S  x  S
z: (val_ring K)
f_left: z  S
w: K
f_1: w  val_ring K
f_2: v w = 0
f_3: z * w = π ^ Inf Q
 {π ^ Inf Q, _⟩}  S

which seems like an easier thing to show.

This has no sorries.

view this post on Zulip Adam Topaz (Jul 09 2020 at 15:27):

You can certainly solve this goal, but it looks like might want to first change ⟨π ^ Inf Q, _⟩ to z * ⟨w, f_1⟩ where the multiplication takes place in the valuation ring, so that you can apply the ideal condition for S.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 15:36):

How can I do this? Using a subtype argument at f_3?

view this post on Zulip Johan Commelin (Jul 09 2020 at 15:37):

I think I would go for rw singleton_subset_iff

view this post on Zulip Adam Topaz (Jul 09 2020 at 15:37):

Well, first try to reduce to proving that the element is in S using singleton_subset_iff, as Johan suggested. Then rewrite using f_3 and go from there.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 16:09):

rw singleton_subset_iff
simp only [submodule.mem_coe],

brings it down to

z: (val_ring K)
f_left: z  S
w: K
f_1: w  val_ring K
f_2: v w = 0
f_3: z * w = π ^ Inf Q
 π ^ Inf Q, _⟩  S

rw <-f_3 does not work, it gives the error :

rewrite tactic failed, motive is not type correct
  λ (_a : K), π ^ Inf Q, _⟩  S = (⟨_a, _⟩  S)

:(

view this post on Zulip Adam Topaz (Jul 09 2020 at 16:26):

I don't know what that means. Does lean know how to fill the hole in the ⟨π ^ Inf Q, _⟩?

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 16:40):

I don't know, but I don't think so. Is there a way to check this?

view this post on Zulip Alex J. Best (Jul 09 2020 at 16:45):

When the _ is in the goal or a hypothesis like this it probably isn't a hole, but rather a proof lean has elected not to display, try set_option pp.proofs true to see it

view this post on Zulip Adam Topaz (Jul 09 2020 at 16:46):

The context doesn't seem to know that π ^ Inf Q is in the valuation ring.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 16:46):

By definition, it is not.

view this post on Zulip Alex J. Best (Jul 09 2020 at 16:47):

Can someone paste some code I can try?

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 16:50):

https://github.com/laughinggas/DVR/blob/86c6dad4514e328c49b62300f1546c15d773b10c/src/Test.lean#L967

view this post on Zulip Adam Topaz (Jul 09 2020 at 17:09):

On line 834, you write use π^(Inf Q)but this is something in K a priori. This might be the issue...
(nevermind -- ignore this)

view this post on Zulip Alex J. Best (Jul 09 2020 at 17:09):

Thanks, love the github username lol.
You can use simp_rw [← f_3], to rewrite f_3 here, its a version of rw that works more like simp so its a bit better at rewriting things that are in a more complicated term.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 17:14):

Adam Topaz said:

On line 834, you write use π^(Inf Q)but this is something in K a priori. This might be the issue...
(nevermind -- ignore this)

As soon as I use this, the first goal is to check that it is in val_ring K.

view this post on Zulip Adam Topaz (Jul 09 2020 at 17:15):

Yeah I just noticed that. Ignore what I said.

view this post on Zulip Johan Commelin (Jul 09 2020 at 18:04):

@Ashvni Narayanan What is your goal now?

view this post on Zulip Johan Commelin (Jul 09 2020 at 18:05):

Or is this solved by now?

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 18:05):

No it is not :(

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 18:07):

z: (val_ring K)
f_left: z  S
w: K
f_1: w  val_ring K
f_2: v w = 0
f_3: z * w = π ^ Inf Q
 z * w, _⟩  S

This is the goal

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 18:11):

I was trying to use

ideal.mul_mem_left

at f_1, but w does not have type val_ring K, which causes an issue.

view this post on Zulip Adam Topaz (Jul 09 2020 at 18:13):

Try change z * \<w,f_1\> \in S

view this post on Zulip Adam Topaz (Jul 09 2020 at 18:14):

I'm not sure if that will help.

view this post on Zulip Johan Commelin (Jul 09 2020 at 18:17):

apply S.mul_mem_right f_left?

view this post on Zulip Johan Commelin (Jul 09 2020 at 18:17):

Or something like that.

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 18:21):

Yes, that works. Thank you so much!

view this post on Zulip Ashvni Narayanan (Jul 09 2020 at 18:21):

Adam Topaz said:

Try change z * \<w,f_1\> \in S

It helped, thank you!

view this post on Zulip Ashvni Narayanan (Jul 10 2020 at 17:42):

instance is_dvr (K:Type*) [field K] [discrete_valuation_field K] : discrete_valuation_ring (val_ring K) :=
{
  prime_ideal' := begin
                  have  :  π : K, v(π) = 1,
                  {
                    cases hv 1 with π hv,
                    use π,
                    rw hv,
                  },
                  cases  with π ,
                  use submodule.span (val_ring K) {π},
                  end
}

This is not a mwe. The

cases  with π ,

line gives me an error :

induction tactic failed, recursor 'Exists.dcases_on' can only eliminate into Prop
state:
K : Type ?,
_inst_6 : field K,
_inst_7 : discrete_valuation_field K,
 :  (π : K), v π = 1
 ideal (val_ring K)

I don't understand why, because I have used exactly the same code elsewhere and it did not create any issues.
Any help is appreciated, thank you!

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:47):

That probably means that your goal is not a proposition

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:48):

Your definition of the prime ideal is data so should really be done in term mode

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:49):

You should probably prove the lemma beforehand, that there exists pi with valuation 1

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:49):

And then use classical.some to define the prime ideal in one line

view this post on Zulip Ashvni Narayanan (Jul 10 2020 at 17:52):

Oh alright, thank you!

view this post on Zulip Reid Barton (Jul 10 2020 at 17:53):

It's probably better to define it in some more obviously invariant way, like the span of all elements of valuation 1, or just the set of elements of positive valuation (right?)

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:55):

That's a good idea

view this post on Zulip Reid Barton (Jul 10 2020 at 17:55):

Then you can prove it's also spanned by any element of valuation 1

view this post on Zulip Kevin Buzzard (Jul 10 2020 at 17:58):

So then when you make the definition, you can define the set (which is data) directly, and then prove that it's an ideal in tactic mode and you won't get the weird error


Last updated: May 06 2021 at 17:38 UTC