feat(number_theory/number_field): add map_mem_ring_of_integers (#16754)

We add `number_field.map_mem_ring_of_integers`, the image of an element of the ring of integers under `f : K →ₐ[ℚ] L` lies in the ring of integer. In particular, the Galois group preserve the ring of integers.

From flt-regular

src/data/polynomial/algebra_map.lean

@@ -217,17 +217,16 @@ theorem eval_unique (φ : R[X] →ₐ[R] A) (p) :
   φ p = eval₂ (algebra_map R A) (φ X) p :=
 by rw [← aeval_def, aeval_alg_hom, aeval_X_left, alg_hom.comp_id]
 
-theorem aeval_alg_hom_apply (f : A →ₐ[R] B) (x : A) (p : R[X]) :
+theorem aeval_alg_hom_apply {F : Type*} [alg_hom_class F R A B] (f : F) (x : A) (p : R[X]) :
   aeval (f x) p = f (aeval x p) :=
-alg_hom.ext_iff.1 (aeval_alg_hom f x) p
+begin
+  refine polynomial.induction_on p (by simp) (λ p q hp hq, _) (by simp),
+  rw [map_add, hp, hq, ← map_add, ← map_add]
+end
 
 theorem aeval_alg_equiv (f : A ≃ₐ[R] B) (x : A) : aeval (f x) = (f : A →ₐ[R] B).comp (aeval x) :=
 aeval_alg_hom (f : A →ₐ[R] B) x
 
-theorem aeval_alg_equiv_apply (f : A ≃ₐ[R] B) (x : A) (p : R[X]) :
-  aeval (f x) p = f (aeval x p) :=
-aeval_alg_hom_apply (f : A →ₐ[R] B) x p
-
 lemma aeval_algebra_map_apply_eq_algebra_map_eval (x : R) (p : R[X]) :
   aeval (algebra_map R A x) p = algebra_map R A (p.eval x) :=
 aeval_alg_hom_apply (algebra.of_id R A) x p
@@ -237,7 +236,7 @@ aeval_alg_hom_apply (algebra.of_id R A) x p
 
 @[simp] lemma aeval_fn_apply {X : Type*} (g : R[X]) (f : X → R) (x : X) :
   ((aeval f) g) x = aeval (f x) g :=
-(aeval_alg_hom_apply (pi.eval_alg_hom _ _ x) f g).symm
+(aeval_alg_hom_apply (pi.eval_alg_hom R (λ _, R) x) f g).symm
 
 @[norm_cast] lemma aeval_subalgebra_coe
   (g : R[X]) {A : Type*} [semiring A] [algebra R A] (s : subalgebra R A) (f : s) :

src/field_theory/adjoin.lean

@@ -886,7 +886,7 @@ end⟩
 /-- Extend a lift `x : lifts F E K` to an element `s : E` whose conjugates are all in `K` -/
 noncomputable def lifts.lift_of_splits (x : lifts F E K) {s : E} (h1 : is_integral F s)
   (h2 : (minpoly F s).splits (algebra_map F K)) : lifts F E K :=
-let h3 : is_integral x.1 s := is_integral_of_is_scalar_tower s h1 in
+let h3 : is_integral x.1 s := is_integral_of_is_scalar_tower h1 in
 let key : (minpoly x.1 s).splits x.2.to_ring_hom :=
   splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero h1))
   ((splits_map_iff _ _).mpr (by {convert h2, exact ring_hom.ext (λ y, x.2.commutes y)}))

src/field_theory/galois.lean

@@ -339,7 +339,7 @@ lemma of_separable_splitting_field_aux
   fintype.card (K⟮x⟯.restrict_scalars F →ₐ[F] E) =
     fintype.card (K →ₐ[F] E) * finrank K K⟮x⟯ :=
 begin
-  have h : is_integral K x := is_integral_of_is_scalar_tower x
+  have h : is_integral K x := is_integral_of_is_scalar_tower
     (is_integral_of_noetherian (is_noetherian.iff_fg.2 hFE) x),
   have h1 : p ≠ 0 := λ hp, by rwa [hp, polynomial.map_zero, polynomial.roots_zero] at hx,
   have h2 : (minpoly K x) ∣ p.map (algebra_map F K),

