Stream: maths

Topic: DVRs

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?

Johan Commelin (Feb 13 2020 at 19:46):

Well, we already have local_ring

Johan Commelin (Feb 13 2020 at 19:46):

So maybe you should extend that

Johan Commelin (Feb 13 2020 at 19:46):

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

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?

Johan Commelin (Feb 13 2020 at 19:49):

You are already extending that, right?

Johan Commelin (Feb 13 2020 at 19:49):

I meant, in addition, extend local ring

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...

Johan Commelin (Feb 13 2020 at 19:51):

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

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.

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

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)


Johan Commelin (Feb 13 2020 at 20:16):

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

Johan Commelin (Feb 13 2020 at 20:16):

exists_nonzero_nonunit?

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 $\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.

Ashwin Iyengar (Apr 26 2020 at 13:02):

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

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...

Kenny Lau (Apr 26 2020 at 13:39):

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

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?

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?

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

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...

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.

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

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

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

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.

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...)?

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')


Ashwin Iyengar (Apr 26 2020 at 16:47):

so it records some data

Ashwin Iyengar (Apr 26 2020 at 16:48):

a PID with a unique nonzero prime ideal

Johan Commelin (Apr 26 2020 at 16:50):

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

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

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.

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?

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.

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

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...

Kevin Buzzard (Apr 26 2020 at 17:03):

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

Kevin Buzzard (Apr 26 2020 at 17:04):

It's either that or make add_group_with_zero

Johan Commelin (Apr 26 2020 at 17:04):

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

Kevin Buzzard (Apr 26 2020 at 17:04):

Or with infinity or whatever

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

Johan Commelin (Apr 26 2020 at 17:04):

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

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

Kevin Buzzard (Apr 26 2020 at 17:05):

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

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?

norms...

Ashwin Iyengar (Apr 26 2020 at 17:08):

I would be happy with multiplicative $\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?

Johan Commelin (Apr 26 2020 at 17:09):

There are ways around that.

Johan Commelin (Apr 26 2020 at 17:10):

We could define free_group, or something like that.

Johan Commelin (Apr 26 2020 at 17:10):

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

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...

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.

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.

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.

Johan Commelin (Apr 26 2020 at 17:15):

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

Johan Commelin (Apr 26 2020 at 17:16):

(Say some subset of the reals)

Johan Commelin (Apr 26 2020 at 17:16):

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

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.

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

Johan Commelin (Apr 27 2020 at 07:45):

I'll try to prioritise these PRs

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!

Johan Commelin (Jun 11 2020 at 12:19):

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

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.

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:

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?

Johan Commelin (Jun 11 2020 at 14:00):

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

Johan Commelin (Jun 11 2020 at 14:00):

That makes R an explicit variable of is_uniformizer.

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*}

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

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!

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?

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)

Johan Commelin (Jun 13 2020 at 11:46):

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

Ashvni Narayanan (Jun 13 2020 at 11:46):

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


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

Ashvni Narayanan (Jun 13 2020 at 12:00):

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

Johan Commelin (Jun 13 2020 at 12:13):

@Chris Hughes Should submodule.is_prinicipal be a class?

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


This is not nice

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?

Johan Commelin (Jun 13 2020 at 12:17):

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

Johan Commelin (Jun 13 2020 at 12:17):

But I agree with the point

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.

Johan Commelin (Jun 13 2020 at 12:23):

@Mario Carneiro what's going on here?

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


Mario Carneiro (Jun 13 2020 at 12:28):

what's the question?

Johan Commelin (Jun 13 2020 at 12:29):

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

Mario Carneiro (Jun 13 2020 at 12:29):

Is it about unbundling ring classes into mixins?

Johan Commelin (Jun 13 2020 at 12:29):

It's about inferred instances not being defeq

Mario Carneiro (Jun 13 2020 at 12:30):

aha, this came up not too long ago

Johan Commelin (Jun 13 2020 at 12:31):

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

Johan Commelin (Jun 13 2020 at 12:31):

With alternating old and new structures?

Mario Carneiro (Jun 13 2020 at 12:31):

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

Mario Carneiro (Jun 13 2020 at 12:32):

It's actually a kind of fundamental problem

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

Mario Carneiro (Jun 13 2020 at 12:34):

it also doesn't work for instances that are variables

Johan Commelin (Jun 13 2020 at 12:36):

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

