[Merged by Bors] - chore(number_theory/number_field/embeddings): golf

src/data/polynomial/ring_division.lean

@@ -671,25 +671,15 @@ lemma bUnion_roots_finite {R S : Type*} [semiring R] [comm_ring S] [is_domain S]
   (m : R →+* S) (d : ℕ) {U : set R} (h : U.finite) :
   (⋃ (f : R[X]) (hf : f.nat_degree ≤ d ∧ ∀ i, (f.coeff i) ∈ U),
     ((f.map m).roots.to_finset : set S)).finite :=
-begin
-  refine set.finite.bUnion _ _,
-  { -- We prove that the set of polynomials under consideration is finite because its
-    -- image by the injective map `π` is finite
-    let π : R[X] → finset.range (d+1) → R := λ f i, f.coeff i,
-    have h_inj : set.inj_on π {f : R[X] | f.nat_degree ≤ d ∧ ∀ (i : ℕ), f.coeff i ∈ U},
-    { intros x hx y hy hxy,
-      rw ext_iff_nat_degree_le hx.1 hy.1,
-      exact_mod_cast λ i hi, congr_fun hxy ⟨i, finset.mem_range_succ_iff.mpr hi⟩, },
-    have h_fin : (set.pi set.univ (λ e : finset.range (d+1), U)).finite := set.finite.pi (λ e, h),
-    refine set.finite.of_finite_image (set.finite.subset h_fin _) h_inj,
-    rw set.image_subset_iff,
-    intros f hf,
-    rw [set.mem_preimage, set.mem_univ_pi],
-    exact λ i, hf.2 i, },
-  { intros i hi,
-    convert root_set_finite (i.map m) S,
-    simp only [algebra.id.map_eq_id, map_id], },
-end
+set.finite.bUnion begin
+  -- We prove that the set of polynomials under consideration is finite because its
+  -- image by the injective map `π` is finite
+  let π : R[X] → fin (d+1) → R := λ f i, f.coeff i,
+  refine ((set.finite.pi $ λ e, h).subset $ _).of_finite_image (_ : set.inj_on π _),
+  { exact set.image_subset_iff.2 (λ f hf i _, hf.2 i) },
+  { refine λ x hx y hy hxy, (ext_iff_nat_degree_le hx.1 hy.1).2 (λ i hi, _),
+    exact id congr_fun hxy ⟨i, nat.lt_succ_of_le hi⟩ },
+end $ λ i hi, finset.finite_to_set _
 
 theorem mem_root_set_iff' {p : T[X]} {S : Type*} [comm_ring S] [is_domain S]
   [algebra T S] (hp : p.map (algebra_map T S) ≠ 0) (a : S) :

src/field_theory/is_alg_closed/basic.lean

@@ -486,3 +486,26 @@ ring_hom.ext_iff.2 (equiv_of_equiv_symm_algebra_map L M hSR)
 end equiv_of_equiv
 
 end is_alg_closure
