DVRs

Stream: maths

[Kevin Buzzard]

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]

Well, we already have local_ring

[Johan Commelin]

So maybe you should extend that

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

You are already extending that, right?

[Johan Commelin]

I meant, in addition, extend local ring

[Johan Commelin]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

exists_nonzero_nonunit?

[Ashwin Iyengar]

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]

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

[Ashwin Iyengar]

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]

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

[Ashwin Iyengar]

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]

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

[Ashwin Iyengar]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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]

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

[Ashwin Iyengar]

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]

so it records some data

[Ashwin Iyengar]

a PID with a unique nonzero prime ideal

[Johan Commelin]

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

[Ashwin Iyengar]

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

[Johan Commelin]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's either that or make add_group_with_zero

[Johan Commelin]

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

[Kevin Buzzard]

Or with infinity or whatever

[Johan Commelin]

Kevin Buzzard said:

It's either that or make add_group_with_zero

add_group_with_infty

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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?

[Johan Commelin]

norms...

[Ashwin Iyengar]

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]

There are ways around that.

[Johan Commelin]

We could define free_group, or something like that.

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

(Say some subset of the reals)

[Johan Commelin]

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

[Johan Commelin]

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

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]

I'll try to prioritise these PRs

[Ashvni Narayanan]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

That makes R an explicit variable of is_uniformizer.

[Johan Commelin]

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

[Johan Commelin]

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

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

[Ashvni Narayanan]

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]

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

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

[Ashvni Narayanan]

I had tried that earlier,

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

gives the error

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

[Johan Commelin]

Aah... right. The solution is

set_option old_structure_cmd true

That will merge the duplicate fields

[Ashvni Narayanan]

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

[Johan Commelin]

@Chris Hughes Should submodule.is_prinicipal be a class?

[Johan Commelin]

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

[Johan Commelin]

This is not nice

[Kevin Buzzard]

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]

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

[Johan Commelin]

But I agree with the point

[Johan Commelin]

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

[Johan Commelin]

@Mario Carneiro what's going on here?

[Johan Commelin]

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]

what's the question?

[Johan Commelin]

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

[Mario Carneiro]

Is it about unbundling ring classes into mixins?

[Johan Commelin]

It's about inferred instances not being defeq

[Mario Carneiro]

aha, this came up not too long ago

[Johan Commelin]

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

[Johan Commelin]

With alternating old and new structures?

[Mario Carneiro]

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

[Mario Carneiro]

It's actually a kind of fundamental problem

[Mario Carneiro]

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]

it also doesn't work for instances that are variables

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

But new structure were introduced for a reason, right?

[Johan Commelin]

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

[Johan Commelin]

And the hierarchy is far from finished.

[Johan Commelin]

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

[Sebastien Gouezel]

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]

I think that would be a good idea.

[Johan Commelin]

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

[Mario Carneiro]

Oh wait, discrete_valuation_ring is actually broken

[Mario Carneiro]

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]

note the separate appearance of comm_ring R and integral_domain R

[Mario Carneiro]

the unification problem fails because it's actually false

[Johan Commelin]

Mario Carneiro said:

note the separate appearance of comm_ring R and integral_domain R

How did that happen?

[Mario Carneiro]

the double extends

[Johan Commelin]

Shouldn't old_structure_cmd take care of that?

[Mario Carneiro]

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

[Kevin Buzzard]

Which structure isn't old?

[Mario Carneiro]

Both, I think

[Mario Carneiro]

local_ring and principal_ideal_domain are both new structures

[Mario Carneiro]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

the compilation here is pretty unquestionably wrong

[Kevin Buzzard]

What is the Lean 3 idiomatic way to proceed?

[Kevin Buzzard]

Is there any harm in just making them old structures?

[Johan Commelin]

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

[Johan Commelin]

Mario wants to fix lean instead.

[Mario Carneiro]

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]

possibly also structure literals are affected

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Kevin Buzzard]

So what do we do?

[Kevin Buzzard]

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]

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

ambiguous overload, possible interpretations
    add_comm
    principal_ideal_domain.add_comm

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

Similarly for is_local

[Adam Topaz]

What are your thoughts about using some definition like this:

import ring_theory.principal_ideal_domain

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

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

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

[Kenny Lau]

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]

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

[Kenny Lau]

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

[Johan Commelin]

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]

how about is_ring and is_comm_ring predicated on semirings

[Kenny Lau]

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

[Kenny Lau]

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

[Johan Commelin]

Why?

[Adam Topaz]

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]

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]

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

[Johan Commelin]

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

[Adam Topaz]

(deleted)

[Johan Commelin]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Adam Topaz]

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]