Mario Carneiro (Jun 13 2020 at 12:38):

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

Johan Commelin (Jun 13 2020 at 12:39):

But new structure were introduced for a reason, right?

Johan Commelin (Jun 13 2020 at 12:39):

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

Johan Commelin (Jun 13 2020 at 12:39):

And the hierarchy is far from finished.

Johan Commelin (Jun 13 2020 at 12:40):

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

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?

Johan Commelin (Jun 13 2020 at 12:41):

I think that would be a good idea.

Johan Commelin (Jun 13 2020 at 12:44):

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

Mario Carneiro (Jun 13 2020 at 12:44):

Oh wait, discrete_valuation_ring is actually broken

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


Mario Carneiro (Jun 13 2020 at 12:45):

note the separate appearance of comm_ring R and integral_domain R

Mario Carneiro (Jun 13 2020 at 12:45):

the unification problem fails because it's actually false

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?

Mario Carneiro (Jun 13 2020 at 12:46):

the double extends

Johan Commelin (Jun 13 2020 at 12:47):

Shouldn't old_structure_cmd take care of that?

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

Kevin Buzzard (Jun 13 2020 at 12:47):

Which structure isn't old?

Both, I think

Mario Carneiro (Jun 13 2020 at 12:48):

local_ring and principal_ideal_domain are both new structures

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

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

Mario Carneiro (Jun 13 2020 at 12:49):

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

Mario Carneiro (Jun 13 2020 at 12:49):

the compilation here is pretty unquestionably wrong

Kevin Buzzard (Jun 13 2020 at 12:54):

What is the Lean 3 idiomatic way to proceed?

Kevin Buzzard (Jun 13 2020 at 12:55):

Is there any harm in just making them old structures?

Johan Commelin (Jun 13 2020 at 12:56):

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

Johan Commelin (Jun 13 2020 at 12:56):

Mario wants to fix lean instead.

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

Mario Carneiro (Jun 13 2020 at 13:01):

possibly also structure literals are affected

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

Mario Carneiro (Jun 13 2020 at 13:03):

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

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

Kevin Buzzard (Jun 13 2020 at 14:33):

So what do we do?

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?

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


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?

Kevin Buzzard (Jun 16 2020 at 00:35):

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

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?

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.

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.

Scott Morrison (Jun 16 2020 at 01:50):

Similarly for is_local

Adam Topaz (Jun 16 2020 at 02:10):

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:

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)

Bhavik Mehta (Jun 16 2020 at 02:31):

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

Kenny Lau (Jun 16 2020 at 02:36):

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

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...

Kenny Lau (Jun 16 2020 at 05:03):

how about is_ring and is_comm_ring predicated on semirings

Kenny Lau (Jun 16 2020 at 05:05):

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

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

Why?

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.

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...

Johan Commelin (Jun 16 2020 at 15:18):

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

Johan Commelin (Jun 16 2020 at 15:18):

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

(deleted)

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.

Johan Commelin (Jun 16 2020 at 15:19):

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

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

Johan Commelin (Jun 16 2020 at 15:21):

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

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.

Kenny Lau (Jun 16 2020 at 15:21):

I guess we would want CDVRs as well

Kenny Lau (Jun 16 2020 at 15:22):

and a proof that they are henselian

Adam Topaz (Jun 16 2020 at 15:22):

What does CDVR stand for?

Kevin Buzzard (Jun 16 2020 at 15:22):

CDVR could also be a predicate

complete DVR

ah ok.

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]


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"

Johan Commelin (Jun 16 2020 at 15:23):

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

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

Kevin Buzzard (Jun 16 2020 at 15:23):

i.e. there's still something missing

Johan Commelin (Jun 16 2020 at 15:23):

Ooh, right, we need another compatibility class.

Kevin Buzzard (Jun 16 2020 at 15:24):

distrib++

Johan Commelin (Jun 16 2020 at 15:24):

I guess we could add is_cdvr which extends complete_space and is_dvr

Kevin Buzzard (Jun 16 2020 at 15:24):

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

Nope...

Johan Commelin (Jun 16 2020 at 15:24):

Because Z_p

Kevin Buzzard (Jun 16 2020 at 15:24):

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

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?

Johan Commelin (Jun 16 2020 at 15:25):

Will that play nice with the rest of the topology?