+
+/-- Let `A` be an algebraically closed field and let `x ∈ K`, with `K/F` an algebraic extension
+  of fields. Then the images of `x` by the `F`-algebra morphisms from `K` to `A` are exactly
+  the roots in `A` of the minimal polynomial of `x` over `F`. -/
+lemma algebra.is_algebraic.range_eval_eq_root_set_minpoly {F K} (A) [field F] [field K] [field A]
+  [is_alg_closed A] [algebra F K] (hK : algebra.is_algebraic F K) [algebra F A] (x : K) :
+  set.range (λ ψ : K →ₐ[F] A, ψ x) = (minpoly F x).root_set A :=
+begin
+  have := algebra.is_algebraic_iff_is_integral.1 hK,
+  ext a, rw mem_root_set_iff (minpoly.ne_zero $ this x) a,
+  refine ⟨_, λ ha, _⟩,
+  { rintro ⟨ψ, rfl⟩, rw [aeval_alg_hom_apply ψ x, minpoly.aeval, map_zero] },
+  let Fx := adjoin_root (minpoly F x),
+  have hx : aeval x (minpoly F x) = 0 := minpoly.aeval F x,
+  letI : algebra Fx A := (adjoin_root.lift (algebra_map F A) a ha).to_algebra,
+  letI : algebra Fx K := (adjoin_root.lift (algebra_map F K) x hx).to_algebra,
+  haveI : is_scalar_tower F Fx A := is_scalar_tower.of_ring_hom (adjoin_root.lift_hom _ a ha),
+  haveI : is_scalar_tower F Fx K := is_scalar_tower.of_ring_hom (adjoin_root.lift_hom _ x hx),
+  haveI : fact (irreducible $ minpoly F x) := ⟨minpoly.irreducible $ this x⟩,
+  let ψ₀ : K →ₐ[Fx] A := is_alg_closed.lift (algebra.is_algebraic_of_larger_base F Fx hK),
+  exact ⟨ψ₀.restrict_scalars F, (congr_arg ψ₀ (adjoin_root.lift_root hx).symm).trans $
+    (ψ₀.commutes _).trans $ adjoin_root.lift_root ha⟩,
+end

src/number_theory/number_field/embeddings.lean

@@ -48,51 +48,15 @@ section roots
 
 open set polynomial
 
