feat(ring_theory/ring_hom/integral): Integral extensions are stable u…

…nder base change. (#15806)

src/ring_theory/integral_closure.lean

@@ -9,6 +9,7 @@ import linear_algebra.matrix.determinant
 import ring_theory.adjoin.fg
 import ring_theory.polynomial.scale_roots
 import ring_theory.polynomial.tower
+import ring_theory.tensor_product
 
 /-!
 # Integral closure of a subring.
@@ -525,6 +526,24 @@ end
   is_integral R (x ^ n) ↔ is_integral R x :=
 ⟨is_integral_of_pow hn, λ hx, is_integral.pow hx n⟩
 
+open_locale tensor_product
+
+lemma is_integral.tmul (x : A) {y : B} (h : is_integral R y) : is_integral A (x ⊗ₜ[R] y) :=
+begin
+  obtain ⟨p, hp, hp'⟩ := h,
+  refine ⟨(p.map (algebra_map R A)).scale_roots x, _, _⟩,
+  { rw polynomial.monic_scale_roots_iff, exact hp.map _ },
+  convert @polynomial.scale_roots_eval₂_mul (A ⊗[R] B) A _ _ _
+    algebra.tensor_product.include_left.to_ring_hom (1 ⊗ₜ y) x using 2,
+  { simp only [alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom, mul_one, one_mul,
+      algebra.tensor_product.include_left_apply, algebra.tensor_product.tmul_mul_tmul] },
+  convert (mul_zero _).symm,
+  rw [polynomial.eval₂_map, algebra.tensor_product.include_left_comp_algebra_map,
+    ← polynomial.eval₂_map],
+  convert polynomial.eval₂_at_apply algebra.tensor_product.include_right.to_ring_hom y,
+  rw [polynomial.eval_map, hp', _root_.map_zero],
+end
+
 section
 
 variables (p : R[X]) (x : S)

src/ring_theory/polynomial/scale_roots.lean

@@ -83,9 +83,9 @@ lemma monic_scale_roots_iff {p : R[X]} (s : R) :
   monic (scale_roots p s) ↔ monic p :=
 by simp only [monic, leading_coeff, nat_degree_scale_roots, coeff_scale_roots_nat_degree]
 
-lemma scale_roots_eval₂_eq_zero {p : S[X]} (f : S →+* R)
-  {r : R} {s : S} (hr : eval₂ f r p = 0) :
-  eval₂ f (f s * r) (scale_roots p s) = 0 :=
+lemma scale_roots_eval₂_mul {p : S[X]} (f : S →+* R)
+  (r : R) (s : S) :
+  eval₂ f (f s * r) (scale_roots p s) = f s ^ p.nat_degree * eval₂ f r p :=
 calc eval₂ f (f s * r) (scale_roots p s) =
   (scale_roots p s).support.sum (λ i, f (coeff p i * s ^ (p.nat_degree - i)) * (f s * r) ^ i) :
   by simp [eval₂_eq_sum, sum_def]
@@ -102,7 +102,11 @@ calc eval₂ f (f s * r) (scale_roots p s) =
                 exact le_nat_degree_of_ne_zero (polynomial.mem_support_iff.mp hi) })
 ... = f s ^ p.nat_degree * p.support.sum (λ (i : ℕ), (f (p.coeff i) * r ^ i)) : finset.mul_sum.symm
 ... = f s ^ p.nat_degree * eval₂ f r p : by { simp [eval₂_eq_sum, sum_def] }
-... = 0 : by rw [hr, _root_.mul_zero]
+
+lemma scale_roots_eval₂_eq_zero {p : S[X]} (f : S →+* R)
+  {r : R} {s : S} (hr : eval₂ f r p = 0) :
+  eval₂ f (f s * r) (scale_roots p s) = 0 :=
+by rw [scale_roots_eval₂_mul, hr, _root_.mul_zero]
 
 lemma scale_roots_aeval_eq_zero [algebra S R] {p : S[X]}
   {r : R} {s : S} (hr : aeval r p = 0) :
@@ -125,4 +129,11 @@ lemma scale_roots_aeval_eq_zero_of_aeval_div_eq_zero [algebra A K]
   aeval (algebra_map A K r) (scale_roots p s) = 0 :=
 scale_roots_eval₂_eq_zero_of_eval₂_div_eq_zero inj hr hs
 
+lemma map_scale_roots (p : R[X]) (x : R) (f : R →+* S) (h : f p.leading_coeff ≠ 0) :
+    (p.scale_roots x).map f = (p.map f).scale_roots (f x) :=
+begin
+  ext,
+  simp [polynomial.nat_degree_map_of_leading_coeff_ne_zero _ h],
+end
+
 end polynomial

src/ring_theory/ring_hom/integral.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2021 Andrew Yang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andrew Yang
+-/
+import ring_theory.local_properties
+import ring_theory.localization.integral
+
+/-!
+
+# The meta properties of integral ring homomorphisms.
+
+-/
+
+namespace ring_hom
+
+open_locale tensor_product
+
+open tensor_product algebra.tensor_product
+
+lemma is_integral_stable_under_composition :
+  stable_under_composition (λ R S _ _ f, by exactI f.is_integral) :=
+by { introv R hf hg, exactI ring_hom.is_integral_trans _ _ hf hg }
+
+lemma is_integral_respects_iso :
+  respects_iso (λ R S _ _ f, by exactI f.is_integral) :=
+begin
+  apply is_integral_stable_under_composition.respects_iso,
+  introv x,
+  resetI,
+  rw ← e.apply_symm_apply x,
+  apply ring_hom.is_integral_map
+end
+
+lemma is_integral_stable_under_base_change :
+  stable_under_base_change (λ R S _ _ f, by exactI f.is_integral) :=
+begin
+  introv R h x,
+  resetI,
+  apply tensor_product.induction_on x,
+  { apply is_integral_zero },
+  { intros x y, exact is_integral.tmul x (h y) },
+  { intros x y hx hy, exact is_integral_add _ hx hy }
+end
+
+end ring_hom

src/ring_theory/tensor_product.lean

@@ -445,6 +445,12 @@ def include_right : B →ₐ[R] A ⊗[R] B :=
 @[simp]
 lemma include_right_apply (b : B) : (include_right : B →ₐ[R] A ⊗[R] B) b = 1 ⊗ₜ b := rfl
 
+lemma include_left_comp_algebra_map {R S T : Type*} [comm_ring R] [comm_ring S] [comm_ring T]
+  [algebra R S] [algebra R T] :
+    (include_left.to_ring_hom.comp (algebra_map R S) : R →+* S ⊗[R] T) =
+      include_right.to_ring_hom.comp (algebra_map R T) :=
+by { ext, simp }
+
 end semiring
 
 section ring