I guess we would want CDVRs as well

[Kenny Lau]

and a proof that they are henselian

[Adam Topaz]

What does CDVR stand for?

[Kevin Buzzard]

CDVR could also be a predicate

[Kevin Buzzard]

complete DVR

[Adam Topaz]

ah ok.

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

i.e. there's still something missing

[Johan Commelin]

Ooh, right, we need another compatibility class.

[Kevin Buzzard]

distrib++

[Johan Commelin]

I guess we could add is_cdvr which extends complete_space and is_dvr

[Kevin Buzzard]

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

[Johan Commelin]

Nope...

[Johan Commelin]

Because Z_p

[Kevin Buzzard]

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

[Ashvni Narayanan]

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

[Johan Commelin]

Will that play nice with the rest of the topology?

[Adam Topaz]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Ashvni Narayanan]

10 equivalent definitions for DVRs?

[Kevin Buzzard]

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

[Kevin Buzzard]

Yes, there are 10 definitions of DVR on Wikipedia

[Kevin Buzzard]

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]

Kevin Buzzard said:

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

No, just 10 constructors.

[Kevin Buzzard]

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

[Ashvni Narayanan]

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]

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]

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]

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

[Johan Commelin]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

is_local_ring isn't a class

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

[Kevin Buzzard]

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

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]

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]

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

[Johan Commelin]

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]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Johan Commelin]

So the class lives in Prop instead of Type*

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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

[Reid Barton]

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

[Reid Barton]

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

[Johan Commelin]

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

[Johan Commelin]

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]

So do you want is_PIR and is_PID?

[Johan Commelin]

No, only is_PIR

[Johan Commelin]

Because it covers everything

[Johan Commelin]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

But at the moment I would go for maximum flexibility.

[Ashvni Narayanan]

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]

A #mwe needs imports!

[Kevin Buzzard]

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

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]

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

[Johan Commelin]

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

[Ashvni Narayanan]

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

[Kevin Buzzard]

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

[Ashvni Narayanan]

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]

the second line has two binders

[Jalex Stark]

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

[Jalex Stark]

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]

Always look at the first error

[Ashvni Narayanan]

Thank you!

[Jalex Stark]

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]

what does open_locale classical do?

[Jalex Stark]

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

[Jalex Stark]

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

[Jalex Stark]

(important edit to the previous post)

[Ashvni Narayanan]

Thank you!

[Jalex Stark]

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]

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

[Jalex Stark]

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]

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]

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]

Now I add the rest

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

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

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

[Jalex Stark]

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]

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

[Jalex Stark]

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]

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]

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]

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

[Jalex Stark]

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]

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

[Ashvni Narayanan]

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]

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

[Kevin Buzzard]

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]

oh and it's a def not an instance.

[Kevin Buzzard]

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]

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]

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]

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

[Ashvni Narayanan]

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

[Adam Topaz]

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]

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]

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]

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]

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

[Ashvni Narayanan]

Adam Topaz said:

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

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

[Johan Commelin]

constructor?

[Johan Commelin]

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

[Ashvni Narayanan]

Oh, ok. Thank you!

[Jalex Stark]

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]

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

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

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

namespace discrete_valuation_field

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

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

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

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

I get the error:

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

Any help is appreciated. Thank you!

[Alex J. Best]

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

[Ashvni Narayanan]

The exact g line gives the error..

[Alex J. Best]

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

[Ashvni Narayanan]

Oh, apologies, I edited the code.

[Kevin Buzzard]

wow that is some error

[Ashvni Narayanan]

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

[Alex J. Best]

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]

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]

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

[Kevin Buzzard]

It's a server running on your computer

[Alex J. Best]

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]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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]

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]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

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

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

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

[Ashvni Narayanan]

What does the .. do?

[Patrick Massot]

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

[Patrick Massot]

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

[Ashvni Narayanan]

Thank you!

[Kevin Buzzard]

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

[Ashvni Narayanan]

The last one (is_subring K) gives me an error

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

[Johan Commelin]

It takes an argument

[Ashvni Narayanan]

Also, why do both is_add_subgroup and add_subgroup exist?

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Ashvni Narayanan]

(deleted)

[Kevin Buzzard]

Which version of lean and mathlib are you using

[Alex J. Best]

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]

Oh nice! This seems to work. Thank you!

[Ashvni Narayanan]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

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]

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

[Johan Commelin]

Maybe you want notation?

notation `S` := valuation_ring K

[Johan Commelin]

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

[Johan Commelin]

You want to prove things about that definition instead

[Johan Commelin]

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]

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]

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]

unfold val_ring?

[Ashvni Narayanan]

