Weird Type Mismatch error

Stream: new members

[Alexandru-Andrei Bosinta]

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]

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

[Kevin Buzzard]

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]

And hence two different zeros

[Kevin Buzzard]

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]

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]

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]

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]

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)

Your version:

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]

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]

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]

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]

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]

Can you extend group with zero instead?

[Kevin Buzzard]

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]

And you can work out inv from the other data

[Alexandru-Andrei Bosinta]

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]

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]

A ring is a monoid with 0

[Kevin Buzzard]

A division ring is a group with zero

[Kevin Buzzard]

A commutative division ring is a field

[Alexandru-Andrei Bosinta]

Oh nvm, I got confused

[Alexandru-Andrei Bosinta]

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]

The technical issue here in the background is the following

[Alexandru-Andrei Bosinta]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

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

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

[Adam Topaz]

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

[Adam Topaz]

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

[Adam Topaz]

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

[Johan Commelin]

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

[Adam Topaz]

Infinite finitely generated fields are all anabelian :wink:

[Johan Commelin]

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

[Adam Topaz]

Lol I just use the Kronecker dimension in general.

[Kevin Buzzard]

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]

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

[Adam Topaz]

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

[Kevin Buzzard]

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

[Adam Topaz]

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

[Kevin Buzzard]

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]

Use the groupoid?

[Kevin Buzzard]

All the Langlandsy stuff should be canonically independent of everything

[Kevin Buzzard]

Maybe the groupoid is the way to go

[Adam Topaz]

This issue is all over the place in anabelian geometry.

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

Adam Topaz said:

Aaron Anderson would just work in a "monster model"

One universe up, just because we can

[Ashvni Narayanan]

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]

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

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]

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

You ask @maintainers

[Kevin Buzzard]

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

[Bryan Gin-ge Chen]

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

[Alexandru-Andrei Bosinta]

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]

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]

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

[Ashvni Narayanan]

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!