refactor(ring_theory): turn localization_map into a typeclass (#8119)

This PR replaces the previous `localization_map (M : submodule R) Rₘ` definition (a ring hom `R →+* Rₘ` that presents `Rₘ` as the localization of `R` at `M`) with a new `is_localization M Rₘ` typeclass that puts these requirements on `algebra_map R Rₘ` instead. An important benefit is that we no longer need to mess with `localization_map.codomain` to put an `R`-algebra structure on `Rₘ`, we can just work with `Rₘ` directly.

The important API changes are in commit 0de78dc, all other commits are simply fixes to the dependent files.

Main changes:
 * `localization_map` has been replaced with `is_localization`, similarly `away_map` -> `is_localization.away`, `localization_map.at_prime` -> `is_localization.at_prime` and `fraction_map` -> `is_fraction_ring`
 * many declarations taking the `localization_map` as a parameter now take `R` and/or `M` and/or `Rₘ`, depending on what can be inferred easily
 * `localization_map.to_map` has been replaced with `algebra_map R Rₘ`
 * `localization_map.codomain` and its instances have been removed (you can now directly use `Rₘ`)
 * `is_localization.alg_equiv` generalizes `fraction_map.alg_equiv_of_quotient` (which has been renamed to `is_fraction_ring.alg_equiv`)
 * `is_localization.sec` has been introduced to replace `(to_localization_map _ _).sec`
 * `localization.of` have been replaced with `algebra` and `is_localization` instances on `localization`, similarly for `localization.away.of`, `localization.at_prime.of` and `fraction_ring.of`.
 * `int.fraction_map` is now an instance `rat.is_fraction_ring`
 * All files depending on the above definitions have had fixes. These were mostly straightforward, except:
 * [Some category-theory arrows in `algebraic_geometry/structure.sheaf` are now plain `ring_hom`s. This change was suggested by @justus-springer in order to help the elaborator figure out the arguments to  `is_localization`.](cf3acc9)
 * Deleted `minpoly.over_int_eq_over_rat` and `minpoly.integer_dvd`, now you can just use `gcd_domain_eq_field_fractions` or `gcd_domain_dvd` respectively. [This removes code duplication in `minpoly.lean`](5695924)
 * `fractional_ideal` does not need to assume `is_localization` everywhere, only for certain specific definitions

Things that stay the same:
 * `localization`, `localization.away`, `localization.at_prime` and `fraction_ring` are still a construction of localizations (although see above for `{localization,localization.away,localization.at_prime,fraction_ring}.of`)

Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Refactoring.20.60localization_map.60

Author: Vierkantor

docs/overview.yaml

@@ -104,7 +104,7 @@ General algebra:
     algebraically closed field: 'is_alg_closed'
     existence of algebraic closure of a field: 'algebraic_closure'
     $\C$ is algebraically closed: 'complex.exists_root'
-    field of fractions of an integral domain: 'fraction_map'
+    field of fractions of an integral domain: 'is_fraction_ring'
     algebraic extension: 'algebra.is_algebraic'
     rupture field: 'adjoin_root'
     splitting field: 'polynomial.splitting_field'

docs/undergrad.yaml

@@ -178,7 +178,7 @@ Ring Theory:
     field $\R$ of real numbers: 'real.division_ring'
     field $\C$ of complex numbers: 'complex.field'
     $\C$ is algebraically closed: 'complex.exists_root'
-    field of fractions of an integral domain: 'fraction_map'
+    field of fractions of an integral domain: 'is_fraction_ring'
     algebraic elements: 'is_algebraic'
     transcendental elements: 'transcendental'
     algebraic extensions: 'algebra.is_algebraic'

src/algebra/char_p/algebra.lean

@@ -68,16 +68,25 @@ char_zero_of_injective_algebra_map free_algebra.algebra_map_left_inverse.injecti
 
 end free_algebra
 
-namespace fraction_ring
+namespace is_fraction_ring
 
-variables {R : Type*} [integral_domain R] (p : ℕ)
+variables (R : Type*) {K : Type*} [integral_domain R] [field K] [algebra R K] [is_fraction_ring R K]
+variables (p : ℕ)
+
+/-- If `R` has characteristic `p`, then so does Frac(R). -/
+lemma char_p_of_is_fraction_ring [char_p R p] : char_p K p :=
+char_p_of_injective_algebra_map (is_fraction_ring.injective R K) p
 
 /-- If `R` has characteristic `p`, then so does `fraction_ring R`. -/
 instance char_p [char_p R p] : char_p (fraction_ring R) p :=
-char_p_of_injective_algebra_map (fraction_map.injective (fraction_ring.of R)) p
+char_p_of_is_fraction_ring R p
+
+/-- If `R` has characteristic `0`, then so does Frac(R). -/
+lemma char_zero_of_is_fraction_ring [char_zero R] : char_zero K :=
+@char_p.char_p_to_char_zero K _ (char_p_of_is_fraction_ring R 0)
 
 /-- If `R` has characteristic `0`, then so does `fraction_ring R`. -/
 instance char_zero [char_zero R] : char_zero (fraction_ring R) :=
-char_p.char_p_to_char_zero (fraction_ring R)
+char_zero_of_is_fraction_ring R
 
-end fraction_ring
+end is_fraction_ring

src/algebraic_geometry/structure_sheaf.lean

@@ -325,67 +325,34 @@ section gcd_domain
 
 /-- For GCD domains, the minimal polynomial over the ring is the same as the minimal polynomial
 over the fraction field. -/
-lemma gcd_domain_eq_field_fractions {A K R : Type*} [integral_domain A]
-  [gcd_monoid A] [field K] [integral_domain R] (f : fraction_map A K) [algebra f.codomain R]
-  [algebra A R] [is_scalar_tower A f.codomain R] {x : R} (hx : is_integral A x) :
-  minpoly f.codomain x = (minpoly A x).map (localization_map.to_ring_hom f) :=
+lemma gcd_domain_eq_field_fractions {A R : Type*} (K : Type*) [integral_domain A]
+  [gcd_monoid A] [field K] [integral_domain R] [algebra A K] [is_fraction_ring A K]
+  [algebra K R] [algebra A R] [is_scalar_tower A K R] {x : R} (hx : is_integral A x) :
+  minpoly K x = (minpoly A x).map (algebra_map A K) :=
 begin
   symmetry,
   refine unique' _ _ _,
-  { exact (polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map f
-  (polynomial.monic.is_primitive (monic hx))).1 (irreducible hx) },
-  { have htower := is_scalar_tower.aeval_apply A f.codomain R x (minpoly A x),
-    simp only [localization_map.algebra_map_eq, aeval] at htower,
-    exact htower.symm },
-  { exact monic_map _ (monic hx) }
-end
-
-/-- The minimal polynomial over `ℤ` is the same as the minimal polynomial over `ℚ`. -/
---TODO use `gcd_domain_eq_field_fractions` directly when localizations are defined
--- in terms of algebras instead of `ring_hom`s
-lemma over_int_eq_over_rat {A : Type*} [integral_domain A] {x : A} [hℚA : algebra ℚ A]
-  (hx : is_integral ℤ x) :
-  minpoly ℚ x = map (int.cast_ring_hom ℚ) (minpoly ℤ x) :=
-begin
-  symmetry,
-  refine unique' _ _ _,
-  { exact (is_primitive.int.irreducible_iff_irreducible_map_cast
-  (polynomial.monic.is_primitive (monic hx))).1 (irreducible hx) },
-  { have htower := is_scalar_tower.aeval_apply ℤ ℚ A x (minpoly ℤ x),
-    simp only [localization_map.algebra_map_eq, aeval] at htower,
-    exact htower.symm },
+  { exact (polynomial.is_primitive.irreducible_iff_irreducible_map_fraction_map
+      (polynomial.monic.is_primitive (monic hx))).1 (irreducible hx) },
+  { have htower := is_scalar_tower.aeval_apply A K R x (minpoly A x),
+    rwa [aeval, eq_comm] at htower },
   { exact monic_map _ (monic hx) }
 end
 
 /-- For GCD domains, the minimal polynomial divides any primitive polynomial that has the integral
 element as root. -/
-lemma gcd_domain_dvd {A K R : Type*}
-  [integral_domain A] [gcd_monoid A] [field K] [integral_domain R]
-  (f : fraction_map A K) [algebra f.codomain R] [algebra A R] [is_scalar_tower A f.codomain R]
+lemma gcd_domain_dvd {A R : Type*} (K : Type*)
+  [integral_domain A] [gcd_monoid A] [field K] [integral_domain R] [algebra A K]
+  [is_fraction_ring A K] [algebra K R] [algebra A R] [is_scalar_tower A K R]
   {x : R} (hx : is_integral A x)
   {P : polynomial A} (hprim : is_primitive P) (hroot : polynomial.aeval x P = 0) :
   minpoly A x ∣ P :=
 begin
-  apply (is_primitive.dvd_iff_fraction_map_dvd_fraction_map f
-    (monic.is_primitive (monic hx)) hprim ).2,
-  rw [← gcd_domain_eq_field_fractions f hx],
-  refine dvd _ _ _,
-  rwa [← localization_map.algebra_map_eq, ← is_scalar_tower.aeval_apply]
-end
-
-/-- The minimal polynomial over `ℤ` divides any primitive polynomial that has the integral element
-as root. -/
--- TODO use `gcd_domain_dvd` directly when localizations are defined in terms of algebras
--- instead of `ring_hom`s
-lemma integer_dvd {A : Type*} [integral_domain A] [algebra ℚ A] {x : A} (hx : is_integral ℤ x)
-  {P : polynomial ℤ} (hprim : is_primitive P) (hroot : polynomial.aeval x P = 0) :
-  minpoly ℤ x ∣ P :=
-begin
-  apply (is_primitive.int.dvd_iff_map_cast_dvd_map_cast _ _
-    (monic.is_primitive (monic hx)) hprim ).2,
-  rw [← over_int_eq_over_rat hx],
+  apply (is_primitive.dvd_iff_fraction_map_dvd_fraction_map K
+    (monic.is_primitive (monic hx)) hprim).2,
+  rw ← gcd_domain_eq_field_fractions K hx,
   refine dvd _ _ _,
-  rwa [(int.cast_ring_hom ℚ).ext_int (algebra_map ℤ ℚ), ← is_scalar_tower.aeval_apply]
+  rwa ← is_scalar_tower.aeval_apply
 end
 
 end gcd_domain

src/field_theory/minpoly.lean

@@ -42,6 +42,8 @@ dedekind domain, dedekind ring
 
 variables (R A K : Type*) [comm_ring R] [integral_domain A] [field K]
 
+local notation R`⁰`:9000 := non_zero_divisors R
+
 /-- 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
@@ -82,16 +84,14 @@ class is_dedekind_domain : Prop :=
 /-- 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) :