Oh, great! Thank you!

[Jalex Stark]

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

[Ashvni Narayanan]

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]

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]

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]

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]

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

[Jalex Stark]

hopefully the proof of that lemma was just rw non_zero?

[Ashvni Narayanan]

Yes

[Ashvni Narayanan]

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]

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]

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

[Scott Morrison]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

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

[Ashvni Narayanan]

Scott Morrison said:

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

Yes

[Ashvni Narayanan]

Kevin Buzzard said:

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

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

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

[Kevin Buzzard]

Yes, it will do.

[Ashvni Narayanan]

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

[Ashvni Narayanan]

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]

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]

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

[Ashvni Narayanan]

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]

Are you using the latest mathlib?

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Ashvni Narayanan]

import ring_theory.ideals

import ring_theory.principal_ideal_domain

import ring_theory.localization

import tactic

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

namespace discrete_valuation_field

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

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

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

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

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

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

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


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

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

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

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

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

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

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

This might help. It is the entire file.

[Kevin Buzzard]

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

[Ashvni Narayanan]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

Oh, I see. Thank you!

[Reid Barton]

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]

Oh ok, thank you!

[Ashvni Narayanan]

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]

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

[Ashvni Narayanan]

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]

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

end

[Johan Commelin]

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

[Johan Commelin]

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

[Bryan Gin-ge Chen]

Doesn't this just work?

import order.bounded_lattice

lemma nat_neq_top (n :ℕ) : (↑n:with_top ℤ) ≠ ⊤ :=
with_top.coe_ne_top

[Johan Commelin]

Unfortunately not.

[Johan Commelin]

It would if n : int of course

[Bryan Gin-ge Chen]

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

[Johan Commelin]

type mismatch, term
  with_top.coe_ne_top
has type
  ↑?m_2 ≠ ⊤
but is expected to have type
  ↑n ≠ ⊤

[Ashvni Narayanan]

Yeah, I get the same error

[Johan Commelin]

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

[Bryan Gin-ge Chen]

Did I copy and paste something wrong? I don't see any errors in the web editor either.

[Ashvni Narayanan]

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]

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

[Bryan Gin-ge Chen]

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

[Johan Commelin]

Crazy :confused:

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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]

That's from yesterday

[Bryan Gin-ge Chen]

I think maybe it's #3157?

[Johan Commelin]

Aha, that makes sense

[Johan Commelin]

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

[Adam Topaz]

This also works:

lemma nat_neq_top (n :ℕ) : (n : with_top ℤ) ≠ ⊤ := by apply with_top.coe_ne_top

[Johan Commelin]

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

[Adam Topaz]

Oh sorry :)

[Ashvni Narayanan]

Oh ok, I will do that. Thank you!

[Ashvni Narayanan]

https://github.com/laughinggas/DVR/blob/cc3a8e881c914fa17f9bde07fbcead8850f9152f/src/Test.lean#L598

I am trying to prove Line 598. Line 608 gives me an error, I don't know how to use the lemma val_int_power then.
Any help is appreciated. Thank you!

[Kevin Buzzard]

α⁻¹ 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]

After unfold val_ring you can do

      suffices : 0 ≤ v (α ^ (-1 : ℤ)),
        simpa,

and then your rewrite will work

[Ashvni Narayanan]

Thank you!

[Ashvni Narayanan]

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]

Does exact g work?

[Adam Topaz]

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

[Mario Carneiro]

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

[Mario Carneiro]

You tried to intro the exists before you have m available

[Mario Carneiro]

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

[Ashvni Narayanan]

Thank you!

[Ashvni Narayanan]

Adam Topaz said:

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

Thanks for pointing this out, you are correct, I forgot to put in additional conditions.

[Ashvni Narayanan]

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]

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]

Thanks! How can I put in the nontrivial condition?

[Kevin Buzzard]

Ideals are a lattice, so I \ne \bot is the preferred way to say I isn't the zero ideal.

[Adam Topaz]

Add an assumption S ≠ ⊥

[Adam Topaz]

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

[Adam Topaz]

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

[Ashvni Narayanan]

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]

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]

What doesn't work and what is the error message

[Adam Topaz]

Does exists_mem_ne_zero_of_ne_bot assume that the ring is a field?

[Adam Topaz]

That may be the issue.

[Ashvni Narayanan]

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]

It looks like there ought to be a lemma saying an ideal is bot iff all its elements are 0

[Adam Topaz]

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]

It should even be true for the zero ring right? because then there is no ideal other than bot

[Adam Topaz]

yeah true.

[Adam Topaz]

in that case everything is bot :)

[Adam Topaz]

The same exact proof works in general:

