Ideal

Stream: maths

[Ashvni Narayanan]

Are ideals in Lean defined only for commutative rings?

[Chris Hughes]

Yes :oh_no:

[Ashvni Narayanan]

(deleted)

[Ashvni Narayanan]

Chris Hughes said:

Yes :oh_no:

Ahh alright.

[Ashvni Narayanan]

I am trying to prove that the valuation ring corresponding to a discrete valuation field is a discrete valuation ring(defined to be a pid with a unique nonzero prime ideal).

lemma has_discrete_valuation (K:Type*) [field K] [discrete_valuation_field K] (S : Type*) (h : S = {x : K | val(x) ≥ 0}) : discrete_valuation_ring S :=
begin
have P := {x : K | val(x) > 0},
have f : principal_ideal_domain S,
sorry,
have P : ideal S,
sorry,
end

The 3rd last line of the proof gives me an error:

failed to synthesize type class instance for
K : Type u_1,
_inst_2 : field K,
_inst_3 : discrete_valuation_field K,
S : Type u_1,
h : S = ↥{x : K | val x ≥ 0},
P : set K,
f : principal_ideal_domain S
⊢ comm_ring S

I don't know how to input the info that S is commutative. Any help is appreciated. Thank you!

[Reid Barton]

What did you already prove about {x : K | val(x) ≥ 0}?

[Kevin Buzzard]

comm_ring S is in some sense not a good goal, because it's not (at least as far as Lean is concerned) a true/false statement.

[Reid Barton]

This setup with h : S = {x : K | val(x) ≥ 0} looks awkward. Better define def valuation_ring (K:Type*) [field K] [discrete_valuation_field K] := {x : K | val(x) ≥ 0} and then write a bunch of instances about it.

[Kevin Buzzard]

Lean likes things best when they're broken up into coherent chunks which are as small as possible, so rather than launching straight into a proof that the valuation ring is a DVR, you want to first prove simpler things about it, like Reid is hinting. Ten small lemmas is better than one big lemma with lots of sublemmas.