Adam Topaz (Jun 16 2020 at 15:25):

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

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

Johan Commelin (Jun 16 2020 at 15:26):

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

Ashvni Narayanan (Jun 16 2020 at 15:26):

10 equivalent definitions for DVRs?

Kevin Buzzard (Jun 16 2020 at 15:26):

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

Kevin Buzzard (Jun 16 2020 at 15:26):

Yes, there are 10 definitions of DVR on Wikipedia

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

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.

Kevin Buzzard (Jun 16 2020 at 15:29):

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

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


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


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

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?

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?

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?

Kevin Buzzard (Jun 16 2020 at 15:34):

is_local_ring isn't a class

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?

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.

Kevin Buzzard (Jun 16 2020 at 15:37):

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

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

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

Kevin Buzzard (Jun 16 2020 at 15:38):

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

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.

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.

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!

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

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.

Johan Commelin (Jun 16 2020 at 16:13):

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

Kevin Buzzard (Jun 16 2020 at 16:15):

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

Johan Commelin (Jun 16 2020 at 16:16):

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

Johan Commelin (Jun 16 2020 at 16:16):

So the class lives in Prop instead of Type*

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?

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.

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.

Reid Barton (Jun 16 2020 at 16:25):

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

Reid Barton (Jun 16 2020 at 16:26):

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

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].

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).

Kevin Buzzard (Jun 16 2020 at 17:06):

So do you want is_PIR and is_PID?

Johan Commelin (Jun 16 2020 at 17:08):

No, only is_PIR

Johan Commelin (Jun 16 2020 at 17:08):

Because it covers everything

Johan Commelin (Jun 16 2020 at 17:09):

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

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?"

Johan Commelin (Jun 16 2020 at 17:10):

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

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?

Johan Commelin (Jun 16 2020 at 17:15):

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

Johan Commelin (Jun 16 2020 at 17:15):

But at the moment I would go for maximum flexibility.

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


Scott Morrison (Jun 17 2020 at 15:25):

A #mwe needs imports!

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)

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) _)))


Johan Commelin (Jun 17 2020 at 16:24):

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

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:

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.

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).

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!

Jalex Stark (Jun 18 2020 at 23:38):

the second line has two binders

Jalex Stark (Jun 18 2020 at 23:39):

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

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 )


Reid Barton (Jun 18 2020 at 23:41):

Always look at the first error

Thank you!

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 )


Ashvni Narayanan (Jun 18 2020 at 23:46):

what does open_locale classical do?

Jalex Stark (Jun 18 2020 at 23:47):

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

Jalex Stark (Jun 18 2020 at 23:47):

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

Jalex Stark (Jun 18 2020 at 23:49):

(important edit to the previous post)

Thank you!

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

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.

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

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.

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 -> ℤ ∨ ∞)


Jalex Stark (Jun 19 2020 at 00:05):

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 )


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


Jalex Stark (Jun 19 2020 at 00:06):

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

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.

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.

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

Jalex Stark (Jun 19 2020 at 00:09):

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

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

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.

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!

Kenny Lau (Jun 19 2020 at 15:30):

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


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.

Kevin Buzzard (Jun 19 2020 at 15:33):

oh and it's a def not an instance.

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).

Adam Topaz (Jun 19 2020 at 15:36):

The units of the valuation are the preimage of $0$. And $1$ is a unit. So the "non_trivial" assumption is not correct here...

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!

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?)

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.

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


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.

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.

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!

Johan Commelin (Jun 24 2020 at 20:39):

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

Ashvni Narayanan (Jun 24 2020 at 20:42):

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

Johan Commelin (Jun 24 2020 at 20:50):

constructor?

Johan Commelin (Jun 24 2020 at 20:50):

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

Ashvni Narayanan (Jun 24 2020 at 20:57):

Oh, ok. Thank you!

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

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,
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!

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

Ashvni Narayanan (Jun 24 2020 at 22:35):

The exact g line gives the error..

Alex J. Best (Jun 24 2020 at 22:36):

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

Ashvni Narayanan (Jun 24 2020 at 22:37):

Oh, apologies, I edited the code.

Kevin Buzzard (Jun 24 2020 at 22:38):

wow that is some error

Ashvni Narayanan (Jun 24 2020 at 22:38):

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

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.

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

Ashvni Narayanan (Jun 24 2020 at 22:41):

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

