feat(ring_theory/{trace,norm}): add trace_gen_eq_next_coeff_minpoly a…

…nd norm_gen_eq_coeff_zero_minpoly (#11420)

We add `trace_gen_eq_next_coeff_minpoly` and `norm_gen_eq_coeff_zero_minpoly`.

From flt-regular.

src/field_theory/splitting_field.lean

@@ -505,6 +505,29 @@ begin
   rw [eval_multiset_prod_X_sub_C_derivative hr]
 end
 
+/-- If `P` is a monic polynomial that splits, then `coeff P 0` equals the product of the roots. -/
+lemma prod_roots_eq_coeff_zero_of_monic_of_split {P : polynomial K} (hmo : P.monic)
+  (hP : P.splits (ring_hom.id K)) : coeff P 0 = (-1) ^ P.nat_degree * P.roots.prod :=
+begin
+  nth_rewrite 0 [eq_prod_roots_of_monic_of_splits_id hmo hP],
+  rw [coeff_zero_eq_eval_zero, eval_multiset_prod, multiset.map_map],
+  simp_rw [function.comp_app, eval_sub, eval_X, zero_sub, eval_C],
+  conv_lhs { congr, congr, funext,
+    rw [neg_eq_neg_one_mul] },
+  rw [multiset.prod_map_mul, multiset.map_const, multiset.prod_repeat, multiset.map_id',
+    splits_iff_card_roots.1 hP]
+end
+
+/-- If `P` is a monic polynomial that splits, then `P.next_coeff` equals the sum of the roots. -/
+lemma sum_roots_eq_next_coeff_of_monic_of_split {P : polynomial K} (hmo : P.monic)
+  (hP : P.splits (ring_hom.id K)) : P.next_coeff = - P.roots.sum :=
+begin
+  nth_rewrite 0 [eq_prod_roots_of_monic_of_splits_id hmo hP],
+  rw [monic.next_coeff_multiset_prod _ _ (λ a ha, _)],
+  { simp_rw [next_coeff_X_sub_C, multiset.sum_map_neg] },
+  { exact monic_X_sub_C a }
+end
+
 end splits
 
 end polynomial

src/ring_theory/norm.lean

@@ -47,7 +47,7 @@ variables {ι : Type w} [fintype ι]
 
 open finite_dimensional
 open linear_map
-open matrix
+open matrix polynomial
 
 open_locale big_operators
 open_locale matrix
@@ -100,24 +100,31 @@ end
 
 section eq_prod_roots
 
-lemma norm_gen_eq_prod_roots [algebra K S] (pb : power_basis K S)
+/-- Given `pb : power_basis K S`, then the norm of `pb.gen` is
+`(-1) ^ pb.dim * coeff ((minpoly K pb.gen).map (algebra_map K F)) 0`. -/
+lemma power_basis.norm_gen_eq_coeff_zero_minpoly [algebra K S] (pb : power_basis K S) :
+  (algebra_map K F) (norm K pb.gen) =
+  (-1) ^ pb.dim * coeff ((minpoly K pb.gen).map (algebra_map K F)) 0 :=
+begin
+  rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_left_mul_matrix,
+      ring_hom.map_mul, map_pow, ring_hom.map_neg, ring_hom.map_one, ← coeff_map,
+      fintype.card_fin],
+end
+
+/-- Given `pb : power_basis K S`, then the norm of `pb.gen` is
+`((minpoly K pb.gen).map (algebra_map K F)).roots.prod`. -/
+lemma power_basis.norm_gen_eq_prod_roots [algebra K S] (pb : power_basis K S)
   (hf : (minpoly K pb.gen).splits (algebra_map K F)) :
   algebra_map K F (norm K pb.gen) =
     ((minpoly K pb.gen).map (algebra_map K F)).roots.prod :=
 begin
-  -- Write the LHS as the 0'th coefficient of `minpoly K pb.gen`
-  rw [norm_eq_matrix_det pb.basis, det_eq_sign_charpoly_coeff, charpoly_left_mul_matrix,
-      ring_hom.map_mul, ring_hom.map_pow, ring_hom.map_neg, ring_hom.map_one,
-      ← polynomial.coeff_map, fintype.card_fin],
-  -- Rewrite `minpoly K pb.gen` as a product over the roots.
-  conv_lhs { rw polynomial.eq_prod_roots_of_splits hf },
-  rw [polynomial.coeff_C_mul, polynomial.coeff_zero_multiset_prod, multiset.map_map,
-      (minpoly.monic pb.is_integral_gen).leading_coeff, ring_hom.map_one, one_mul],
-  -- Incorporate the `-1` from the `charpoly` back into the product.
-  rw [← multiset.prod_repeat (-1 : F), ← pb.nat_degree_minpoly,
-      polynomial.nat_degree_eq_card_roots hf, ← multiset.map_const, ← multiset.prod_map_mul],
-  -- And conclude that both sides are the same.
-  congr, convert multiset.map_id _, ext f, simp
+  rw [power_basis.norm_gen_eq_coeff_zero_minpoly, ← pb.nat_degree_minpoly,
+    prod_roots_eq_coeff_zero_of_monic_of_split
+      (monic_map _ (minpoly.monic (power_basis.is_integral_gen _)))
+      ((splits_id_iff_splits _).2 hf)],
+  simp only [power_basis.nat_degree_minpoly, nat_degree_map],
+  rw [← mul_assoc, ← mul_pow],
+  simp
 end
 
 end eq_prod_roots