+lemma is_dedekind_domain_iff (K : Type*) [field K] [algebra A K] [is_fraction_ring A K] :
   is_dedekind_domain A ↔
     (¬ is_field A) ∧ is_noetherian_ring A ∧ dimension_le_one A ∧
-    integral_closure A f.codomain = ⊥ :=
+    integral_closure A K = ⊥ :=
 ⟨λ ⟨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]⟩,
+  by rw [←integral_closure_map_alg_equiv (fraction_ring.alg_equiv A K), 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]⟩⟩
+  by rw [←integral_closure_map_alg_equiv (fraction_ring.alg_equiv A K).symm, hi, algebra.map_bot]⟩⟩
 
 /--
 A Dedekind domain is an integral domain that is not a field, is Noetherian, and the
@@ -110,25 +110,25 @@ section inverse
 
 open_locale classical
 
-variables {R₁ : Type*} [integral_domain R₁] {g : fraction_map R₁ K}
-variables {I J : fractional_ideal g}
+variables {R₁ : Type*} [integral_domain R₁] [algebra R₁ K] [is_fraction_ring R₁ K]
+variables {I J : fractional_ideal R₁⁰ K}
 
-noncomputable instance : has_inv (fractional_ideal g) := ⟨λ I, 1 / I⟩
+noncomputable instance : has_inv (fractional_ideal R₁⁰ K) := ⟨λ I, 1 / I⟩
 
 lemma inv_eq : I⁻¹ = 1 / I := rfl
 