Kevin Buzzard (Jun 24 2020 at 22:41):

It's a server running on your computer

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.

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?

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) } :=
zero := _,
neg := _,
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.

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.

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

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

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

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

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

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.

Kevin Buzzard (Jun 24 2020 at 22:57):

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

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⟩,


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?

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

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,
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) } :=


Ashvni Narayanan (Jun 25 2020 at 12:24):

What does the .. do?

Patrick Massot (Jun 25 2020 at 12:28):

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

Thank you!

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.

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
which has type
set ?m_1 → Prop


Johan Commelin (Jun 25 2020 at 12:42):

It takes an argument

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)

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.

(deleted)

Kevin Buzzard (Jun 25 2020 at 13:48):

Which version of lean and mathlib are you using

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?

Ashvni Narayanan (Jun 25 2020 at 14:24):

Oh nice! This seems to work. Thank you!

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!

Johan Commelin (Jun 26 2020 at 17:01):

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

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.

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].)

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."

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) }

Johan Commelin (Jun 26 2020 at 17:04):

Maybe you want notation?

notation S := valuation_ring K


Johan Commelin (Jun 26 2020 at 17:04):

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

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).

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!

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!

Jalex Stark (Jun 27 2020 at 15:13):

unfold val_ring?

Ashvni Narayanan (Jun 27 2020 at 15:14):

Oh, great! Thank you!

Jalex Stark (Jun 27 2020 at 15:15):

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

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


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"

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?

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?)

Ashvni Narayanan (Jun 27 2020 at 16:02):

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

Jalex Stark (Jun 27 2020 at 16:15):

hopefully the proof of that lemma was just rw non_zero?

Yes

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!

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 _.

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

Scott Morrison (Jun 29 2020 at 11:18):

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

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

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)

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"

Ashvni Narayanan (Jun 29 2020 at 11:23):

Scott Morrison said:

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

Yes

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
term
val_ring K
has type
Type ? : Type (max 1 (?+1))
but is expected to have type
set ?m_1 : Type ?


Yes, it will do.

Ashvni Narayanan (Jun 29 2020 at 11:26):

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

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.

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?

Kevin Buzzard (Jun 29 2020 at 11:29):

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

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..

Kevin Buzzard (Jun 29 2020 at 11:31):

Are you using the latest mathlib?

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.

Kevin Buzzard (Jun 29 2020 at 11:31):

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

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
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,
unfold val_ring,
simp,
rintros,
have g : min (v(a)) (v(b)) ≤ v(a + b),
{
},
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,
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,
{
cases f,
exact f_left,
},
{
exact α.2,
},
{
exact b.2,
},
}
end
end discrete_valuation_field


This might help. It is the entire file.

Kevin Buzzard (Jun 29 2020 at 11:34):

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

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) (hπ : π ∈ unif K)

lemma val_unif_eq_one : v(π) = 1 :=
begin
unfold unif at hπ,
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!

Johan Commelin (Jun 30 2020 at 12:16):

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

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.

Johan Commelin (Jun 30 2020 at 12:17):

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

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

Ashvni Narayanan (Jun 30 2020 at 12:25):

Oh, I see. Thank you!

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!

Ashvni Narayanan (Jun 30 2020 at 16:01):

Oh ok, thank you!

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!

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.

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..

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


Johan Commelin (Jun 30 2020 at 16:39):

Unfortunately there don't seem to be lemmas for \u \u n = \u n.

Johan Commelin (Jun 30 2020 at 16:39):

Which is a hole in the with_top API that should be fixed first.

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


Johan Commelin (Jun 30 2020 at 16:42):

Unfortunately not.

Johan Commelin (Jun 30 2020 at 16:42):

It would if n : int of course

Bryan Gin-ge Chen (Jun 30 2020 at 16:43):

Strange, I don't see any errors in my Lean.

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 ≠ ⊤


Ashvni Narayanan (Jun 30 2020 at 16:44):

Yeah, I get the same error

Johan Commelin (Jun 30 2020 at 16:44):

This is on a mathlib that is more than 3 hours old, I admit

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.

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?

Bryan Gin-ge Chen (Jun 30 2020 at 16:45):

My "playground" project is apparently on commit 35fbfe0a40395e6ea394f05b1c56a2fbcf4b33ce from 2 days ago.

Bryan Gin-ge Chen (Jun 30 2020 at 16:45):