@@ -194,8 +201,8 @@ lemma norm_eq_prod_embeddings_gen
     (@@finset.univ (power_basis.alg_hom.fintype pb)).prod (λ σ, σ pb.gen) :=
 begin
   letI := classical.dec_eq E,
-  rw [norm_gen_eq_prod_roots pb hE, fintype.prod_equiv pb.lift_equiv', finset.prod_mem_multiset,
-    finset.prod_eq_multiset_prod, multiset.to_finset_val,
+  rw [power_basis.norm_gen_eq_prod_roots pb hE, fintype.prod_equiv pb.lift_equiv',
+    finset.prod_mem_multiset, finset.prod_eq_multiset_prod, multiset.to_finset_val,
     multiset.erase_dup_eq_self.mpr, multiset.map_id],
   { exact nodup_roots ((separable_map _).mpr hfx) },
   { intro x, refl },

src/ring_theory/trace.lean

@@ -195,29 +195,31 @@ open algebra polynomial
 variables {F : Type*} [field F]
 variables [algebra K S] [algebra K F]
 
-lemma power_basis.trace_gen_eq_sum_roots [nontrivial S] (pb : power_basis K S)
-  (hf : (minpoly K pb.gen).splits (algebra_map K F)) :
+/-- Given `pb : power_basis K S`, then the trace of `pb.gen` is
+`-((minpoly K pb.gen).map (algebra_map K F)).next_coeff`. -/
+lemma power_basis.trace_gen_eq_next_coeff_minpoly [nontrivial S] (pb : power_basis K S) :
   algebra_map K F (trace K S pb.gen) =
-    ((minpoly K pb.gen).map (algebra_map K F)).roots.sum :=
+    -((minpoly K pb.gen).map (algebra_map K F)).next_coeff :=
 begin
   have d_pos : 0 < pb.dim := power_basis.dim_pos pb,
   have d_pos' : 0 < (minpoly K pb.gen).nat_degree, { simpa },
   haveI : nonempty (fin pb.dim) := ⟨⟨0, d_pos⟩⟩,
-  -- Write the LHS as the `d-1`'th coefficient of `minpoly K pb.gen`
   rw [trace_eq_matrix_trace pb.basis, trace_eq_neg_charpoly_coeff, charpoly_left_mul_matrix,
       ring_hom.map_neg, ← pb.nat_degree_minpoly, fintype.card_fin,
       ← next_coeff_of_pos_nat_degree _ d_pos',
-      ← next_coeff_map (algebra_map K F).injective],
-  -- Rewrite `minpoly K pb.gen` as a product over the roots.
-  conv_lhs { rw eq_prod_roots_of_splits hf },
-  rw [monic.next_coeff_mul, next_coeff_C_eq_zero, zero_add, monic.next_coeff_multiset_prod],
-  -- And conclude both sides are the same.
-  simp_rw [next_coeff_X_sub_C, multiset.sum_map_neg, neg_neg],
-  -- Now we deal with the side conditions.
-  { intros, apply monic_X_sub_C },
-  { convert monic_one, simp [(minpoly.monic pb.is_integral_gen).leading_coeff] },
-  { apply monic_multiset_prod_of_monic,
-    intros, apply monic_X_sub_C },
+      ← next_coeff_map (algebra_map K F).injective]
+end
+
+/-- Given `pb : power_basis K S`, then the trace of `pb.gen` is
+`((minpoly K pb.gen).map (algebra_map K F)).roots.sum`. -/
+lemma power_basis.trace_gen_eq_sum_roots [nontrivial S] (pb : power_basis K S)
+  (hf : (minpoly K pb.gen).splits (algebra_map K F)) :
+  algebra_map K F (trace K S pb.gen) =
+    ((minpoly K pb.gen).map (algebra_map K F)).roots.sum :=
+begin
+  rw [power_basis.trace_gen_eq_next_coeff_minpoly, sum_roots_eq_next_coeff_of_monic_of_split
+    (monic_map _ (minpoly.monic (power_basis.is_integral_gen _)))
+    ((splits_id_iff_splits _).2 hf), neg_neg]
 end
 
 namespace intermediate_field.adjoin_simple