-lemma inv_zero' : (0 : fractional_ideal g)⁻¹ = 0 := fractional_ideal.div_zero
+lemma inv_zero' : (0 : fractional_ideal R₁⁰ K)⁻¹ = 0 := fractional_ideal.div_zero
 
-lemma inv_nonzero {J : fractional_ideal g} (h : J ≠ 0) :
-J⁻¹ = ⟨(1 : fractional_ideal g) / J, fractional_ideal.fractional_div_of_nonzero h⟩ :=
+lemma inv_nonzero {J : fractional_ideal R₁⁰ K} (h : J ≠ 0) :
+J⁻¹ = ⟨(1 : fractional_ideal R₁⁰ K) / J, fractional_ideal.fractional_div_of_nonzero h⟩ :=
 fractional_ideal.div_nonzero _
 
-lemma coe_inv_of_nonzero {J : fractional_ideal g} (h : J ≠ 0) :
-  (↑J⁻¹ : submodule R₁ g.codomain) = g.coe_submodule 1 / J :=
+lemma coe_inv_of_nonzero {J : fractional_ideal R₁⁰ K} (h : J ≠ 0) :
+  (↑J⁻¹ : submodule R₁ K) = is_localization.coe_submodule K 1 / J :=
 by { rwa inv_nonzero _, refl, assumption}
 
 /-- `I⁻¹` is the inverse of `I` if `I` has an inverse. -/