The web editor is on this commit from 14 hours ago.

Crazy :confused:

Bryan Gin-ge Chen (Jun 30 2020 at 16:52):

#3132 (merged 7 days ago) looks related, possibly?

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)


Johan Commelin (Jun 30 2020 at 16:54):

That's from yesterday

Bryan Gin-ge Chen (Jun 30 2020 at 16:55):

I think maybe it's #3157?

Johan Commelin (Jun 30 2020 at 16:57):

Aha, that makes sense

Johan Commelin (Jun 30 2020 at 16:57):

@Ashvni Narayanan Please try updating mathlib. It might solve your problem (-;

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


Johan Commelin (Jun 30 2020 at 16:58):

That's what Bryan already wrote. But it depends on having today's mathlib, not yesterdays.

Oh sorry :)

Ashvni Narayanan (Jun 30 2020 at 17:23):

Oh ok, I will do that. Thank you!

Ashvni Narayanan (Jul 02 2020 at 15:22):

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!

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.

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

Thank you!

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!




Adam Topaz (Jul 04 2020 at 02:18):

Does exact g work?

Adam Topaz (Jul 04 2020 at 02:21):

Wait, isn't your lemma false? Why should n be unique?

Mario Carneiro (Jul 04 2020 at 02:23):

The problem is that m is out of scope of the metavariable

Mario Carneiro (Jul 04 2020 at 02:23):

You tried to intro the exists before you have m available

Mario Carneiro (Jul 04 2020 at 02:24):

If you move the cases line to the beginning then exact g works

Thank you!

Ashvni Narayanan (Jul 04 2020 at 02:26):

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.

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 (hπ : π ∈ 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,
hπ : π ∈ 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!

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.)

Ashvni Narayanan (Jul 06 2020 at 22:47):

Thanks! How can I put in the nontrivial condition?

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.

Adam Topaz (Jul 06 2020 at 22:48):

Add an assumption S ≠ ⊥

Adam Topaz (Jul 06 2020 at 22:49):

And as for the membership issue: ∃ n : ℕ, π^n ∈ set.range (λ s : S, (s : K))

Adam Topaz (Jul 06 2020 at 22:50):

That at least typechecks. There are other possibilities as well.

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.

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
hπ: π ∈ unif K
S: ideal ↥(val_ring K)
Q: set ℕ := {n : ℕ | ∃ (x : ↥(val_ring K)) (H : x ∈ S), ↑n = v ↑x}
h: S ≠ ⊥
⊢ Q.nonempty


Reid Barton (Jul 08 2020 at 00:24):

What doesn't work and what is the error message

Adam Topaz (Jul 08 2020 at 00:28):

Does exists_mem_ne_zero_of_ne_bot assume that the ring is a field?

Adam Topaz (Jul 08 2020 at 00:28):

That may be the issue.

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!

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

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 $1 \neq 0$, but it's done in mathlib for vector spaces.

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

yeah true.

Adam Topaz (Jul 08 2020 at 00:32):

in that case everything is bot :)

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,
have : ∀x∈s, (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


Mario Carneiro (Jul 08 2020 at 00:41):

I think contrapose! should do this pretty easily

Adam Topaz (Jul 08 2020 at 00:42):

I just copied the proof from mathlib :)

Adam Topaz (Jul 08 2020 at 00:42):

Except I changed the field to a ring

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
hπ: π ∈ 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!

Reid Barton (Jul 09 2020 at 14:22):

Looks like the apply bug again

Reid Barton (Jul 09 2020 at 14:23):

I would just build the term manually: refine le_trans l _

Reid Barton (Jul 09 2020 at 14:23):

oh, you have both parts already

Jalex Stark (Jul 09 2020 at 14:28):

does linarith close it?

Reid Barton (Jul 09 2020 at 14:28):

exact le_trans l f_left

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


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.

Reid Barton (Jul 09 2020 at 14:29):

You can try convert instead of exact.

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


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


Johan Commelin (Jul 09 2020 at 14:34):

Which is false... so you need to backtrack.

Adam Topaz (Jul 09 2020 at 14:36):

It looks like a subtype thing again... π ^ Inf Q vs ⟨π ^ Inf Q, _⟩

Johan Commelin (Jul 09 2020 at 14:36):

Yup. Can you convert (some stuff) using 1

