Skip to content

Instantly share code, notes, and snippets.

@adamtopaz

adamtopaz/dvr.lean

Last active Jun 16, 2020
Embed
What would you like to do?
A DVR is a valuation ring which is a PID
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 valuation ring
(nonfield : ∃ u : A, ∀ v : A, u * v ≠ 1) -- or a better formulation
open DVR
instance local_ring_of_dvr (A : Type*) [DVR A] : local_ring A :=
begin
split,
intro a,
cases val_cond a (1-a) with z hz,
cases hz,
{
left,
refine ⟨⟨a,1+z,_,_⟩,rfl⟩,
{
rw [mul_add,hz],
ring,
},
{
rw [mul_comm,mul_add,hz],
ring,
}
},
{
right,
refine ⟨⟨1-a,1+z,_,_⟩,rfl⟩,
{
rw [mul_add, hz],
ring,
},
{
rw [mul_comm,mul_add,hz],
ring,
}
}
end
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment