## Stream: new members

### Topic: Weird Type Mismatch error

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 07:09):

I am getting a very weird error and I have no idea why this is not working. I couldn't reproduce the error more minimally than this. Can someone help please?

import ring_theory.ideal.basic

lemma maximal_ideal_of_field_quotient (R : Type) [comm_ring R] (I : ideal R) [field I.quotient] : I.is_maximal := begin
refine ideal.is_maximal_iff.mpr _,
split, { sorry },
{ intros J x hIJ hxI hxJ,
have hxne0 : (ideal.quotient.mk I x) ≠ (0 : I.quotient), {
intro h,
have hxI2 : x ∈ I, {exact ideal.quotient.eq_zero_iff_mem.1 h},
sorry
},
sorry}
end


Error:

type mismatch at application
ideal.quotient.eq_zero_iff_mem.mp h
term
h
has type
⇑(ideal.quotient.mk I) x = 0
but is expected to have type
⇑(ideal.quotient.mk I) x = 0
state:
R : Type,
_inst_1 : comm_ring R,
I : ideal R,
_inst_2 : field I.quotient,
J : ideal R,
x : R,
hIJ : I ≤ J,
hxI : x ∉ I,
hxJ : x ∈ J,
h : ⇑(ideal.quotient.mk I) x = 0
⊢ x ∈ I


#### Kevin Buzzard (Aug 29 2020 at 07:16):

Try using convert instead of exact. What happens if you set_option pp.all true?

#### Kevin Buzzard (Aug 29 2020 at 07:17):

Oh I think I see it. I don't think field I.quotient means what you think it means. It means "let's put a random field structure on the quotient, completely unrelated to the quotient ring structure". So now you have two ring structures on something and they don't agree

#### Kevin Buzzard (Aug 29 2020 at 07:18):

And hence two different zeros

#### Kevin Buzzard (Aug 29 2020 at 07:19):

I posted a way to do this in another thread recently. Maybe search for is_integral_domain and a conversation involving Damiano Testa and Johan and I

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 08:18):

Oh, I see now why only the converse of my statement was in Lean. I guess I will try to work on is_field then.

#### Kevin Buzzard (Aug 29 2020 at 09:19):

I wrote it a few days ago but didn't PR it. Did you find it? Search on mobile isn't finding it for me. There is a technical issue with it. Unfortunately fields have extra data -- the inv function, which is unique but not part of the ring story. I still think it's a useful thing to have though

#### Kevin Buzzard (Aug 29 2020 at 09:21):

I posted it in a discussion about transporting integral domains across isomorphisms and proving that if R/I was an ID then I was prime

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 09:34):

Looks like it was the same thread you mentioned earlier and seems like I just skipped that code when reading the thread. Though I did something slightly differently, but wouldn't this be better since you can use inverse notation without calling is_field.to_field or something?

My version:

structure is_field (R : Type) [comm_ring R] extends nontrivial R, has_inv R :=
(mul_inv_cancel : ∀ {a : R}, a ≠ 0 → a * a⁻¹ = 1)
(inv_zero : (0 : R)⁻¹ = 0)


structure is_field (R : Type u) [ring R] : Prop :=
(exists_pair_ne : ∃ (x y : R), x ≠ y)
(mul_comm : ∀ (x y : R), x * y = y * x)
(mul_inv_cancel' : ∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1)


#### Kevin Buzzard (Aug 29 2020 at 09:49):

Make sure it's a Prop. There's a bug in Lean 3 which might make that structure a type by default. Put  : Prop before the := . But now you'll have to make this inv operator on your quotient. You could try both and see which is easier to use. I'm not very good at definitions. @Johan Commelin was not positive about this being a good idea and I'm not very good at definitions.

#### Kevin Buzzard (Aug 29 2020 at 09:49):

Oh wait if you're extending data then it probably isn't a prop. Isn't the point to get a true/false statement?

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 09:51):