Johan Commelin (Jul 09 2020 at 14:36):

The using 1 will make it less aggresive.

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


?

Johan Commelin (Jul 09 2020 at 14:53):

I don't know what that means.

Johan Commelin (Jul 09 2020 at 14:53):

What did your goal look like after the convert .... using 1?

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
hπ: π ∈ 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.

Johan Commelin (Jul 09 2020 at 14:57):

There must be a lemma singleton_subset or singleton_subset_iff

Johan Commelin (Jul 09 2020 at 14:57):

Does simp help you here?

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}


Johan Commelin (Jul 09 2020 at 14:59):

Aha, and with using 2?

Ashvni Narayanan (Jul 09 2020 at 14:59):

Johan Commelin said:

Does simp help you here?

No

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))


Johan Commelin (Jul 09 2020 at 15:05):

Aha, we clearly don't want that.

Ashvni Narayanan (Jul 09 2020 at 15:05):

using 2 gives

⊢ {⟨π ^ Inf Q, _⟩} = {π ^ Inf Q}


plus

⊢ has_singleton K (set ↥(val_ring K))


twice.

Johan Commelin (Jul 09 2020 at 15:05):

So let's move back to the inclusion that you had reduced the goal to.

Kenny Lau (Jul 09 2020 at 15:14):

if you livestream in discord then we can compete to tell you the tactic you need!

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.

Adam Topaz (Jul 09 2020 at 15:16):

Where did your assumption l come from?

Ashvni Narayanan (Jul 09 2020 at 15:23):

I had not solved l, just put a sorry. :(

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
hπ: π ∈ 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.

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.

Ashvni Narayanan (Jul 09 2020 at 15:36):

How can I do this? Using a subtype argument at f_3?

Johan Commelin (Jul 09 2020 at 15:37):

I think I would go for rw singleton_subset_iff

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.

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)


:(

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, _⟩?

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?

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

Adam Topaz (Jul 09 2020 at 16:46):

The context doesn't seem to know that π ^ Inf Q is in the valuation ring.

Ashvni Narayanan (Jul 09 2020 at 16:46):

By definition, it is not.

Alex J. Best (Jul 09 2020 at 16:47):

Can someone paste some code I can try?

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)

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.

Ashvni Narayanan (Jul 09 2020 at 17:14):

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.

Adam Topaz (Jul 09 2020 at 17:15):

Yeah I just noticed that. Ignore what I said.

Johan Commelin (Jul 09 2020 at 18:04):

@Ashvni Narayanan What is your goal now?

Johan Commelin (Jul 09 2020 at 18:05):

Or is this solved by now?

No it is not :(

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

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.

Adam Topaz (Jul 09 2020 at 18:13):

Try change z * \<w,f_1\> \in S

Adam Topaz (Jul 09 2020 at 18:14):

I'm not sure if that will help.

Johan Commelin (Jul 09 2020 at 18:17):

apply S.mul_mem_right f_left?

Johan Commelin (Jul 09 2020 at 18:17):

Or something like that.

Ashvni Narayanan (Jul 09 2020 at 18:21):

Yes, that works. Thank you so much!

Ashvni Narayanan (Jul 09 2020 at 18:21):

Try change z * \<w,f_1\> \in S

It helped, thank you!

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 hπ : ∃ π : K, v(π) = 1,
{
cases hv 1 with π hv,
use π,
rw hv,
},
cases hπ with π hπ,
use submodule.span (val_ring K) {π},
end
}


This is not a mwe. The

cases hπ with π hπ,


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,
hπ : ∃ (π : 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!

Kevin Buzzard (Jul 10 2020 at 17:47):

That probably means that your goal is not a proposition

Kevin Buzzard (Jul 10 2020 at 17:48):

Your definition of the prime ideal is data so should really be done in term mode

Kevin Buzzard (Jul 10 2020 at 17:49):

You should probably prove the lemma beforehand, that there exists pi with valuation 1

Kevin Buzzard (Jul 10 2020 at 17:49):

And then use classical.some to define the prime ideal in one line

Ashvni Narayanan (Jul 10 2020 at 17:52):

Oh alright, thank you!

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?)

Kevin Buzzard (Jul 10 2020 at 17:55):

That's a good idea

Reid Barton (Jul 10 2020 at 17:55):

Then you can prove it's also spanned by any element of valuation 1

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