-/-- Let `A` an algebraically closed field and let `x ∈ K`, with `K` a number field. For `F`,
-subfield of `K`, the images of `x` by the `F`-algebra morphisms from `K` to `A` are exactly
-the roots in `A` of the minimal polynomial of `x` over `F`. -/
-lemma range_eq_roots (F K A : Type*) [field F] [number_field F] [field K] [number_field K]
-  [field A] [is_alg_closed A] [algebra F K] [algebra F A] (x : K) :
-  range (λ ψ : K →ₐ[F] A, ψ x) = (minpoly F x).root_set A :=
-begin
-  haveI : finite_dimensional F K := finite_dimensional.right ℚ  _ _ ,
-  have hx : is_integral F x := is_separable.is_integral F x,
-  ext a, split,
-  { rintro ⟨ψ, hψ⟩,
-    rw [mem_root_set_iff, ←hψ],
-    { rw aeval_alg_hom_apply ψ x (minpoly F x),
-      simp only [minpoly.aeval, map_zero], },
-    exact minpoly.ne_zero hx, },
-  { intro ha,
-    let Fx := adjoin_root (minpoly F x),
-    haveI : fact (irreducible $ minpoly F x) := ⟨minpoly.irreducible hx⟩,
-    have hK : (aeval x) (minpoly F x) = 0 := minpoly.aeval _ _,
-    have hA : (aeval a) (minpoly F x) = 0,
-    { rwa [aeval_def, ←eval_map, ←mem_root_set_iff'],
-      exact monic.ne_zero (monic.map (algebra_map F A) (minpoly.monic hx)), },
-    letI : algebra Fx A := ring_hom.to_algebra (by convert adjoin_root.lift (algebra_map F A) a hA),
-    letI : algebra Fx K := ring_hom.to_algebra (by convert adjoin_root.lift (algebra_map F K) x hK),
-    haveI : finite_dimensional Fx K := finite_dimensional.right ℚ  _ _ ,
-    let ψ₀ : K →ₐ[Fx] A := is_alg_closed.lift (algebra.is_algebraic_of_finite _ _),
-    haveI : is_scalar_tower F Fx K := is_scalar_tower.of_ring_hom (adjoin_root.lift_hom _ _ hK),
-    haveI : is_scalar_tower F Fx A := is_scalar_tower.of_ring_hom (adjoin_root.lift_hom _ _ hA),
-    let ψ : K →ₐ[F] A := alg_hom.restrict_scalars F ψ₀,
-    refine ⟨ψ, _⟩,
-    rw (_ : x = (algebra_map Fx K) (adjoin_root.root (minpoly F x))),
-    rw (_ : a = (algebra_map Fx A) (adjoin_root.root (minpoly F x))),
-    exact alg_hom.commutes _ _,
-    exact (adjoin_root.lift_root hA).symm,
-    exact (adjoin_root.lift_root hK).symm, },
-end
-
-variables (K A : Type*) [field K] [number_field K] [field A] [char_zero A] [is_alg_closed A] (x : K)
+variables (K A : Type*) [field K] [number_field K]
+  [field A] [algebra ℚ A] [is_alg_closed A] (x : K)
 
 /-- Let `A` be an algebraically closed field and let `x ∈ K`, with `K` a number field.
 The images of `x` by the embeddings of `K` in `A` are exactly the roots in `A` of
 the minimal polynomial of `x` over `ℚ`. -/
-lemma rat_range_eq_roots : range (λ φ : K →+* A, φ x) = (minpoly ℚ x).root_set A :=
+lemma range_eval_eq_root_set_minpoly : range (λ φ : K →+* A, φ x) = (minpoly ℚ x).root_set A :=
 begin
-  convert range_eq_roots ℚ K A x using 1,
+  convert (number_field.is_algebraic K).range_eval_eq_root_set_minpoly A x using 1,
   ext a,
   exact ⟨λ ⟨φ, hφ⟩, ⟨φ.to_rat_alg_hom, hφ⟩, λ ⟨φ, hφ⟩, ⟨φ.to_ring_hom, hφ⟩⟩,
 end
@@ -106,20 +70,16 @@ open finite_dimensional polynomial set
 variables {K : Type*} [field K] [number_field K]
 variables {A : Type*} [normed_field A] [is_alg_closed A] [normed_algebra ℚ A]
 
-lemma coeff_bdd_of_norm_le {B : ℝ} {x : K} (h : ∀ φ : K →+* A, ∥φ x∥ ≤ B) (i : ℕ):
+lemma coeff_bdd_of_norm_le {B : ℝ} {x : K} (h : ∀ φ : K →+* A, ∥φ x∥ ≤ B) (i : ℕ) :
   ∥(minpoly ℚ x).coeff i∥ ≤ (max B 1) ^ (finrank ℚ K) * (finrank ℚ K).choose ((finrank ℚ K) / 2) :=
 begin
-  have hx : is_integral ℚ x := is_separable.is_integral _ _,
-  rw (by rw [coeff_map, norm_algebra_map'] :
-    ∥(minpoly ℚ x).coeff i∥ = ∥(map (algebra_map ℚ A) (minpoly ℚ x)).coeff i∥),
+  have hx := is_separable.is_integral ℚ x,
+  rw [← norm_algebra_map' A, ← coeff_map (algebra_map ℚ A)],
   refine coeff_bdd_of_roots_le _ (minpoly.monic hx) (is_alg_closed.splits_codomain _)
-    (minpoly.nat_degree_le hx) _ i,
-  intros z hz,
-  rsuffices ⟨φ, rfl⟩ : ∃ (φ : K →+* A), φ x = z, {exact h φ },
-  letI : char_zero A := char_zero_of_injective_algebra_map (algebra_map ℚ _).injective,
-  rw [← set.mem_range, rat_range_eq_roots, mem_root_set_iff, aeval_def],
-  convert (mem_roots_map _).mp hz,
-  repeat { exact monic.ne_zero (minpoly.monic hx), },
+    (minpoly.nat_degree_le hx) (λ z hz, _) i,
+  classical, rw ← multiset.mem_to_finset at hz,
+  obtain ⟨φ, rfl⟩ := (range_eval_eq_root_set_minpoly K A x).symm.subset hz,
+  exact h φ,
 end
 
 variables (K A)
@@ -131,42 +91,33 @@ lemma finite_of_norm_le (B : ℝ) :
 begin
   let C := nat.ceil ((max B 1) ^ (finrank ℚ K) * (finrank ℚ K).choose ((finrank ℚ K) / 2)),
   have := bUnion_roots_finite (algebra_map ℤ K) (finrank ℚ K) (finite_Icc (-C : ℤ) C),
-  refine this.subset (λ x hx, _),
-  have h_map_rat_minpoly := minpoly.gcd_domain_eq_field_fractions' ℚ hx.1,
-  rw mem_Union,
-  use minpoly ℤ x,
-  rw [mem_Union, exists_prop],
-  refine ⟨⟨_, λ i, _⟩, _⟩,
-  { rw [← nat_degree_map_eq_of_injective (algebra_map ℤ ℚ).injective_int _, ← h_map_rat_minpoly],
-    exact minpoly.nat_degree_le (is_integral_of_is_scalar_tower _ hx.1), },
-  { rw [mem_Icc, ← abs_le, ← @int.cast_le ℝ],
-    apply le_trans _ (nat.le_ceil _),
-    convert coeff_bdd_of_norm_le hx.2 i,
-    simp only [h_map_rat_minpoly, coeff_map, eq_int_cast, int.norm_cast_rat, int.norm_eq_abs,
-      int.cast_abs], },
-  { rw [finset.mem_coe, multiset.mem_to_finset, mem_roots, is_root.def, ← eval₂_eq_eval_map,
-      ← aeval_def],
-    { exact minpoly.aeval ℤ x, },
-    { exact monic.ne_zero (monic.map (algebra_map ℤ K) (minpoly.monic hx.1)), }},
+  refine this.subset (λ x hx, _), simp_rw mem_Union,
+  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), },
+  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],
 end
 
 /-- An algebraic integer whose conjugates are all of norm one is a root of unity. -/
 lemma pow_eq_one_of_norm_eq_one {x : K}