src/field_theory/is_alg_closed/algebraic_closure.lean

@@ -257,7 +257,7 @@ def of_step_hom (n) : step k n →ₐ[k] algebraic_closure k :=
 
 theorem is_algebraic : algebra.is_algebraic k (algebraic_closure k) :=
 λ z, is_algebraic_iff_is_integral.2 $ let ⟨n, x, hx⟩ := exists_of_step k z in
-hx ▸ is_integral_alg_hom (of_step_hom k n) (step.is_integral k n x)
+hx ▸ map_is_integral (of_step_hom k n) (step.is_integral k n x)
 
 instance : is_alg_closure k (algebraic_closure k) :=
 ⟨algebraic_closure.is_alg_closed k, is_algebraic k⟩

src/field_theory/minpoly.lean

@@ -454,7 +454,7 @@ begin
   let L := fraction_ring S,
   rw [← gcd_domain_eq_field_fractions K L hs],
   refine minpoly.eq_of_algebra_map_eq (is_fraction_ring.injective S L)
-    (is_integral_of_is_scalar_tower _ hs) rfl
+    (is_integral_of_is_scalar_tower hs) rfl
 end
 
 variable [no_zero_smul_divisors R S]

src/field_theory/normal.lean

@@ -86,7 +86,7 @@ lemma normal.tower_top_of_normal [h : normal F E] : normal K E :=
 normal_iff.2 $ λ x, begin
   cases h.out x with hx hhx,
   rw algebra_map_eq F K E at hhx,
-  exact ⟨is_integral_of_is_scalar_tower x hx, polynomial.splits_of_splits_of_dvd (algebra_map K E)
+  exact ⟨is_integral_of_is_scalar_tower hx, polynomial.splits_of_splits_of_dvd (algebra_map K E)
     (polynomial.map_ne_zero (minpoly.ne_zero hx))
     ((polynomial.splits_map_iff (algebra_map F K) (algebra_map K E)).mpr hhx)
     (minpoly.dvd_map_of_is_scalar_tower F K x)⟩,
