feat(ring_theory/dedekind_domain): definitions (#4000)

Defines `is_dedekind_domain` in three variants:

1.  `is_dedekind_domain`: Noetherian, Integrally closed, Krull dimension 1, thanks to @Vierkantor 
2. `is_dedekind_domain_dvr`: Noetherian, localization at every nonzero prime is a DVR
3. `is_dedekind_domain_inv`: Every nonzero ideal is invertible.

TODO: prove that these definitions are equivalent.

This PR also includes some misc. lemmas required to show the definitions are independent of choice of fraction field.

Co-Authored-By: mushokunosora <knaka3435@gmail.com>
Co-Authored-By: faenuccio <filippo.nuccio@univ-st-etienne.fr>
Co-Authored-By: Vierkantor <vierkantor@vierkantor.com>



Co-authored-by: Anne Baanen <t.baanen@vu.nl>
Co-authored-by: mushokunosora <38799099+mushokunosora@users.noreply.github.com>
Co-authored-by: Vierkantor <vierkantor@vierkantor.com>
Co-authored-by: Rob Lewis <Rob.y.lewis@gmail.com>
Co-authored-by: Vierkantor <Vierkantor@users.noreply.github.com>

Author: 3 people

docs/references.bib

@@ -369,3 +369,18 @@ @book{Hofstadter-1979
       series        = "Penguin books",
       year          = "1979",
 }
+
+@book{marcus1977number,
+  title={Number fields},
+  author={Marcus, Daniel A and Sacco, Emanuele},
+  volume={2},
+  year={1977},
+  publisher={Springer}
+}
+
+@book{cassels1967algebraic,
+  title={Algebraic number theory: proceedings of an instructional conference},
+  author={Cassels, John William Scott and Fr{\"o}lich, Albrecht},
+  year={1967},
+  publisher={Academic Pr}
+}

src/ring_theory/algebra.lean

@@ -484,6 +484,7 @@ namespace alg_equiv
 variables {R : Type u} {A₁ : Type v} {A₂ : Type w} {A₃ : Type u₁}
 variables [comm_semiring R] [semiring A₁] [semiring A₂] [semiring A₃]
 variables [algebra R A₁] [algebra R A₂] [algebra R A₃]
+variables (e : A₁ ≃ₐ[R] A₂)
 
 instance : has_coe_to_fun (A₁ ≃ₐ[R] A₂) := ⟨_, alg_equiv.to_fun⟩
 
@@ -511,7 +512,7 @@ rfl
 
 @[simp] lemma to_fun_apply {e : A₁ ≃ₐ[R] A₂} {a : A₁} : e.to_fun a = e a := rfl
 
-@[simp, norm_cast] lemma coe_ring_equiv (e : A₁ ≃ₐ[R] A₂) : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := rfl
+@[simp, norm_cast] lemma coe_ring_equiv : ((e : A₁ ≃+* A₂) : A₁ → A₂) = e := rfl
 
 lemma coe_ring_equiv_injective : function.injective (λ e : A₁ ≃ₐ[R] A₂, (e : A₁ ≃+* A₂)) :=
 begin
@@ -522,15 +523,15 @@ begin
   exact congr_fun w a,
 end
 
-@[simp] lemma map_add (e : A₁ ≃ₐ[R] A₂) : ∀ x y, e (x + y) = e x + e y := e.to_add_equiv.map_add
+@[simp] lemma map_add : ∀ x y, e (x + y) = e x + e y := e.to_add_equiv.map_add
 
-@[simp] lemma map_zero (e : A₁ ≃ₐ[R] A₂) : e 0 = 0 := e.to_add_equiv.map_zero
+@[simp] lemma map_zero : e 0 = 0 := e.to_add_equiv.map_zero
 
-@[simp] lemma map_mul (e : A₁ ≃ₐ[R] A₂) : ∀ x y, e (x * y) = (e x) * (e y) := e.to_mul_equiv.map_mul
+@[simp] lemma map_mul : ∀ x y, e (x * y) = (e x) * (e y) := e.to_mul_equiv.map_mul
 
-@[simp] lemma map_one (e : A₁ ≃ₐ[R] A₂) : e 1 = 1 := e.to_mul_equiv.map_one
+@[simp] lemma map_one : e 1 = 1 := e.to_mul_equiv.map_one
 
-@[simp] lemma commutes (e : A₁ ≃ₐ[R] A₂) : ∀ (r : R), e (algebra_map R A₁ r) = algebra_map R A₂ r :=
+@[simp] lemma commutes : ∀ (r : R), e (algebra_map R A₁ r) = algebra_map R A₂ r :=
   e.commutes'
 
 @[simp] lemma map_neg {A₁ : Type v} {A₂ : Type w}
@@ -541,21 +542,30 @@ end
   [ring A₁] [ring A₂] [algebra R A₁] [algebra R A₂] (e : A₁ ≃ₐ[R] A₂) :
   ∀ x y, e (x - y) = e x - e y := e.to_add_equiv.map_sub
 
-lemma map_sum (e : A₁ ≃ₐ[R] A₂) {ι : Type*} (f : ι → A₁) (s : finset ι) :
+lemma map_sum {ι : Type*} (f : ι → A₁) (s : finset ι) :
   e (∑ x in s, f x) = ∑ x in s, e (f x) :=
 e.to_add_equiv.map_sum f s
 
+/-- Interpret an algebra equivalence as an algebra homomorphism.
+
+This definition is included for symmetry with the other `to_*_hom` projections.
+The `simp` normal form is to use the coercion of the `has_coe_to_alg_hom` instance. -/
+def to_alg_hom : A₁ →ₐ[R] A₂ :=
+{ map_one' := e.map_one, map_zero' := e.map_zero, ..e }
+
 instance has_coe_to_alg_hom : has_coe (A₁ ≃ₐ[R] A₂) (A₁ →ₐ[R] A₂) :=
-  ⟨λ e, { map_one' := e.map_one, map_zero' := e.map_zero, ..e }⟩
+⟨to_alg_hom⟩
+
+@[simp] lemma to_alg_hom_eq_coe : e.to_alg_hom = e := rfl
 
-@[simp, norm_cast] lemma coe_alg_hom (e : A₁ ≃ₐ[R] A₂) : ((e : A₁ →ₐ[R] A₂) : A₁ → A₂) = e :=
-  rfl
+@[simp, norm_cast] lemma coe_alg_hom : ((e : A₁ →ₐ[R] A₂) : A₁ → A₂) = e :=
+rfl
 
-lemma injective (e : A₁ ≃ₐ[R] A₂) : function.injective e := e.to_equiv.injective
+lemma injective : function.injective e := e.to_equiv.injective
 
-lemma surjective (e : A₁ ≃ₐ[R] A₂) : function.surjective e := e.to_equiv.surjective
+lemma surjective : function.surjective e := e.to_equiv.surjective
 
-lemma bijective (e : A₁ ≃ₐ[R] A₂) : function.bijective e := e.to_equiv.bijective
+lemma bijective : function.bijective e := e.to_equiv.bijective
 
 instance : has_one (A₁ ≃ₐ[R] A₁) := ⟨{commutes' := λ r, rfl, ..(1 : A₁ ≃+* A₁)}⟩
 
@@ -625,6 +635,29 @@ def to_linear_equiv (e : A₁ ≃ₐ[R] A₂) : A₁ ≃ₗ[R] A₂ :=
 
 @[simp] lemma to_linear_equiv_apply (e : A₁ ≃ₐ[R] A₂) (x : A₁) : e.to_linear_equiv x = e x := rfl
 
+theorem to_linear_equiv_inj {e₁ e₂ : A₁ ≃ₐ[R] A₂} (H : e₁.to_linear_equiv = e₂.to_linear_equiv) :
+  e₁ = e₂ :=
+ext $ λ x, show e₁.to_linear_equiv x = e₂.to_linear_equiv x, by rw H
+
+/-- Interpret an algebra equivalence as a linear map. -/
+def to_linear_map : A₁ →ₗ[R] A₂ :=
+e.to_alg_hom.to_linear_map
+
+@[simp] lemma to_alg_hom_to_linear_map :
+  (e : A₁ →ₐ[R] A₂).to_linear_map = e.to_linear_map := rfl
+
+@[simp] lemma to_linear_equiv_to_linear_map :
+  e.to_linear_equiv.to_linear_map = e.to_linear_map := rfl
+
+@[simp] lemma to_linear_map_apply (x : A₁) : e.to_linear_map x = e x := rfl
+
+theorem to_linear_map_inj {e₁ e₂ : A₁ ≃ₐ[R] A₂} (H : e₁.to_linear_map = e₂.to_linear_map) :
+  e₁ = e₂ :=
+ext $ λ x, show e₁.to_linear_map x = e₂.to_linear_map x, by rw H
+
+@[simp] lemma trans_to_linear_map (f : A₁ ≃ₐ[R] A₂) (g : A₂ ≃ₐ[R] A₃) :
+  (f.trans g).to_linear_map = g.to_linear_map.comp f.to_linear_map := rfl
+
 end alg_equiv
 
 namespace algebra
@@ -908,6 +941,10 @@ theorem map_le {S : subalgebra R A} {f : A →ₐ[R] B} {U : subalgebra R B} :
   map S f ≤ U ↔ S ≤ comap' U f :=
 set.image_subset_iff
 
+lemma mem_map {S : subalgebra R A} {f : A →ₐ[R] B} {y : B} :
+  y ∈ map S f ↔ ∃ x ∈ S, f x = y :=
+subsemiring.mem_map
+
 instance integral_domain {R A : Type*} [comm_ring R] [integral_domain A] [algebra R A]
   (S : subalgebra R A) : integral_domain S :=
 @subring.domain A _ S _

src/ring_theory/algebra_operations.lean

@@ -279,6 +279,24 @@ lemma mem_div_iff_smul_subset {x : A} {I J : submodule R A} : x ∈ I / J ↔ x
   λ h y hy, h (set.smul_mem_smul_set hy) ⟩
 
 lemma le_div_iff {I J K : submodule R A} : I ≤ J / K ↔ ∀ (x ∈ I) (z ∈ K), x * z ∈ J := iff.refl _
+
+@[simp] lemma map_div {B : Type*} [comm_ring B] [algebra R B]
+  (I J : submodule R A) (h : A ≃ₐ[R] B) :
+  (I / J).map h.to_linear_map = I.map h.to_linear_map / J.map h.to_linear_map :=
+begin
+  ext x,
+  simp only [mem_map, mem_div_iff_forall_mul_mem],
+  split,
+  { rintro ⟨x, hx, rfl⟩ _ ⟨y, hy, rfl⟩,
+    exact ⟨x * y, hx _ hy, h.map_mul x y⟩ },
+  { rintro hx,
+    refine ⟨h.symm x, λ z hz, _, h.apply_symm_apply x⟩,
+    obtain ⟨xz, xz_mem, hxz⟩ := hx (h z) ⟨z, hz, rfl⟩,
+    convert xz_mem,
+    apply h.injective,
+    erw [h.map_mul, h.apply_symm_apply, hxz] }
+end
+
 end quotient
 
 end comm_ring

src/ring_theory/dedekind_domain.lean

@@ -0,0 +1,140 @@
+/-
+Copyright (c) 2020 Kenji Nakagawa. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenji Nakagawa, Anne Baanen, Filippo A. E. Nuccio
+-/
+import ring_theory.discrete_valuation_ring
+import ring_theory.fractional_ideal
+import ring_theory.ideal.over
+
+/-!
+# Dedekind domains
+
+This file defines the notion of a Dedekind domain (or Dedekind ring),
+giving three equivalent definitions (TODO: and shows that they are equivalent).
+
+## Main definitions
+
+ - `is_dedekind_domain` defines a Dedekind domain as a commutative ring that is not a field,
+   Noetherian, integrally closed in its field of fractions and has Krull dimension exactly one.
+   `is_dedekind_domain_iff` shows that this does not depend on the choice of field of fractions.
+ - `is_dedekind_domain_dvr` alternatively defines a Dedekind domain as an integral domain that is not a field,
+   Noetherian, and the localization at every nonzero prime ideal is a discrete valuation ring.
+ - `is_dedekind_domain_inv` alternatively defines a Dedekind domain as an integral domain that is not a field,
+   and every nonzero fractional ideal is invertible.
+ - `is_dedekind_domain_inv_iff` shows that this does note depend on the choice of field of fractions.
+
+## Implementation notes
+
+The definitions that involve a field of fractions choose a canonical field of fractions,
+but are independent of that choice. The `..._iff` lemmas express this independence.
+
+## References
+
+* [D. Marcus, *Number Fields*][marcus1977number]
+* [J.W.S. Cassels, A. Frölich, *Algebraic Number Theory*][cassels1967algebraic]
+
+## Tags
+
+dedekind domain, dedekind ring
+-/
+
+variables (R A K : Type*) [comm_ring R] [integral_domain A] [field K]
+
+/-- A ring `R` has Krull dimension at most one if all nonzero prime ideals are maximal. -/
+def ring.dimension_le_one : Prop :=
+∀ p ≠ (⊥ : ideal R), p.is_prime → p.is_maximal
+
+open ideal ring
+
+namespace ring
+
+lemma dimension_le_one.principal_ideal_ring
+  [is_principal_ideal_ring A] : dimension_le_one A :=
+λ p nonzero prime, by { haveI := prime, exact is_prime.to_maximal_ideal nonzero }
+
+lemma dimension_le_one.integral_closure [nontrivial R] [algebra R A]
+  (h : dimension_le_one R) : dimension_le_one (integral_closure R A) :=
+begin
+  intros p ne_bot prime,
+  haveI := prime,
+  refine integral_closure.is_maximal_of_is_maximal_comap p
+    (h _ (integral_closure.comap_ne_bot ne_bot) _),
+  apply is_prime.comap
+end
+end ring
+
+/--
+A Dedekind domain is an integral domain that is Noetherian, integrally closed, and
+has Krull dimension exactly one (`not_is_field` and `dimension_le_one`).
+
+The integral closure condition is independent of the choice of field of fractions:
+use `is_dedekind_domain_iff` to prove `is_dedekind_domain` for a given `fraction_map`.
+
+This is the default implementation, but there are equivalent definitions,
+`is_dedekind_domain_dvr` and `is_dedekind_domain_inv`.
+TODO: Prove that these are actually equivalent definitions.
+-/
+class is_dedekind_domain : Prop :=
+(not_is_field : ¬ is_field A)
+(is_noetherian_ring : is_noetherian_ring A)
+(dimension_le_one : dimension_le_one A)
+(is_integrally_closed : integral_closure A (fraction_ring A) = ⊥)
+
+/-- An integral domain is a Dedekind domain iff and only if it is not a field, is Noetherian, has dimension ≤ 1,
+and is integrally closed in a given fraction field.
+In particular, this definition does not depend on the choice of this fraction field. -/
+lemma is_dedekind_domain_iff (f : fraction_map A K) :
+  is_dedekind_domain A ↔
+    (¬ is_field A) ∧ is_noetherian_ring A ∧ dimension_le_one A ∧
+    integral_closure A f.codomain = ⊥ :=
+⟨λ ⟨hf, hr, hd, hi⟩, ⟨hf, hr, hd,
+  by rw [←integral_closure_map_alg_equiv (fraction_ring.alg_equiv_of_quotient f),
+         hi, algebra.map_bot]⟩,
+ λ ⟨hf, hr, hd, hi⟩, ⟨hf, hr, hd,
+  by rw [←integral_closure_map_alg_equiv (fraction_ring.alg_equiv_of_quotient f).symm,
+         hi, algebra.map_bot]⟩⟩
+
+/--
+A Dedekind domain is an integral domain that is not a field, is Noetherian, and the localization at
+every nonzero prime is a discrete valuation ring.
+
+This is equivalent to `is_dedekind_domain`.
+TODO: prove the equivalence.
+-/
+structure is_dedekind_domain_dvr : Prop :=
+(not_is_field : ¬ is_field A)
+(is_noetherian_ring : is_noetherian_ring A)
+(is_dvr_at_nonzero_prime : ∀ P ≠ (⊥ : ideal A), P.is_prime →
+  discrete_valuation_ring (localization.at_prime P))
+
+/--
+A Dedekind domain is an integral domain that is not a field such that every fractional ideal has an inverse.
+
+This is equivalent to `is_dedekind_domain`.
+TODO: prove the equivalence.
+-/
+structure is_dedekind_domain_inv : Prop :=
+(not_is_field : ¬ is_field A)
+(mul_inv_cancel : ∀ I ≠ (⊥ : fractional_ideal (fraction_ring.of A)), I * I⁻¹ = 1)
+
+section
+
+open ring.fractional_ideal
+
+lemma is_dedekind_domain_inv_iff (f : fraction_map A K) :
+  is_dedekind_domain_inv A ↔
+    (¬ is_field A) ∧ (∀ I ≠ (⊥ : fractional_ideal f), I * I⁻¹ = 1) :=
+begin
+  split; rintros ⟨hf, hi⟩; use hf; intros I hI,
+  { have := hi (map (fraction_ring.alg_equiv_of_quotient f).symm.to_alg_hom I) (map_ne_zero _ hI),
+    erw [← map_inv, ← fractional_ideal.map_mul] at this,
+    convert congr_arg (map (fraction_ring.alg_equiv_of_quotient f).to_alg_hom) this;
+      simp only [alg_equiv.to_alg_hom_eq_coe, map_symm_map, map_one] },
+  { have := hi (map (fraction_ring.alg_equiv_of_quotient f).to_alg_hom I) (map_ne_zero _ hI),
+    erw [← map_inv, ← fractional_ideal.map_mul] at this,
+    convert congr_arg (map (fraction_ring.alg_equiv_of_quotient f).symm.to_alg_hom) this;
+      simp only [alg_equiv.to_alg_hom_eq_coe, map_map_symm, map_one] }
+end
+
+end