What I needed this was so that Lean can take the data for the usual ring structure on I.quotient and then tell Lean that this data extends to a field. Before, Lean was giving I.quotient a random field structure and that wasn't working.

#### Kevin Buzzard (Aug 29 2020 at 09:52):

Right but to make it a field in the sense of lean you still have to add the data of inv because for some reason that's the way fields are set up in lean

#### Kevin Buzzard (Aug 29 2020 at 09:53):

Can you extend group with zero instead?

#### Kevin Buzzard (Aug 29 2020 at 09:53):

The issue is that a field isn't just a ring which is a field, it's a ring plus a new function inv which satisfies the axioms of a field

#### Kevin Buzzard (Aug 29 2020 at 09:54):

And you can work out inv from the other data

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 09:54):

I am not sure what you mean by extending group with zero. Isn't it already a group with 0 since it is a ring?

#### Kevin Buzzard (Aug 29 2020 at 09:54):

The way I did it was asking for an abstract existence of inv and then building it later when I needed field not just is_field

#### Kevin Buzzard (Aug 29 2020 at 09:55):

A ring is a monoid with 0

#### Kevin Buzzard (Aug 29 2020 at 09:55):

A division ring is a group with zero

#### Kevin Buzzard (Aug 29 2020 at 09:55):

A commutative division ring is a field

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 09:55):

Oh nvm, I got confused

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 09:56):

I guess the best way to not run into problems is to make the is_field into a Prop the way you described it and have propositions to turn it into a field for when it is necessary.

#### Kevin Buzzard (Aug 29 2020 at 09:57):

The technical issue here in the background is the following

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 09:58):

Group with 0 wouldn't work, since that extends has_inv so it is the same issue.

#### Kevin Buzzard (Aug 29 2020 at 09:59):

If we start with h1 : field k and then make h2 : is_field k and then h3 : field k then h1 and h3 might have invs which are equal as functions but which are not definitionally equal

#### Kevin Buzzard (Aug 29 2020 at 10:00):

And so you can imagine a situation where you have two terms of type field k which are not definitionally equal, and this is bad because field is a class

#### Kevin Buzzard (Aug 29 2020 at 10:01):

And the type class inference system doesn't expect this sort of thing to happen so it might lead to problems down the line

#### Kevin Buzzard (Aug 29 2020 at 10:02):

But to be quite frank we certainly need the lemma that if the quotient is a field then the ideal is maximal so we seem to need a predicate on commutative rings saying they are fields

#### Kevin Buzzard (Aug 29 2020 at 10:03):

Maybe it's just the construction of field from is_field which should be avoided in general

#### Kevin Buzzard (Aug 29 2020 at 10:04):

Go ahead and make a PR :-) How are Dedekind domains? Which of the two PRs are you working with, or are you using another one? :-/

#### Alexandru-Andrei Bosinta (Aug 29 2020 at 10:06):

Thank you for the insight! I will prove this theorem and I will look into PRing it. Right now I wasn't exactly working on Dedekind Domains. I used a definition I did for Dedekind domains a while ago, then I defined a number field and a number ring and I was working on proving that a number ring is a dedekind domain, though I needed this theorem to do it (or at least that is the way it is done in the book I am following).

#### Kevin Buzzard (Aug 29 2020 at 16:07):

@Ashvni Narayanan you might be interested in this. Ashvni is thinking about proving that the class group of a number field is finite. I don't know what the most general statement is. The class group of a general Dedekind domain is not finite -- finiteness is an arithmetic issue, not an algebraic one. The class group of a global field is finite. A global field has a funny definition as far as I can see -- it is either a number field or a finite extension of (Z/pZ)(T). To define the integers of a finite extension of (Z/pZ)(T) you have to "choose an infinity"! If you choose the usual one, then the integers of (Z/pZ)(T) are (Z/pZ)[T], which has trivial class group. Other infinities are available. What is driving the finiteness of the class group? Is it something to do with the fact that all residue fields are finite in both of these cases, or do you need more? I should know this but I don't.

