feat(ring_theory/localization): fraction rings of algebraic extensions are algebraic (#11717)

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Author: Chris Hughes

src/ring_theory/algebraic.lean

@@ -72,18 +72,29 @@ by simp only [is_algebraic, alg_hom.injective_iff, not_forall, and.comm, exists_
 end
 
 section zero_ne_one
-variables (R : Type u) {A : Type v} [comm_ring R] [nontrivial R] [ring A] [algebra R A]
+variables (R : Type u) {S : Type*} {A : Type v} [comm_ring R]
+variables [comm_ring S] [ring A] [algebra R A] [algebra R S] [algebra S A]
+variables [is_scalar_tower R S A]
 
 /-- An integral element of an algebra is algebraic.-/
-lemma is_integral.is_algebraic {x : A} (h : is_integral R x) : is_algebraic R x :=
+lemma is_integral.is_algebraic [nontrivial R] {x : A} (h : is_integral R x) :
+  is_algebraic R x :=
 by { rcases h with ⟨p, hp, hpx⟩, exact ⟨p, hp.ne_zero, hpx⟩ }
 
 variables {R}
 
 /-- An element of `R` is algebraic, when viewed as an element of the `R`-algebra `A`. -/
-lemma is_algebraic_algebra_map (a : R) : is_algebraic R (algebra_map R A a) :=
+lemma is_algebraic_algebra_map [nontrivial R] (a : R) : is_algebraic R (algebra_map R A a) :=
 ⟨X - C a, X_sub_C_ne_zero a, by simp only [aeval_C, aeval_X, alg_hom.map_sub, sub_self]⟩
 
+lemma is_algebraic_algebra_map_of_is_algebraic {a : S} (h : is_algebraic R a) :
+  is_algebraic R (algebra_map S A a) :=
+begin
+  obtain ⟨f, hf₁, hf₂⟩ := h,
+  use [f, hf₁],
+  rw [← is_scalar_tower.algebra_map_aeval R S A, hf₂, ring_hom.map_zero]
+end
+
 end zero_ne_one
 
 section field
@@ -123,15 +134,26 @@ end
 
 variables (K L)
 
-/-- If A is an algebraic algebra over R, then A is algebraic over A when S is an extension of R,
+/-- If x is algebraic over R, then x is algebraic over S when S is an extension of R,
   and the map from `R` to `S` is injective. -/
-lemma is_algebraic_of_larger_base_of_injective (hinj : function.injective (algebra_map R S))
-  (A_alg : is_algebraic R A) : is_algebraic S A :=
-λ x, let ⟨p, hp₁, hp₂⟩ := A_alg x in
+lemma _root_.is_algebraic_of_larger_base_of_injective (hinj : function.injective (algebra_map R S))
+  {x : A} (A_alg : _root_.is_algebraic R x) : _root_.is_algebraic S x :=
+let ⟨p, hp₁, hp₂⟩ := A_alg in
 ⟨p.map (algebra_map _ _),
   by rwa [ne.def, ← degree_eq_bot, degree_map' hinj, degree_eq_bot],
   by simpa⟩
 
+/-- If A is an algebraic algebra over R, then A is algebraic over S when S is an extension of R,
+  and the map from `R` to `S` is injective. -/
+lemma is_algebraic_of_larger_base_of_injective (hinj : function.injective (algebra_map R S))
+  (A_alg : is_algebraic R A) : is_algebraic S A :=
+λ x, is_algebraic_of_larger_base_of_injective hinj (A_alg x)
+
+/-- If x is a algebraic over K, then x is algebraic over L when L is an extension of K -/
+lemma _root_.is_algebraic_of_larger_base {x : A} (A_alg : _root_.is_algebraic K x) :
+  _root_.is_algebraic L x :=
+_root_.is_algebraic_of_larger_base_of_injective (algebra_map K L).injective A_alg
+
 /-- If A is an algebraic algebra over K, then A is algebraic over L when L is an extension of K -/
 lemma is_algebraic_of_larger_base (A_alg : is_algebraic K A) : is_algebraic L A :=
 is_algebraic_of_larger_base_of_injective (algebra_map K L).injective A_alg

src/ring_theory/localization.lean

@@ -2662,6 +2662,14 @@ noncomputable instance : field (fraction_ring A) :=
   (algebra_map _ _ r / algebra_map A _ s : fraction_ring A) :=
 by rw [localization.mk_eq_mk', is_fraction_ring.mk'_eq_div]
 
+noncomputable instance [is_domain R] [field K] [algebra R K] [no_zero_smul_divisors R K] :
+  algebra (fraction_ring R) K :=
+ring_hom.to_algebra (is_fraction_ring.lift (no_zero_smul_divisors.algebra_map_injective R _))
+
+instance [is_domain R] [field K] [algebra R K] [no_zero_smul_divisors R K] :
+  is_scalar_tower R (fraction_ring R) K :=
+is_scalar_tower.of_algebra_map_eq (λ x, (is_fraction_ring.lift_algebra_map _ x).symm)
+
 variables (A)
 
 /-- Given an integral domain `A` and a localization map to a field of fractions
@@ -2672,3 +2680,50 @@ noncomputable def alg_equiv (K : Type*) [field K] [algebra A K] [is_fraction_rin
 localization.alg_equiv (non_zero_divisors A) K
 
 end fraction_ring
+
+namespace is_fraction_ring
+
+variables (R S K)
+
+/-- `S` is algebraic over `R` iff a fraction ring of `S` is algebraic over `R` -/
+lemma is_algebraic_iff' [field K] [is_domain R] [is_domain S] [algebra R K] [algebra S K]
+  [no_zero_smul_divisors R K] [is_fraction_ring S K] [is_scalar_tower R S K] :
+  algebra.is_algebraic R S ↔ algebra.is_algebraic R K :=
+begin
+  simp only [algebra.is_algebraic],
+  split,
+  { intros h x,
+    rw [is_fraction_ring.is_algebraic_iff R (fraction_ring R) K, is_algebraic_iff_is_integral],
+    obtain ⟨(a : S), b, ha, rfl⟩ := @div_surjective S _ _ _ _ _ _ x,
+    obtain ⟨f, hf₁, hf₂⟩ := h b,
+    rw [div_eq_mul_inv],
+    refine is_integral_mul _ _,
+    { rw [← is_algebraic_iff_is_integral],
+      refine _root_.is_algebraic_of_larger_base_of_injective
+        (no_zero_smul_divisors.algebra_map_injective R (fraction_ring R)) _,
+      exact is_algebraic_algebra_map_of_is_algebraic (h a) },
+    { rw [← is_algebraic_iff_is_integral],
+      use (f.map (algebra_map R (fraction_ring R))).reverse,
+      split,
+      { rwa [ne.def, polynomial.reverse_eq_zero, ← polynomial.degree_eq_bot,
+          polynomial.degree_map_eq_of_injective
+            (no_zero_smul_divisors.algebra_map_injective R (fraction_ring R)),
+          polynomial.degree_eq_bot]},
+      { haveI : invertible (algebra_map S K b),
+           from is_unit.invertible (is_unit_of_mem_non_zero_divisors
+              (mem_non_zero_divisors_iff_ne_zero.2
+                (λ h, non_zero_divisors.ne_zero ha
+                    ((ring_hom.injective_iff (algebra_map S K)).1
+                    (no_zero_smul_divisors.algebra_map_injective _ _) b h)))),
+        rw [polynomial.aeval_def, ← inv_of_eq_inv, polynomial.eval₂_reverse_eq_zero_iff,
+          polynomial.eval₂_map, ← is_scalar_tower.algebra_map_eq, ← polynomial.aeval_def,
+          ← is_scalar_tower.algebra_map_aeval, hf₂, ring_hom.map_zero] } } },
+  { intros h x,
+    obtain ⟨f, hf₁, hf₂⟩ := h (algebra_map S K x),
+    use [f, hf₁],
+    rw [← is_scalar_tower.algebra_map_aeval] at hf₂,
+    exact (algebra_map S K).injective_iff.1
+      (no_zero_smul_divisors.algebra_map_injective _ _) _ hf₂ }
+end
+
+end is_fraction_ring