@@ -97,7 +97,7 @@ lemma alg_hom.normal_bijective [h : normal F E] (ϕ : E →ₐ[F] K) : function.
 { letI : algebra E K := ϕ.to_ring_hom.to_algebra,
   obtain ⟨h1, h2⟩ := h.out (algebra_map K E x),
   cases minpoly.mem_range_of_degree_eq_one E x (h2.def.resolve_left (minpoly.ne_zero h1)
-    (minpoly.irreducible (is_integral_of_is_scalar_tower x
+    (minpoly.irreducible (is_integral_of_is_scalar_tower
       ((is_integral_algebra_map_iff (algebra_map K E).injective).mp h1)))
     (minpoly.dvd E x ((algebra_map K E).injective (by
     { rw [ring_hom.map_zero, aeval_map_algebra_map, ← aeval_algebra_map_apply],
@@ -109,7 +109,7 @@ variables {F} {E} {E' : Type*} [field E'] [algebra F E']
 lemma normal.of_alg_equiv [h : normal F E] (f : E ≃ₐ[F] E') : normal F E' :=
 normal_iff.2 $ λ x, begin
   cases h.out (f.symm x) with hx hhx,
-  have H := is_integral_alg_hom f.to_alg_hom hx,
+  have H := map_is_integral f.to_alg_hom hx,
   rw [alg_equiv.to_alg_hom_eq_coe, alg_equiv.coe_alg_hom, alg_equiv.apply_symm_apply] at H,
   use H,
   apply polynomial.splits_of_splits_of_dvd (algebra_map F E') (minpoly.ne_zero hx),
@@ -245,11 +245,12 @@ def alg_hom.restrict_normal_aux [h : normal F E] :
     rintros x ⟨y, ⟨z, hy⟩, hx⟩,
     rw [←hx, ←hy],
     apply minpoly.mem_range_of_degree_eq_one E,
-    exact or.resolve_left (h.splits z).def (minpoly.ne_zero (h.is_integral z))
-      (minpoly.irreducible $ is_integral_of_is_scalar_tower _ $
-        is_integral_alg_hom ϕ $ is_integral_alg_hom _ $ h.is_integral z)
-      (minpoly.dvd E _ $ by rw [aeval_map_algebra_map, aeval_alg_hom_apply, aeval_alg_hom_apply,
-        minpoly.aeval, alg_hom.map_zero, alg_hom.map_zero]) }⟩,
+    refine or.resolve_left (h.splits z).def (minpoly.ne_zero (h.is_integral z))
+      (minpoly.irreducible _) (minpoly.dvd E _ (by simp [aeval_alg_hom_apply])),
+    simp only [alg_hom.to_ring_hom_eq_coe, alg_hom.coe_to_ring_hom],
+    suffices : is_integral F _,
+    { exact is_integral_of_is_scalar_tower this },
+    exact map_is_integral ϕ (map_is_integral (to_alg_hom F E K₁) (h.is_integral z)) }⟩,
   map_zero' := subtype.ext ϕ.map_zero,
   map_one' := subtype.ext ϕ.map_one,
   map_add' := λ x y, subtype.ext (ϕ.map_add x y),
@@ -330,7 +331,7 @@ noncomputable def alg_hom.lift_normal [h : normal F E] : E →ₐ[F] E :=
   @intermediate_field.alg_hom_mk_adjoin_splits' _ _ _ _ _ _ _
   ((is_scalar_tower.to_alg_hom F K₂ E).comp ϕ).to_ring_hom.to_algebra _
   (intermediate_field.adjoin_univ _ _)
-  (λ x hx, ⟨is_integral_of_is_scalar_tower x (h.out x).1,
+  (λ x hx, ⟨is_integral_of_is_scalar_tower (h.out x).1,
     splits_of_splits_of_dvd _ (map_ne_zero (minpoly.ne_zero (h.out x).1))
     (by { rw [splits_map_iff, ←is_scalar_tower.algebra_map_eq], exact (h.out x).2 })
     (minpoly.dvd_map_of_is_scalar_tower F K₁ x)⟩)

src/field_theory/separable.lean

@@ -486,7 +486,7 @@ variables (F K E : Type*) [field F] [field K] [field E] [algebra F K] [algebra F
   [algebra K E] [is_scalar_tower F K E]
 
 lemma is_separable_tower_top_of_is_separable [is_separable F E] : is_separable K E :=
-⟨λ x, is_integral_of_is_scalar_tower x (is_separable.is_integral F x),
+⟨λ x, is_integral_of_is_scalar_tower (is_separable.is_integral F x),
  λ x, (is_separable.separable F x).map.of_dvd (minpoly.dvd_map_of_is_scalar_tower _ _ _)⟩
 
 lemma is_separable_tower_bot_of_is_separable [h : is_separable F E] : is_separable F K :=

src/field_theory/splitting_field.lean

@@ -467,7 +467,7 @@ begin
     (submodule.fg_iff_finite_dimensional _).1
       (fg_adjoin_of_finite s.finite_to_set H3)).of_subalgebra_to_submodule,
   letI := field_of_finite_dimensional F (algebra.adjoin F (↑s : set K)),
-  have H5 : is_integral (algebra.adjoin F (↑s : set K)) a := is_integral_of_is_scalar_tower a H1,
+  have H5 : is_integral (algebra.adjoin F (↑s : set K)) a := is_integral_of_is_scalar_tower H1,
   have H6 : (minpoly (algebra.adjoin F (↑s : set K)) a).splits
     (algebra_map (algebra.adjoin F (↑s : set K)) L),
   { refine polynomial.splits_of_splits_of_dvd _

src/linear_algebra/charpoly/basic.lean

@@ -61,7 +61,7 @@ to the linear map itself, is zero.
 See `matrix.aeval_self_charpoly` for the equivalent statement about matrices. -/
 lemma aeval_self_charpoly : aeval f f.charpoly = 0 :=
 begin
-  apply (linear_equiv.map_eq_zero_iff (alg_equiv_matrix _).to_linear_equiv).1,
+  apply (linear_equiv.map_eq_zero_iff (alg_equiv_matrix (choose_basis R M)).to_linear_equiv).1,
   rw [alg_equiv.to_linear_equiv_apply, ← alg_equiv.coe_alg_hom,
     ← polynomial.aeval_alg_hom_apply _ _ _, charpoly_def],
   exact aeval_self_charpoly _,

src/number_theory/number_field/basic.lean

@@ -102,6 +102,10 @@ integral_closure.is_integrally_closed_of_finite_extension ℚ
 lemma is_integral_coe (x : 𝓞 K) : is_integral ℤ (x : K) :=
 x.2
 
+lemma map_mem_ring_of_integers {F L : Type*} [field L] [char_zero K] [char_zero L]
+  [alg_hom_class F ℚ K L] (f : F) (x : 𝓞 K) : f x ∈ 𝓞 L :=
+(mem_ring_of_integers _ _).2 $ map_is_integral_int f $ ring_of_integers.is_integral_coe x
+
 /-- The ring of integers of `K` are equivalent to any integral closure of `ℤ` in `K` -/
 protected noncomputable def equiv (R : Type*) [comm_ring R] [algebra R K]
   [is_integral_closure R ℤ K] : 𝓞 K ≃+* R :=

src/number_theory/number_field/embeddings.lean

@@ -95,7 +95,7 @@ begin
   have h_map_ℚ_minpoly := minpoly.gcd_domain_eq_field_fractions' ℚ hx.1,
   refine ⟨_, ⟨_, λ i, _⟩, (mem_root_set_iff (minpoly.ne_zero hx.1) x).2 (minpoly.aeval ℤ x)⟩,
   { rw [← (minpoly.monic hx.1).nat_degree_map (algebra_map ℤ ℚ), ← h_map_ℚ_minpoly],
-    exact minpoly.nat_degree_le (is_integral_of_is_scalar_tower x hx.1), },
+    exact minpoly.nat_degree_le (is_integral_of_is_scalar_tower hx.1) },
   rw [mem_Icc, ← abs_le, ← @int.cast_le ℝ],
   refine (eq.trans_le _ $ coeff_bdd_of_norm_le hx.2 i).trans (nat.le_ceil _),
   rw [h_map_ℚ_minpoly, coeff_map, eq_int_cast, int.norm_cast_rat, int.norm_eq_abs, int.cast_abs],

src/ring_theory/integral_closure.lean

@@ -114,15 +114,20 @@ variables {R A B S : Type*}
 variables [comm_ring R] [comm_ring A] [comm_ring B] [comm_ring S]
 variables [algebra R A] [algebra R B] (f : R →+* S)
 
-theorem is_integral_alg_hom {A B : Type*} [ring A] [ring B] [algebra R A] [algebra R B]
-  (f : A →ₐ[R] B) {x : A} (hx : is_integral R x) : is_integral R (f x) :=
-let ⟨p, hp, hpx⟩ :=
-hx in ⟨p, hp, by rw [← aeval_def, aeval_alg_hom_apply, aeval_def, hpx, f.map_zero]⟩
+lemma map_is_integral {B C F : Type*} [ring B] [ring C] [algebra R B] [algebra A B]
+  [algebra R C] [is_scalar_tower R A B] [algebra A C] [is_scalar_tower R A C] {b : B}
+  [alg_hom_class F A B C] (f : F) (hb : is_integral R b) : is_integral R (f b) :=
+begin
+  obtain ⟨P, hP⟩ := hb,
+  refine ⟨P, hP.1, _⟩,
+  rw [← aeval_def, show (aeval (f b)) P = (aeval (f b)) (P.map (algebra_map R A)), by simp,
+    aeval_alg_hom_apply, aeval_map_algebra_map, aeval_def, hP.2, _root_.map_zero]
+end
 
 theorem is_integral_alg_hom_iff {A B : Type*} [ring A] [ring B] [algebra R A] [algebra R B]
   (f : A →ₐ[R] B) (hf : function.injective f) {x : A} : is_integral R (f x) ↔ is_integral R x :=
 begin
-  refine ⟨_, is_integral_alg_hom f⟩,
+  refine ⟨_, map_is_integral f⟩,
   rintros ⟨p, hp, hx⟩,
   use [p, hp],
   rwa [← f.comp_algebra_map, ← alg_hom.coe_to_ring_hom, ← polynomial.hom_eval₂,
@@ -132,17 +137,22 @@ end
 @[simp]
 theorem is_integral_alg_equiv {A B : Type*} [ring A] [ring B] [algebra R A] [algebra R B]
   (f : A ≃ₐ[R] B) {x : A} : is_integral R (f x) ↔ is_integral R x :=
-⟨λ h, by simpa using is_integral_alg_hom f.symm.to_alg_hom h, is_integral_alg_hom f.to_alg_hom⟩
+⟨λ h, by simpa using map_is_integral f.symm.to_alg_hom h, map_is_integral f.to_alg_hom⟩
 
 theorem is_integral_of_is_scalar_tower [algebra A B] [is_scalar_tower R A B]
-  (x : B) (hx : is_integral R x) : is_integral A x :=
+  {x : B} (hx : is_integral R x) : is_integral A x :=
 let ⟨p, hp, hpx⟩ := hx in
 ⟨p.map $ algebra_map R A, hp.map _,
   by rw [← aeval_def, aeval_map_algebra_map, aeval_def, hpx]⟩
 
+lemma map_is_integral_int {B C F : Type*} [ring B] [ring C] {b : B}
+  [ring_hom_class F B C] (f : F) (hb : is_integral ℤ b) :
+  is_integral ℤ (f b) :=
+map_is_integral (f : B →+* C).to_int_alg_hom hb
+
 theorem is_integral_of_subring {x : A} (T : subring R)
   (hx : is_integral T x) : is_integral R x :=
-is_integral_of_is_scalar_tower x hx
+is_integral_of_is_scalar_tower hx
 
 lemma is_integral.algebra_map [algebra A B] [is_scalar_tower R A B]
   {x : A} (h : is_integral R x) :
@@ -503,9 +513,9 @@ begin
   rw subalgebra.mem_map,
   split,
   { rintros ⟨x, hx, rfl⟩,
-    exact is_integral_alg_hom f hx },
+    exact map_is_integral f hx },
   { intro hy,
-    use [f.symm y, is_integral_alg_hom (f.symm : B →ₐ[R] A) hy],
+    use [f.symm y, map_is_integral (f.symm : B →ₐ[R] A) hy],
     simp }
 end
 
@@ -852,7 +862,7 @@ begin
   { rw [finset.mem_coe, frange, finset.mem_image] at hx,
     rcases hx with ⟨i, _, rfl⟩,
     rw coeff_map,
-    exact is_integral_alg_hom (is_scalar_tower.to_alg_hom R A B) (A_int _) },
+    exact map_is_integral (is_scalar_tower.to_alg_hom R A B) (A_int _) },
   { apply fg_adjoin_singleton_of_integral,
     exact is_integral_trans_aux _ pmonic hp }
 end

src/ring_theory/norm.lean

@@ -305,7 +305,7 @@ lemma is_integral_norm [algebra S L] [algebra S K] [is_scalar_tower S K L]
   [is_separable K L] [finite_dimensional K L] {x : L} (hx : _root_.is_integral S x) :
   _root_.is_integral S (norm K x) :=
 begin
-  have hx' : _root_.is_integral K x := is_integral_of_is_scalar_tower _ hx,
+  have hx' : _root_.is_integral K x := is_integral_of_is_scalar_tower hx,
   rw [← is_integral_algebra_map_iff (algebra_map K (algebraic_closure L)).injective,
       norm_eq_prod_roots],
   { refine (is_integral.multiset_prod (λ y hy, _)).pow _,

src/ring_theory/trace.lean

@@ -286,7 +286,7 @@ open polynomial
 lemma algebra.is_integral_trace [finite_dimensional L F] {x : F} (hx : _root_.is_integral R x) :
   _root_.is_integral R (algebra.trace L F x) :=
 begin
-  have hx' : _root_.is_integral L x := is_integral_of_is_scalar_tower _ hx,
+  have hx' : _root_.is_integral L x := is_integral_of_is_scalar_tower hx,
   rw [← is_integral_algebra_map_iff (algebra_map L (algebraic_closure F)).injective,
       trace_eq_sum_roots],
   { refine (is_integral.multiset_sum _).nsmul _,