import algebra
import linear_algebra

variables {R : Type*} [ring R]
variables {M : Type*} [add_comm_group M] [module R M]

lemma exists_mem_ne_zero_of_ne_bot {s : submodule R M} (h : s ≠ ⊥) : ∃ b : M, b ∈ s ∧ b ≠ 0 :=
begin
  classical,
  by_contradiction hex,
  have : ∀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]

I think contrapose! should do this pretty easily

[Adam Topaz]

I just copied the proof from mathlib :)

[Adam Topaz]

Except I changed the field to a ring

[Ashvni Narayanan]

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]

Looks like the apply bug again

[Reid Barton]

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

[Reid Barton]

oh, you have both parts already

[Jalex Stark]

does linarith close it?

[Reid Barton]

exact le_trans l f_left

[Ashvni Narayanan]

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]

OK, well I don't know what this is but then you need to fix this anyways.

[Reid Barton]

You can try convert instead of exact.

[Ashvni Narayanan]

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]

Reid Barton said:

You can try convert instead of exact.

This gives me a goal :

⊢ ↥(val_ring K) = K

[Johan Commelin]

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

[Adam Topaz]

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

[Johan Commelin]

Yup. Can you convert (some stuff) using 1

[Johan Commelin]

The using 1 will make it less aggresive.

[Ashvni Narayanan]

Is there a way to apply

using 1

to a goal of the form

⊢ {⟨π ^ Inf Q, _⟩} ⊆ ↑S

?

[Johan Commelin]

I don't know what that means.

[Johan Commelin]

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

[Ashvni Narayanan]

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]

There must be a lemma singleton_subset or singleton_subset_iff

[Johan Commelin]

Does simp help you here?

[Ashvni Narayanan]

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]

Aha, and with using 2?

[Ashvni Narayanan]

Johan Commelin said:

Does simp help you here?

No

[Ashvni Narayanan]

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]

Aha, we clearly don't want that.

[Ashvni Narayanan]

using 2 gives

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

plus

⊢ has_singleton K (set ↥(val_ring K))

twice.

[Johan Commelin]

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

[Kenny Lau]

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

[Adam Topaz]

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]

Where did your assumption l come from?

[Ashvni Narayanan]

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

[Ashvni Narayanan]

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]

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]

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

[Johan Commelin]

I think I would go for rw singleton_subset_iff

[Adam Topaz]

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]

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]

I don't know what that means. Does lean know how to fill the hole in the ⟨π ^ Inf Q, _⟩?

[Ashvni Narayanan]

I don't know, but I don't think so. Is there a way to check this?

[Alex J. Best]

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]

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

[Ashvni Narayanan]

By definition, it is not.

[Alex J. Best]

Can someone paste some code I can try?

[Ashvni Narayanan]

https://github.com/laughinggas/DVR/blob/86c6dad4514e328c49b62300f1546c15d773b10c/src/Test.lean#L967

[Adam Topaz]

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]

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]

Adam Topaz said:

On line 834, you write use π^(Inf Q)but this is something in K a priori. This might be the issue...
(nevermind -- ignore this)

As soon as I use this, the first goal is to check that it is in val_ring K.

[Adam Topaz]

Yeah I just noticed that. Ignore what I said.

[Johan Commelin]

@Ashvni Narayanan What is your goal now?

[Johan Commelin]

Or is this solved by now?

[Ashvni Narayanan]

No it is not :(

[Ashvni Narayanan]

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]

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]

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

[Adam Topaz]

I'm not sure if that will help.

[Johan Commelin]

apply S.mul_mem_right f_left?

[Johan Commelin]

Or something like that.

[Ashvni Narayanan]

Yes, that works. Thank you so much!

[Ashvni Narayanan]

Adam Topaz said:

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

It helped, thank you!

[Ashvni Narayanan]

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]

That probably means that your goal is not a proposition

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Ashvni Narayanan]

Oh alright, thank you!

[Reid Barton]

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]

That's a good idea

[Reid Barton]

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

[Kevin Buzzard]

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

[Filippo A. E. Nuccio]

While working on DVR's with @María Inés de Frutos Fernández we observed that the file ring_theory/valuation/tfae.lean (that gives equivalent conditions for being a DVR) is in the valuation folder, and that there is a ring_theory/discrete_valuation_ring file with generalities on DVR's. It would seem more reasonable to us to create a DVR folder with both these files. Any objections?

[Johan Commelin]

Sounds good to me.
Is tfae.lean only about DVRs? Or also about more general valuations?

[Filippo A. E. Nuccio]

Only about DVR, I would say.

[Filippo A. E. Nuccio]

Done, #18867