From 66d422f37e9545a419797fd727f3ad90899b5a34 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 3 Oct 2022 21:17:28 -0400 Subject: [PATCH 1/6] golf `coeff_le_of_roots_le` --- src/topology/algebra/polynomial.lean | 73 ++++++++++------------------ 1 file changed, 25 insertions(+), 48 deletions(-) diff --git a/src/topology/algebra/polynomial.lean b/src/topology/algebra/polynomial.lean index bccc53ba4c7c8..4b194094af552 100644 --- a/src/topology/algebra/polynomial.lean +++ b/src/topology/algebra/polynomial.lean @@ -133,10 +133,9 @@ else ⟨p.coeff 0, by rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]; simp⟩ section roots -open_locale polynomial -open_locale nnreal +open_locale polynomial nnreal -variables {F K : Type*} [field F] [normed_field K] +variables {F K : Type*} [comm_ring F] [normed_field K] open multiset @@ -145,8 +144,8 @@ lemma eq_one_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (hB : B < 0) p = 1 := h1.nat_degree_eq_zero_iff_eq_one.mp begin contrapose !hB, - rw nat_degree_eq_card_roots h2 at hB, - obtain ⟨z, hz⟩ := multiset.card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB), + rw [← h1.nat_degree_map, nat_degree_eq_card_roots' h2] at hB, swap, apply_instance, + obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB), exact le_trans (norm_nonneg _) (h3 z hz), end @@ -154,49 +153,27 @@ lemma coeff_le_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (i : ℕ) (h1 : p.monic) (h2 : splits f p) (h3 : ∀ z ∈ (map f p).roots, ∥z∥ ≤ B) : ∥ (map f p).coeff i ∥ ≤ B^(p.nat_degree - i) * p.nat_degree.choose i := begin - have hcd : card (map f p).roots = p.nat_degree := (nat_degree_eq_card_roots h2).symm, - obtain hB | hB := le_or_lt 0 B, - { by_cases hi : i ≤ p.nat_degree, - { rw [eq_prod_roots_of_splits h2, monic.def.mp h1, ring_hom.map_one, ring_hom.map_one, one_mul], - rw prod_X_sub_C_coeff, - swap, rwa hcd, - rw [norm_mul, (by norm_num : ∥(-1 : K) ^ (card (map f p).roots - i)∥= 1), one_mul], - apply le_trans (le_sum_of_subadditive norm _ _ _ ), - rotate, exact norm_zero, exact norm_add_le, - rw multiset.map_map, - suffices : ∀ r ∈ multiset.map (norm_hom ∘ prod) - (powerset_len (card (map f p).roots - i) (map f p).roots), r ≤ B^(p.nat_degree - i), - { convert sum_le_sum_map _ this, - simp only [hi, hcd, multiset.map_const, card_map, card_powerset_len, nat.choose_symm, - sum_repeat, nsmul_eq_mul, mul_comm], }, - { intros r hr, - obtain ⟨t, ht⟩ := multiset.mem_map.mp hr, - have hbounds : ∀ x ∈ (multiset.map norm_hom t), 0 ≤ x ∧ x ≤ B, - { intros x hx, - obtain ⟨z, hz⟩ := multiset.mem_map.mp hx, - rw ←hz.right, - exact ⟨norm_nonneg z, - h3 z (mem_of_le (mem_powerset_len.mp ht.left).left hz.left)⟩, }, - lift B to ℝ≥0 using hB, - lift (multiset.map norm_hom t) to (multiset ℝ≥0) using (λ x hx, (hbounds x hx).left) - with normt hn, - rw (by rw_mod_cast [←ht.right, function.comp_apply, ←prod_hom t norm_hom, ←hn] : - r = normt.prod), - convert multiset.prod_le_pow_card normt _ _, - { rw (_ : card normt = card (multiset.map coe normt)), - rwa [hn, ←hcd, card_map, (mem_powerset_len.mp ht.left).right.symm], - rwa card_map, }, - { intros x hx, - have xmem : (x : ℝ) ∈ multiset.map coe normt := mem_map_of_mem _ hx, - exact (hbounds x xmem).right, }}}, - { push_neg at hi, - rw [nat.choose_eq_zero_of_lt hi, coeff_eq_zero_of_nat_degree_lt, norm_zero], - rw_mod_cast mul_zero, - { rwa monic.nat_degree_map h1, - apply_instance, }}}, - { rw [eq_one_of_roots_le hB h1 h2 h3, polynomial.map_one, nat_degree_one, zero_tsub, pow_zero, - one_mul, coeff_one], - split_ifs; norm_num [h], }, + obtain hB | hB := lt_or_le B 0, + { rw [eq_one_of_roots_le hB h1 h2 h3, polynomial.map_one, + nat_degree_one, zero_tsub, pow_zero, one_mul, coeff_one], + split_ifs; norm_num [h] }, + have : (map f p).nat_degree = p.nat_degree := h1.nat_degree_map _, + obtain hi | hi := le_or_lt i p.nat_degree, + { rw [coeff_eq_esymm_roots_of_splits ((splits_id_iff_splits f).2 h2) (this.substr hi), + (h1.map _).leading_coeff, one_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul], + apply ((norm_multiset_sum_le _).trans $ sum_le_card_nsmul _ _ $ λ r hr, _).trans, + { rw [multiset.map_map, card_map, card_powerset_len, this, + ←nat_degree_eq_card_roots' h2, this, nat.choose_symm hi, mul_comm, nsmul_eq_mul] }, + simp_rw multiset.mem_map at hr, + obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr, + rw [mem_powerset_len, this] at hs, + lift B to ℝ≥0 using hB, + rw [←coe_nnnorm, ←nnreal.coe_pow, nnreal.coe_le_coe, + ←nnnorm_hom_apply, ←monoid_hom.coe_coe, monoid_hom.map_multiset_prod], + refine (prod_le_pow_card _ B $ λ x hx, _).trans_eq (by rw [card_map, hs.2]), + obtain ⟨z, hz, rfl⟩ := multiset.mem_map.1 hx, + exact h3 z (mem_of_le hs.1 hz) }, + { rw [coeff_eq_zero_of_nat_degree_lt, norm_zero], { positivity }, { rwa this } }, end /-- The coefficients of the monic polynomials of bounded degree with bounded roots are From f5f4432553c3f628cfa4bf1395bc2a65832ccf5f Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 3 Oct 2022 21:32:26 -0400 Subject: [PATCH 2/6] simplification --- src/topology/algebra/polynomial.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/topology/algebra/polynomial.lean b/src/topology/algebra/polynomial.lean index 4b194094af552..977f47d68072d 100644 --- a/src/topology/algebra/polynomial.lean +++ b/src/topology/algebra/polynomial.lean @@ -144,7 +144,7 @@ lemma eq_one_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (hB : B < 0) p = 1 := h1.nat_degree_eq_zero_iff_eq_one.mp begin contrapose !hB, - rw [← h1.nat_degree_map, nat_degree_eq_card_roots' h2] at hB, swap, apply_instance, + rw [← h1.nat_degree_map f, nat_degree_eq_card_roots' h2] at hB, obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB), exact le_trans (norm_nonneg _) (h3 z hz), end @@ -157,7 +157,7 @@ begin { rw [eq_one_of_roots_le hB h1 h2 h3, polynomial.map_one, nat_degree_one, zero_tsub, pow_zero, one_mul, coeff_one], split_ifs; norm_num [h] }, - have : (map f p).nat_degree = p.nat_degree := h1.nat_degree_map _, + have : (map f p).nat_degree = p.nat_degree := h1.nat_degree_map f, obtain hi | hi := le_or_lt i p.nat_degree, { rw [coeff_eq_esymm_roots_of_splits ((splits_id_iff_splits f).2 h2) (this.substr hi), (h1.map _).leading_coeff, one_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul], From 2e666f54a554b775c28f545fbdef361fd26efb93 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Mon, 3 Oct 2022 21:41:49 -0400 Subject: [PATCH 3/6] a bit more golf --- src/topology/algebra/polynomial.lean | 34 ++++++++++++++-------------- 1 file changed, 17 insertions(+), 17 deletions(-) diff --git a/src/topology/algebra/polynomial.lean b/src/topology/algebra/polynomial.lean index 977f47d68072d..f6683a87c15d5 100644 --- a/src/topology/algebra/polynomial.lean +++ b/src/topology/algebra/polynomial.lean @@ -157,23 +157,23 @@ begin { rw [eq_one_of_roots_le hB h1 h2 h3, polynomial.map_one, nat_degree_one, zero_tsub, pow_zero, one_mul, coeff_one], split_ifs; norm_num [h] }, - have : (map f p).nat_degree = p.nat_degree := h1.nat_degree_map f, - obtain hi | hi := le_or_lt i p.nat_degree, - { rw [coeff_eq_esymm_roots_of_splits ((splits_id_iff_splits f).2 h2) (this.substr hi), - (h1.map _).leading_coeff, one_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul], - apply ((norm_multiset_sum_le _).trans $ sum_le_card_nsmul _ _ $ λ r hr, _).trans, - { rw [multiset.map_map, card_map, card_powerset_len, this, - ←nat_degree_eq_card_roots' h2, this, nat.choose_symm hi, mul_comm, nsmul_eq_mul] }, - simp_rw multiset.mem_map at hr, - obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr, - rw [mem_powerset_len, this] at hs, - lift B to ℝ≥0 using hB, - rw [←coe_nnnorm, ←nnreal.coe_pow, nnreal.coe_le_coe, - ←nnnorm_hom_apply, ←monoid_hom.coe_coe, monoid_hom.map_multiset_prod], - refine (prod_le_pow_card _ B $ λ x hx, _).trans_eq (by rw [card_map, hs.2]), - obtain ⟨z, hz, rfl⟩ := multiset.mem_map.1 hx, - exact h3 z (mem_of_le hs.1 hz) }, - { rw [coeff_eq_zero_of_nat_degree_lt, norm_zero], { positivity }, { rwa this } }, + rw ← h1.nat_degree_map f, + obtain hi | hi := lt_or_le (map f p).nat_degree i, + { rw [coeff_eq_zero_of_nat_degree_lt hi, norm_zero], positivity }, + rw [coeff_eq_esymm_roots_of_splits ((splits_id_iff_splits f).2 h2) hi, + (h1.map _).leading_coeff, one_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul], + apply ((norm_multiset_sum_le _).trans $ sum_le_card_nsmul _ _ $ λ r hr, _).trans, + { rw [multiset.map_map, card_map, card_powerset_len, + ←nat_degree_eq_card_roots' h2, nat.choose_symm hi, mul_comm, nsmul_eq_mul] }, + simp_rw multiset.mem_map at hr, + obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr, + rw mem_powerset_len at hs, + lift B to ℝ≥0 using hB, + rw [←coe_nnnorm, ←nnreal.coe_pow, nnreal.coe_le_coe, + ←nnnorm_hom_apply, ←monoid_hom.coe_coe, monoid_hom.map_multiset_prod], + refine (prod_le_pow_card _ B $ λ x hx, _).trans_eq (by rw [card_map, hs.2]), + obtain ⟨z, hz, rfl⟩ := multiset.mem_map.1 hx, + exact h3 z (mem_of_le hs.1 hz), end /-- The coefficients of the monic polynomials of bounded degree with bounded roots are From e61cf7f7969f4a27684a752f55361f081cb79241 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 4 Oct 2022 02:13:00 -0400 Subject: [PATCH 4/6] golf embeddings --- .../number_field/embeddings.lean | 104 +++++++----------- 1 file changed, 40 insertions(+), 64 deletions(-) diff --git a/src/number_theory/number_field/embeddings.lean b/src/number_theory/number_field/embeddings.lean index 543b924f44482..a968e59358f1c 100644 --- a/src/number_theory/number_field/embeddings.lean +++ b/src/number_theory/number_field/embeddings.lean @@ -51,38 +51,25 @@ 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) : +-- ! should be moved to another namespace +lemma range_eq_roots (F K A : Type*) [field F] [field K] [field A] [is_alg_closed A] + [algebra F K] (hK : algebra.is_algebraic 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, }, + 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), + haveI : fact (irreducible $ minpoly F x) := ⟨minpoly.irreducible $ this 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 _ _ ha), + haveI : is_scalar_tower F Fx K := is_scalar_tower.of_ring_hom (adjoin_root.lift_hom _ _ hx), + 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 variables (K A : Type*) [field K] [number_field K] [field A] [char_zero A] [is_alg_closed A] (x : K) @@ -92,7 +79,7 @@ The images of `x` by the embeddings of `K` in `A` are exactly the roots in `A` o the minimal polynomial of `x` over `ℚ`. -/ lemma rat_range_eq_roots : range (λ φ : K →+* A, φ x) = (minpoly ℚ x).root_set A := begin - convert range_eq_roots ℚ K A x using 1, + convert range_eq_roots ℚ K A (number_field.is_algebraic K) x using 1, ext a, exact ⟨λ ⟨φ, hφ⟩, ⟨φ.to_rat_alg_hom, hφ⟩, λ ⟨φ, hφ⟩, ⟨φ.to_ring_hom, hφ⟩⟩, end @@ -106,20 +93,17 @@ 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∥), + 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, ← finset.mem_coe] at hz, + haveI : char_zero A := char_zero_of_injective_algebra_map (algebra_map ℚ A).injective, + obtain ⟨φ, rfl⟩ := (rat_range_eq_roots K A x).symm.subset (_ : z ∈ _), { exact h φ }, + rw root_set_def, convert hz using 5, end variables (K A) @@ -132,39 +116,31 @@ 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], + have h_map_ℚ_minpoly := minpoly.gcd_domain_eq_field_fractions' ℚ hx.1, + simp_rw mem_Union, + refine ⟨_, ⟨_, λ i, _⟩, (mem_root_set_iff (minpoly.ne_zero hx.1) x).2 (minpoly.aeval ℤ x)⟩, + { rw [← (minpoly.monic hx.1).nat_degree_map (_ : ℤ →+* ℚ), ← h_map_ℚ_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)), }}, + rw [mem_Icc, ← abs_le, ← @int.cast_le ℝ], + apply le_trans _ (nat.le_ceil _), + convert coeff_bdd_of_norm_le hx.2 i, + 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)], }}, + wlog : b < a := habne using [a b], + refine ⟨a - b, tsub_pos_of_lt habne, _⟩, + rw [← nat.sub_add_cancel habne.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 }, { rw set.maps_univ_to, exact λ a, ⟨hxi.pow a, λ φ, by simp [hx φ, norm_pow, one_pow]⟩, }, end From 5855d168e159df156bf8aa002fe42a201e9124b3 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Tue, 4 Oct 2022 02:58:40 -0400 Subject: [PATCH 5/6] golf bUnion_roots_finite --- src/data/polynomial/ring_division.lean | 28 +++++++++----------------- 1 file changed, 9 insertions(+), 19 deletions(-) diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean index 074500c466758..608c51c1090f9 100644 --- a/src/data/polynomial/ring_division.lean +++ b/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) : From de172ccb5e366668c4e74248bc13ad88bfb50911 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Wed, 5 Oct 2022 19:32:22 -0400 Subject: [PATCH 6/6] out of WIP status --- src/field_theory/is_alg_closed/basic.lean | 23 +++++++ .../number_field/embeddings.lean | 61 ++++++------------- 2 files changed, 41 insertions(+), 43 deletions(-) diff --git a/src/field_theory/is_alg_closed/basic.lean b/src/field_theory/is_alg_closed/basic.lean index 5f7495206061a..5a2282e04aba4 100644 --- a/src/field_theory/is_alg_closed/basic.lean +++ b/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 diff --git a/src/number_theory/number_field/embeddings.lean b/src/number_theory/number_field/embeddings.lean index a968e59358f1c..53e4582bd1cce 100644 --- a/src/number_theory/number_field/embeddings.lean +++ b/src/number_theory/number_field/embeddings.lean @@ -48,38 +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`. -/ --- ! should be moved to another namespace -lemma range_eq_roots (F K A : Type*) [field F] [field K] [field A] [is_alg_closed A] - [algebra F K] (hK : algebra.is_algebraic F K) [algebra F A] (x : K) : - 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), - haveI : fact (irreducible $ minpoly F x) := ⟨minpoly.irreducible $ this 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 _ _ ha), - haveI : is_scalar_tower F Fx K := is_scalar_tower.of_ring_hom (adjoin_root.lift_hom _ _ hx), - 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 - -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 (number_field.is_algebraic K) 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 @@ -96,14 +73,13 @@ 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 : ℕ) : ∥(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 _ _, + 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) (λ z hz, _) i, - classical, rw [← multiset.mem_to_finset, ← finset.mem_coe] at hz, - haveI : char_zero A := char_zero_of_injective_algebra_map (algebra_map ℚ A).injective, - obtain ⟨φ, rfl⟩ := (rat_range_eq_roots K A x).symm.subset (_ : z ∈ _), { exact h φ }, - rw root_set_def, convert hz using 5, + 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) @@ -115,15 +91,13 @@ 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, _), + refine this.subset (λ x hx, _), simp_rw mem_Union, have h_map_ℚ_minpoly := minpoly.gcd_domain_eq_field_fractions' ℚ hx.1, - simp_rw mem_Union, refine ⟨_, ⟨_, λ i, _⟩, (mem_root_set_iff (minpoly.ne_zero hx.1) x).2 (minpoly.aeval ℤ x)⟩, - { rw [← (minpoly.monic hx.1).nat_degree_map (_ : ℤ →+* ℚ), ← h_map_ℚ_minpoly], - exact minpoly.nat_degree_le (is_integral_of_is_scalar_tower _ hx.1), }, + { 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 ℝ], - apply le_trans _ (nat.le_ceil _), - convert coeff_bdd_of_norm_le hx.2 i, + 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 @@ -135,14 +109,15 @@ 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 : b < a := habne using [a b], - refine ⟨a - b, tsub_pos_of_lt habne, _⟩, - rw [← nat.sub_add_cancel habne.le, pow_add, mul_left_eq_self₀] at h, + 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 }, - { rw set.maps_univ_to, - exact λ a, ⟨hxi.pow a, λ φ, by simp [hx φ, norm_pow, one_pow]⟩, }, + { exact λ a _, ⟨hxi.pow a, λ φ, by simp only [hx φ, norm_pow, one_pow, map_pow]⟩ }, end end bounded