-theorem right_inverse_eq (I J : fractional_ideal g) (h : I * J = 1) :
+theorem right_inverse_eq (I J : fractional_ideal R₁⁰ K) (h : I * J = 1) :
   J = I⁻¹ :=
 begin
   have hI : I ≠ 0 := fractional_ideal.ne_zero_of_mul_eq_one I J h,
@@ -148,27 +148,27 @@ begin
   exact fractional_ideal.mul_mem_mul hx hy
 end
 
-theorem mul_inv_cancel_iff {I : fractional_ideal g} :
+theorem mul_inv_cancel_iff {I : fractional_ideal R₁⁰ K} :
   I * I⁻¹ = 1 ↔ ∃ J, I * J = 1 :=
-⟨λ h, ⟨I⁻¹, h⟩, λ ⟨J, hJ⟩, by rwa [← @right_inverse_eq _ _ _ _ _ I J hJ]⟩
+⟨λ h, ⟨I⁻¹, h⟩, λ ⟨J, hJ⟩, by rwa ← right_inverse_eq K I J hJ⟩
 
-variables {K' : Type*} [field K'] {g' : fraction_map R₁ K'}
+variables {K' : Type*} [field K'] [algebra R₁ K'] [is_fraction_ring R₁ K']
 
-@[simp] lemma map_inv (I : fractional_ideal g) (h : g.codomain ≃ₐ[R₁] g'.codomain) :
-  (I⁻¹).map (h : g.codomain →ₐ[R₁] g'.codomain) = (I.map h)⁻¹ :=
+@[simp] lemma map_inv (I : fractional_ideal R₁⁰ K) (h : K ≃ₐ[R₁] K') :
+  (I⁻¹).map (h : K →ₐ[R₁] K') = (I.map h)⁻¹ :=
 by rw [inv_eq, fractional_ideal.map_div, fractional_ideal.map_one, inv_eq]
 
 open_locale classical
 
 open submodule submodule.is_principal
 
-@[simp] lemma span_singleton_inv (x : g.codomain) :
-  (fractional_ideal.span_singleton x)⁻¹ = fractional_ideal.span_singleton (x⁻¹) :=
+@[simp] lemma span_singleton_inv (x : K) :
+  (fractional_ideal.span_singleton R₁⁰ x)⁻¹ = fractional_ideal.span_singleton _ (x⁻¹) :=
 fractional_ideal.one_div_span_singleton x
 
-lemma mul_generator_self_inv (I : fractional_ideal g)
-  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
-  I * fractional_ideal.span_singleton (generator (I : submodule R₁ g.codomain))⁻¹ = 1 :=
+lemma mul_generator_self_inv (I : fractional_ideal R₁⁰ K)
+  [submodule.is_principal (I : submodule R₁ K)] (h : I ≠ 0) :
+  I * fractional_ideal.span_singleton _ (generator (I : submodule R₁ K))⁻¹ = 1 :=
 begin
   -- Rewrite only the `I` that appears alone.
   conv_lhs { congr, rw fractional_ideal.eq_span_singleton_of_principal I },
@@ -180,16 +180,16 @@ begin
     fractional_ideal.span_singleton_zero]
 end
 
-lemma invertible_of_principal (I : fractional_ideal g)
-  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
+lemma invertible_of_principal (I : fractional_ideal R₁⁰ K)
+  [submodule.is_principal (I : submodule R₁ K)] (h : I ≠ 0) :
   I * I⁻¹ = 1 :=
 (fractional_ideal.mul_div_self_cancel_iff).mpr
-  ⟨fractional_ideal.span_singleton (generator (I : submodule R₁ g.codomain))⁻¹,
-    @mul_generator_self_inv _ _ _ _ _ I _ h⟩
+  ⟨fractional_ideal.span_singleton _ (generator (I : submodule R₁ K))⁻¹,
+    mul_generator_self_inv _ I h⟩
 
-lemma invertible_iff_generator_nonzero (I : fractional_ideal g)
-  [submodule.is_principal (I : submodule R₁ g.codomain)] :
-  I * I⁻¹ = 1 ↔ generator (I : submodule R₁ g.codomain) ≠ 0 :=
+lemma invertible_iff_generator_nonzero (I : fractional_ideal R₁⁰ K)
+  [submodule.is_principal (I : submodule R₁ K)] :
+  I * I⁻¹ = 1 ↔ generator (I : submodule R₁ K) ≠ 0 :=
 begin
   split,
   { intros hI hg,
@@ -200,21 +200,21 @@ begin
     apply invertible_of_principal,
     rw [fractional_ideal.eq_span_singleton_of_principal I],
     intro hI,
-    have := fractional_ideal.mem_span_singleton_self (generator (I : submodule R₁ g.codomain)),
+    have := fractional_ideal.mem_span_singleton_self _ (generator (I : submodule R₁ K)),
     rw [hI, fractional_ideal.mem_zero_iff] at this,
     contradiction }
 end
 
-lemma is_principal_inv (I : fractional_ideal g)
-  [submodule.is_principal (I : submodule R₁ g.codomain)] (h : I ≠ 0) :
+lemma is_principal_inv (I : fractional_ideal R₁⁰ K)
+  [submodule.is_principal (I : submodule R₁ K)] (h : I ≠ 0) :
   submodule.is_principal (I⁻¹).1 :=
 begin
   rw [fractional_ideal.val_eq_coe, fractional_ideal.is_principal_iff],
-  use (generator (I : submodule R₁ g.codomain))⁻¹,
-  have hI : I  * fractional_ideal.span_singleton ((generator (I : submodule R₁ g.codomain))⁻¹)  = 1,
-  apply @mul_generator_self_inv _ _ _ _ _ I _ h,
-  apply (@right_inverse_eq _ _ _ _ _ I (fractional_ideal.span_singleton
-    ( (generator (I : submodule R₁ g.codomain))⁻¹)) hI).symm,
+  use (generator (I : submodule R₁ K))⁻¹,
+  have hI : I  * fractional_ideal.span_singleton _ ((generator (I : submodule R₁ K))⁻¹)  = 1,
+  apply mul_generator_self_inv _ I h,
+  exact (right_inverse_eq _ I (fractional_ideal.span_singleton _
+    ((generator (I : submodule R₁ K))⁻¹)) hI).symm
 end
 
 /--
@@ -226,22 +226,22 @@ 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 * (1 / I) = 1)
+(mul_inv_cancel : ∀ I ≠ (⊥ : fractional_ideal A⁰ (fraction_ring A)), I * (1 / I) = 1)
 
 open ring.fractional_ideal
 
-lemma is_dedekind_domain_inv_iff (f : fraction_map A K) :
+lemma is_dedekind_domain_inv_iff (K : Type*) [field K] [algebra A K] [is_fraction_ring A K] :
   is_dedekind_domain_inv A ↔
-    (¬ is_field A) ∧ (∀ I ≠ (⊥ : fractional_ideal f), I * I⁻¹ = 1) :=
+    (¬ is_field A) ∧ (∀ I ≠ (⊥ : fractional_ideal A⁰ K), I * I⁻¹ = 1) :=
 begin
-  set h : (fraction_ring.of A).codomain ≃ₐ[A] f.codomain := fraction_ring.alg_equiv_of_quotient f,
+  set h : fraction_ring A ≃ₐ[A] K := fraction_ring.alg_equiv A K,
   split; rintros ⟨hf, hi⟩; use hf; intros I hI,
   { have := hi (map ↑h.symm I) (map_ne_zero _ hI),
-    convert congr_arg (map (h : (fraction_ring.of A).codomain →ₐ[A] f.codomain)) this;
+    convert congr_arg (map (h : fraction_ring A →ₐ[A] K)) this;
       simp only [map_symm_map, map_one, fractional_ideal.map_mul, fractional_ideal.map_div,
                  inv_eq] },
   { have := hi (map ↑h I) (map_ne_zero _ hI),
-    convert congr_arg (map (h.symm : f.codomain →ₐ[A] (fraction_ring.of A).codomain)) this;
+    convert congr_arg (map (h.symm : K →ₐ[A] fraction_ring A)) this;
       simp only [map_map_symm, map_one, fractional_ideal.map_mul, fractional_ideal.map_div,
                  inv_eq] },
 end