#### Alex J. Best (Aug 29 2020 at 16:19):

Artin-Whaples seem to think its the product formula, https://projecteuclid.org/euclid.bams/1183507128

#### Adam Topaz (Aug 29 2020 at 16:21):

It's the product formula and finiteness of residue fields, IMO

#### Adam Topaz (Aug 29 2020 at 16:23):

FWIW, the "uniform" definition of a global field is a finitely generated field of Kronecker dimension 1

#### Adam Topaz (Aug 29 2020 at 16:25):

The best intuition I have for this comes from the Lang-Neron theorem.

#### Johan Commelin (Aug 29 2020 at 16:25):

I wonder how we are going to name the fields of higher dimension once we get more theorems about them (-;

#### Adam Topaz (Aug 29 2020 at 16:26):

Infinite finitely generated fields are all anabelian :wink:

#### Johan Commelin (Aug 29 2020 at 16:27):

Are we going to call the 2-dim fields superglobal? And then hyperglobal? ultraglobal?

#### Adam Topaz (Aug 29 2020 at 16:27):

Lol I just use the Kronecker dimension in general.

#### Kevin Buzzard (Aug 29 2020 at 16:27):

I think Weil tries to do the general case in "basic number theory" but that book is such a chore read, I've not opened it for years. What little I once knew I learnt from there.

#### Kevin Buzzard (Aug 29 2020 at 16:28):

(I mean unifying number fields and 1-d function fields over finite fields)

#### Adam Topaz (Aug 29 2020 at 16:29):

There is also a class field theory for all f.g. fields, btw

#### Kevin Buzzard (Aug 29 2020 at 16:31):

These things will be interesting to formalise -- even the statements.

#### Adam Topaz (Aug 29 2020 at 16:31):

Higher dimensional local fields are called "higher local fields" (very creative)

#### Kevin Buzzard (Aug 29 2020 at 16:32):

I am still unclear about how I'm going to be talking about representations of Gal(Q-bar/Q) and whether or not I'm supposed to be picking a Q-bar or proving things valid for all Q-bar's.

#### Adam Topaz (Aug 29 2020 at 16:32):

Use the groupoid?

#### Kevin Buzzard (Aug 29 2020 at 16:32):

All the Langlandsy stuff should be canonically independent of everything

#### Kevin Buzzard (Aug 29 2020 at 16:33):

Maybe the groupoid is the way to go

#### Adam Topaz (Aug 29 2020 at 16:33):

This issue is all over the place in anabelian geometry.

#### Kevin Buzzard (Aug 29 2020 at 16:33):

but it's funny because in all the Langlands papers I read (at least those written by the French, who are careful about these things) they choose an alg closure of Q on line 1.

#### Adam Topaz (Aug 29 2020 at 16:33):

We are usually lazy and just work with profinite groups with outer-morphisms

#### Kevin Buzzard (Aug 29 2020 at 16:34):

and if people are doing more serious things then they even "choose Langlands parameters", which means choosing a Q-bar, a Q_p-bar for all p, and maps from Q-bar to C and to all Q_p-bar's. This is again all on line 1.

#### Adam Topaz (Aug 29 2020 at 16:34):

@Aaron Anderson would just work in a "monster model"

#### Kevin Buzzard (Aug 29 2020 at 16:35):

"Make so many choices that it is impossible to conceive of them. And now let's begin. And all the important stuff will be independent of all these choices. I promise."

#### Aaron Anderson (Aug 29 2020 at 16:46):

Aaron Anderson would just work in a "monster model"

One universe up, just because we can

#### Ashvni Narayanan (Aug 30 2020 at 11:25):

Kevin Buzzard said:

Ashvni Narayanan you might be interested in this. Ashvni is thinking about proving that the class group of a number field is finite. I don't know what the most general statement is. The class group of a general Dedekind domain is not finite -- finiteness is an arithmetic issue, not an algebraic one. The class group of a global field is finite. A global field has a funny definition as far as I can see -- it is either a number field or a finite extension of (Z/pZ)(T). To define the integers of a finite extension of (Z/pZ)(T) you have to "choose an infinity"! If you choose the usual one, then the integers of (Z/pZ)(T) are (Z/pZ)[T], which has trivial class group. Other infinities are available. What is driving the finiteness of the class group? Is it something to do with the fact that all residue fields are finite in both of these cases, or do you need more? I should know this but I don't.

I am looking into it. I defined a number field, but if @Alexandru-Andrei Bosinta has already done some non-trivial work on it, I guess it does not make sense to redo it. I wanted to prove the finiteness of the ideal class group of number fields, hoping that the Dedekind domain PRs are done by then. I was also hoping that the proof of finiteness for number fields would give me some ideas as to how much we can generalize the statement. As far as I recall, I think there is a theorem that says that all abelian groups occur as class groups for some Dedekind domain. Moreover, it is sufficient to look at quadratic extensions (this is a highly incomplete statement). That is all I can say as of now.

#### Alexandru-Andrei Bosinta (Aug 30 2020 at 14:35):

@Ashvni Narayanan I say we compare definitions and whatever work each of us done on it. I didn't get to do much though, but I can give you the work I did so far. There is probably a better way to do this, but I find it easiest to post it here for now.

import algebra.field
import data.rat.basic
import ring_theory.algebra
import ring_theory.algebraic
import ring_theory.integral_closure

open function
open_locale classical big_operators

def is_integrally_closed_domain (R : Type) [comm_ring R] : Prop := ∀ {r s : R}, s ≠ 0 → (∃ (n : ℕ) (f : ℕ → R)
(hf : f 0 = 1), ∑ ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0) → s ∣ r

class dedekind_id (R : Type) [integral_domain R] : Prop :=
(noetherian : is_noetherian_ring R)
(int_closed : is_integrally_closed_domain R)
(max_nonzero_primes : ∀ P : ideal R, P ≠ ⊥ → P.is_prime → P.is_maximal)

class number_field (K : Type) :=
(fld : field K)
(alg : algebra ℚ K)
(fd : finite_dimensional ℚ K)

instance field_of_number_field (K : Type) [number_field K] : field K := _inst_1.fld

instance algebra_of_number_field (K : Type) [number_field K] : algebra ℚ K := _inst_1.alg

instance infinite_of_number_field (K : Type) [number_field K] : infinite K := begin
let f : ℤ → K := (λ n, (n : ℚ) • (1 : K)),
apply infinite.of_injective f,
intros x y hxy,
have hxy2 : (x : ℚ) • (1 : K) = (y : ℚ) • (1 : K), exact hxy,
have h : 0 = ((x : ℚ) - (y : ℚ)) • (1 : K), calc 0 = (x : ℚ) • (1 : K) - (y : ℚ) • (1 : K) : by rw sub_eq_zero.mpr hxy
... = (x : ℚ) • (1 : K) + (-((y : ℚ) • (1 : K))) : sub_eq_add_neg (↑x • 1) (↑y • 1)
... = (x : ℚ) • (1 : K) + ((-(y : ℚ)) • (1 : K)) : by rw neg_smul
... = ((x : ℚ) + (-(y : ℚ))) • (1 : K) : by rw add_smul
... = ((x : ℚ) - (y : ℚ)) • (1 : K) : by rw sub_eq_add_neg,
have h2 : ((x : ℚ) - (y : ℚ)) = 0 ∨ (1 : K) = 0, {exact (@smul_eq_zero ℚ K _ _ _ ((x : ℚ) - (y : ℚ)) (1 : K)).1 (eq.symm h)},
cases h2, {have h3 : (x : ℚ) = (y : ℚ), exact sub_eq_zero.mp h2,
exact (rat.coe_int_inj (x : ℤ) (y : ℤ)).1 h3},
{exfalso, revert h2, simp}
end

def number_ring (K : Type) [number_field K] := @integral_closure ℤ K _ (@field.to_comm_ring K _inst_1.fld) _

theorem integral_domain_of_number_ring (K : Type) [number_field K] : integral_domain (number_ring K) :=
(number_ring K).integral_domain

example (K : Type) [field K] (x : K) (h : x ≠ 0): x * (field.inv x) = 1 := field.mul_inv_cancel h

/-- A predicate to express that a ring is a field.

This is mainly useful because such a predicate does not contain data,
and can therefore be easily transported along ring isomorphisms. -/
structure is_field (R : Type) [ring R] : Prop :=
(exists_pair_ne : ∃ (x y : R), x ≠ y)
(mul_comm : ∀ (x y : R), x * y = y * x)
(mul_inv_cancel' : ∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1)

/-- Every field satisfies the predicate for integral domains. -/
lemma field.to_is_field (R : Type) [field R] : is_field R :=
{mul_inv_cancel' := λ a ha, ⟨a⁻¹, field.mul_inv_cancel ha⟩,
.. (‹_› : field R) }

noncomputable def is_field.to_field (R : Type) [ring R] (h : is_field R) : field R :=
{inv := (λ a, if ha : a = 0 then 0 else classical.some (is_field.mul_inv_cancel' h ha)),
inv_zero := (dif_pos rfl),
mul_inv_cancel := (λ a ha, begin
convert classical.some_spec (is_field.mul_inv_cancel' h ha),
exact dif_neg ha
end),
.._inst_1, ..h}

/-- There is a unique inverse in a field.
-/
lemma uniq_inv_of_is_field (R : Type) [comm_ring R] [is_field R]: ∀ (x : R), x ≠ 0 → ∃! (y : R), x * y = 1 := begin
intros x hx,
apply exists_unique_of_exists_of_unique,
{exact _inst_2.mul_inv_cancel' hx},
intros y z hxy hxz,
calc y = y * 1 : eq.symm (mul_one y)
... = y * (x * z) : by rw hxz
... = (y * x) * z : eq.symm (mul_assoc y x z)
... = (x * y) * z : by rw mul_comm y x
... = 1 * z : by rw hxy
... = z : one_mul z
end

/-- If the quotient of a comm_ring by an ideal is a field, then the ideal is maximal
-/
lemma maximal_ideal_of_is_field_quotient (R : Type) [comm_ring R] (I : ideal R)
[@is_field I.quotient (comm_ring.to_ring (ideal.quotient I))] : I.is_maximal := begin
apply ideal.is_maximal_iff.2,
split, {intro h,
rcases (_inst_2.exists_pair_ne) with ⟨⟨x⟩, ⟨y⟩, hxy⟩,
apply hxy,
apply ideal.quotient.eq.2,
rw ←mul_one (x-y),
apply submodule.smul_mem',
exact h},
{intros J x hIJ hxnI hxJ,
have hxn0 : (ideal.quotient.mk I x) ≠ 0,
{exact @mt ((ideal.quotient.mk I x) = 0) (x ∈ I) ideal.quotient.eq_zero_iff_mem.1 hxnI},
have hinvx : ∃ (y : I.quotient), (ideal.quotient.mk I x) * y = 1, {exact _inst_2.mul_inv_cancel' hxn0},
rcases hinvx with ⟨⟨y⟩, hy⟩,
change (ideal.quotient.mk I x) * (ideal.quotient.mk I y) = 1 at hy,
rw ←((ideal.quotient.mk I).map_mul x y) at hy,
have hxy1I : x*y-1 ∈ I, exact ideal.quotient.eq.1 hy,
have hxy1J : x*y-1 ∈ J, exact hIJ hxy1I,
have hxyJ : x*y ∈ J, exact ideal.mul_mem_right J hxJ,
have hend : x*y-(x*y-1) ∈ J, exact ideal.sub_mem J hxyJ hxy1J,
have h1 : 1 = x*y-(x*y-1), by ring,
rw h1,
exact hend}
end

/-- The quotient of a ring by an ideal is a field iff the ideal is maximal.
-/
theorem maximal_ideal_iff_is_field_quotient (R : Type) [comm_ring R] (I : ideal R) :
I.is_maximal ↔ (@is_field I.quotient (comm_ring.to_ring (ideal.quotient I))) := begin
split,
{intro h,
exact @field.to_is_field I.quotient (@ideal.quotient.field _ _ I h)},
{intro h,
exact @maximal_ideal_of_is_field_quotient R _ I h,}
end

theorem dedekind_domain_of_number_ring (K : Type) [number_field K] : dedekind_id (number_ring K) := {
noetherian := sorry,
int_closed := sorry,
max_nonzero_primes := (begin
intros P hP hPp,
have hid : integral_domain P.quotient, exact @ideal.quotient.integral_domain _ _ P hPp,
have hfin : fintype P.quotient, {sorry},
have hf : is_field (P.quotient), {sorry},
exact @maximal_ideal_of_is_field_quotient (number_ring K) _ P hf,
end)}


I defined a number field (hopefully this definition works) and I proved that the field has to be infinite (though I am not sure what this fact will be used for yet). I defined a number ring and attempted to start proving that it is a dedekind domain, but I needed a theorem for that.

#### Ashvni Narayanan (Aug 30 2020 at 15:02):

Alexandru-Andrei Bosinta said:

Ashvni Narayanan I say we compare definitions and whatever work each of us done on it. I didn't get to do much though, but I can give you the work I did so far. There is probably a better way to do this, but I find it easiest to post it here for now.

import algebra.field
import data.rat.basic
import ring_theory.algebra
import ring_theory.algebraic
import ring_theory.integral_closure

open function
open_locale classical big_operators

def is_integrally_closed_domain (R : Type) [comm_ring R] : Prop := ∀ {r s : R}, s ≠ 0 → (∃ (n : ℕ) (f : ℕ → R)
(hf : f 0 = 1), ∑ ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0) → s ∣ r

class dedekind_id (R : Type) [integral_domain R] : Prop :=
(noetherian : is_noetherian_ring R)
(int_closed : is_integrally_closed_domain R)
(max_nonzero_primes : ∀ P : ideal R, P ≠ ⊥ → P.is_prime → P.is_maximal)

class number_field (K : Type) :=
(fld : field K)
(alg : algebra ℚ K)
(fd : finite_dimensional ℚ K)

instance field_of_number_field (K : Type) [number_field K] : field K := _inst_1.fld

instance algebra_of_number_field (K : Type) [number_field K] : algebra ℚ K := _inst_1.alg

instance infinite_of_number_field (K : Type) [number_field K] : infinite K := begin
let f : ℤ → K := (λ n, (n : ℚ) • (1 : K)),
apply infinite.of_injective f,
intros x y hxy,
have hxy2 : (x : ℚ) • (1 : K) = (y : ℚ) • (1 : K), exact hxy,
have h : 0 = ((x : ℚ) - (y : ℚ)) • (1 : K), calc 0 = (x : ℚ) • (1 : K) - (y : ℚ) • (1 : K) : by rw sub_eq_zero.mpr hxy
... = (x : ℚ) • (1 : K) + (-((y : ℚ) • (1 : K))) : sub_eq_add_neg (↑x • 1) (↑y • 1)
... = (x : ℚ) • (1 : K) + ((-(y : ℚ)) • (1 : K)) : by rw neg_smul
... = ((x : ℚ) + (-(y : ℚ))) • (1 : K) : by rw add_smul
... = ((x : ℚ) - (y : ℚ)) • (1 : K) : by rw sub_eq_add_neg,
have h2 : ((x : ℚ) - (y : ℚ)) = 0 ∨ (1 : K) = 0, {exact (@smul_eq_zero ℚ K _ _ _ ((x : ℚ) - (y : ℚ)) (1 : K)).1 (eq.symm h)},
cases h2, {have h3 : (x : ℚ) = (y : ℚ), exact sub_eq_zero.mp h2,
exact (rat.coe_int_inj (x : ℤ) (y : ℤ)).1 h3},
{exfalso, revert h2, simp}
end

def number_ring (K : Type) [number_field K] := @integral_closure ℤ K _ (@field.to_comm_ring K _inst_1.fld) _

theorem integral_domain_of_number_ring (K : Type) [number_field K] : integral_domain (number_ring K) :=
(number_ring K).integral_domain

example (K : Type) [field K] (x : K) (h : x ≠ 0): x * (field.inv x) = 1 := field.mul_inv_cancel h

/-- A predicate to express that a ring is a field.

This is mainly useful because such a predicate does not contain data,
and can therefore be easily transported along ring isomorphisms. -/
structure is_field (R : Type) [ring R] : Prop :=
(exists_pair_ne : ∃ (x y : R), x ≠ y)
(mul_comm : ∀ (x y : R), x * y = y * x)
(mul_inv_cancel' : ∀ {a : R}, a ≠ 0 → ∃ b, a * b = 1)

/-- Every field satisfies the predicate for integral domains. -/
lemma field.to_is_field (R : Type) [field R] : is_field R :=
{mul_inv_cancel' := λ a ha, ⟨a⁻¹, field.mul_inv_cancel ha⟩,
.. (‹_› : field R) }

noncomputable def is_field.to_field (R : Type) [ring R] (h : is_field R) : field R :=
{inv := (λ a, if ha : a = 0 then 0 else classical.some (is_field.mul_inv_cancel' h ha)),
inv_zero := (dif_pos rfl),
mul_inv_cancel := (λ a ha, begin
convert classical.some_spec (is_field.mul_inv_cancel' h ha),
exact dif_neg ha
end),
.._inst_1, ..h}

/-- There is a unique inverse in a field.
-/
lemma uniq_inv_of_is_field (R : Type) [comm_ring R] [is_field R]: ∀ (x : R), x ≠ 0 → ∃! (y : R), x * y = 1 := begin
intros x hx,
apply exists_unique_of_exists_of_unique,
{exact _inst_2.mul_inv_cancel' hx},
intros y z hxy hxz,
calc y = y * 1 : eq.symm (mul_one y)
... = y * (x * z) : by rw hxz
... = (y * x) * z : eq.symm (mul_assoc y x z)
... = (x * y) * z : by rw mul_comm y x
... = 1 * z : by rw hxy
... = z : one_mul z
end

/-- If the quotient of a comm_ring by an ideal is a field, then the ideal is maximal
-/
lemma maximal_ideal_of_is_field_quotient (R : Type) [comm_ring R] (I : ideal R)
[@is_field I.quotient (comm_ring.to_ring (ideal.quotient I))] : I.is_maximal := begin
apply ideal.is_maximal_iff.2,
split, {intro h,
rcases (_inst_2.exists_pair_ne) with ⟨⟨x⟩, ⟨y⟩, hxy⟩,
apply hxy,
apply ideal.quotient.eq.2,
rw ←mul_one (x-y),
apply submodule.smul_mem',
exact h},
{intros J x hIJ hxnI hxJ,
have hxn0 : (ideal.quotient.mk I x) ≠ 0,
{exact @mt ((ideal.quotient.mk I x) = 0) (x ∈ I) ideal.quotient.eq_zero_iff_mem.1 hxnI},
have hinvx : ∃ (y : I.quotient), (ideal.quotient.mk I x) * y = 1, {exact _inst_2.mul_inv_cancel' hxn0},
rcases hinvx with ⟨⟨y⟩, hy⟩,
change (ideal.quotient.mk I x) * (ideal.quotient.mk I y) = 1 at hy,
rw ←((ideal.quotient.mk I).map_mul x y) at hy,
have hxy1I : x*y-1 ∈ I, exact ideal.quotient.eq.1 hy,
have hxy1J : x*y-1 ∈ J, exact hIJ hxy1I,
have hxyJ : x*y ∈ J, exact ideal.mul_mem_right J hxJ,
have hend : x*y-(x*y-1) ∈ J, exact ideal.sub_mem J hxyJ hxy1J,
have h1 : 1 = x*y-(x*y-1), by ring,
rw h1,
exact hend}
end

/-- The quotient of a ring by an ideal is a field iff the ideal is maximal.
-/
theorem maximal_ideal_iff_is_field_quotient (R : Type) [comm_ring R] (I : ideal R) :
I.is_maximal ↔ (@is_field I.quotient (comm_ring.to_ring (ideal.quotient I))) := begin
split,
{intro h,
exact @field.to_is_field I.quotient (@ideal.quotient.field _ _ I h)},
{intro h,
exact @maximal_ideal_of_is_field_quotient R _ I h,}
end

theorem dedekind_domain_of_number_ring (K : Type) [number_field K] : dedekind_id (number_ring K) := {
noetherian := sorry,
int_closed := sorry,
max_nonzero_primes := (begin
intros P hP hPp,
have hid : integral_domain P.quotient, exact @ideal.quotient.integral_domain _ _ P hPp,
have hfin : fintype P.quotient, {sorry},
have hf : is_field (P.quotient), {sorry},
exact @maximal_ideal_of_is_field_quotient (number_ring K) _ P hf,
end)}


I defined a number field (hopefully this definition works) and I proved that the field has to be infinite (though I am not sure what this fact will be used for yet). I defined a number ring and attempted to start proving that it is a dedekind domain, but I needed a theorem for that.

Thanks a lot, this is very helpful!

#### Alexandru-Andrei Bosinta (Aug 30 2020 at 18:12):

@Kevin Buzzard I wrote the theorem (quotient by an ideal is a field iff the ideal is maximal) and I want to make a pull request. I read from the page "How to contribute to mathlib", so I would like to ask for write access to a non-master branch. I don't really know who to ask (or even if what I am asking makes sense, but that is what that page tells you to ask for). My github username is AlexandruBosinta.

#### Kevin Buzzard (Aug 30 2020 at 18:13):

Your docstring comment /-- Every field satisfies the predicate for integral domains. -/ should probably say ...for fields

#### Bryan Gin-ge Chen (Aug 30 2020 at 18:13):

@Alexandru-Andrei Bosinta Invite sent! https://github.com/leanprover-community/mathlib/invitations

#### Alexandru-Andrei Bosinta (Aug 30 2020 at 18:14):

Yeah, I changed it. That was what was originally written there (I took it directly from some code you posted on another thread) and I didn't initially change it.

#### Kenji Nakagawa (Aug 31 2020 at 13:58):

It's worth mentioning @Alexandru-Andrei Bosinta and @Ashvni Narayanan that there's a thread in #maths called "Dedekind Domains" which should be of interest.

#### Kevin Buzzard (Aug 31 2020 at 14:02):

Yes, this thread is poorly named now and hence will be hard to find later

#### Ashvni Narayanan (Aug 31 2020 at 14:17):

Kenji Nakagawa said:

It's worth mentioning Alexandru-Andrei Bosinta and Ashvni Narayanan that there's a thread in #maths called "Dedekind Domains" which should be of interest.

Thank you!

Last updated: May 11 2021 at 14:11 UTC