-  (hxi : is_integral ℤ x)  (hx : ∀ φ : K →+* A, ∥φ x∥ = 1) :
+  (hxi : is_integral ℤ x) (hx : ∀ φ : K →+* A, ∥φ x∥ = 1) :
   ∃ (n : ℕ) (hn : 0 < n), x ^ n = 1 :=
 begin
   obtain ⟨a, -, b, -, habne, h⟩ := @set.infinite.exists_ne_map_eq_of_maps_to _ _ _ _
     ((^) x : ℕ → K) set.infinite_univ _ (finite_of_norm_le K A (1:ℝ)),
   { replace habne := habne.lt_or_lt,
-    wlog : a < b := habne using [a b],
-    refine ⟨b - a, tsub_pos_of_lt habne, _⟩,
-    have hxne : x ≠ 0,
-    { contrapose! hx,
-      simp only [hx, norm_zero, ring_hom.map_zero, ne.def, not_false_iff, zero_ne_one],
-      use (is_alg_closed.lift (number_field.is_algebraic K)).to_ring_hom, },
-    { rw [pow_sub₀ _ hxne habne.le, h, mul_inv_cancel (pow_ne_zero b hxne)], }},
-  { rw set.maps_univ_to,
-    exact λ a, ⟨hxi.pow a, λ φ, by simp [hx φ, norm_pow, one_pow]⟩, },
+    have : _, swap, cases habne, swap,
+    { revert a b, exact this },
+    { exact this b a h.symm habne },
+    refine λ a b h hlt, ⟨a - b, tsub_pos_of_lt hlt, _⟩,
+    rw [← nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h,
+    refine h.resolve_right (λ hp, _),
+    specialize hx (is_alg_closed.lift (number_field.is_algebraic K)).to_ring_hom,
+    rw [pow_eq_zero hp, map_zero, norm_zero] at hx, norm_num at hx },
+  { exact λ a _, ⟨hxi.pow a, λ φ, by simp only [hx φ, norm_pow, one_pow, map_pow]⟩ },
 end
 
 end bounded