feat(ring_theory/discriminant): add of_power_basis_eq_norm (#11149)

From flt-regular.

src/data/fin/interval.lean

@@ -14,6 +14,8 @@ intervals as finsets and fintypes.
 
 open finset fin
 
+open_locale big_operators
+
 variables (n : ℕ)
 
 instance : locally_finite_order (fin n) := subtype.locally_finite_order _
@@ -223,6 +225,23 @@ begin
   { rw [filter_le_le_eq_Icc, card_Icc] }
 end
 
+lemma prod_filter_lt_mul_neg_eq_prod_off_diag {R : Type*} [comm_monoid R] {n : ℕ}
+  {f : fin n → fin n → R} :
+  ∏ i, (∏ j in univ.filter (λ j, i < j), (f j i) * (f i j)) =
+  ∏ i, (∏ j in univ.filter (λ j, i ≠ j), (f j i)) :=
+begin
+  simp_rw [ne_iff_lt_or_gt, or.comm, filter_or, prod_mul_distrib],
+  have : ∀ i : fin n, disjoint (filter (gt i) univ) (filter (has_lt.lt i) univ),
+  { simp_rw disjoint_filter,
+    intros i x y,
+    apply lt_asymm },
+  simp only [prod_union, this, prod_mul_distrib],
+  rw mul_comm,
+  congr' 1,
+  rw [prod_sigma', prod_sigma'],
+  refine prod_bij' (λ i hi, ⟨i.2, i.1⟩) _ _ (λ i hi, ⟨i.2, i.1⟩) _ _ _; simp
+end
+
 end filter
 
 end fin

src/ring_theory/discriminant.lean

@@ -5,6 +5,7 @@ Authors: Riccardo Brasca
 -/
 
 import ring_theory.trace
+import ring_theory.norm
 
 /-!
 # Discriminant of a family of vectors
@@ -26,7 +27,7 @@ Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we
   `algebra.discr A ((P.map (algebra_map A B)).mul_vec b)`.
 * `algebra.discr_not_zero_of_linear_independent` : over a field, if `b` is linear independent, then
   `algebra.discr K b ≠ 0`.
-* `algebra.discr_eq_det_embeddings_matrix_reindex_pow_two` if `L/K` is a field extension and
+* `algebra.discr_eq_det_embeddings_matrix_reindex_pow_two` : if `L/K` is a field extension and
   `b : ι → L`, then `discr K b` is the square of the determinant of the matrix whose `(i, j)`
   coefficient is `σⱼ (b i)`, where `σⱼ : L →ₐ[K] E` is the embedding in an algebraically closed
   field `E` corresponding to `j : ι` via a bijection `e : ι ≃ (L →ₐ[K] E)`.
@@ -64,6 +65,7 @@ variable [fintype ι]
 
 section basic
 
+/-- If `b` is not linear independent, then `algebra.discr A b = 0`. -/
 lemma discr_zero_of_not_linear_independent [is_domain A] {b : ι → B}
   (hli : ¬linear_independent A b) : discr A b = 0 :=
 begin
@@ -82,12 +84,15 @@ end
 
 variable {A}
 
+/-- Relation between `algebra.discr A ι b` and
+`algebra.discr A ((P.map (algebra_map A B)).vec_mul b)`. -/
 lemma discr_of_matrix_vec_mul [decidable_eq ι] (b : ι → B) (P : matrix ι ι A) :
   discr A ((P.map (algebra_map A B)).vec_mul b) = P.det ^ 2 * discr A b :=
 by rw [discr_def, trace_matrix_of_matrix_vec_mul, det_mul, det_mul, det_transpose, mul_comm,
     ← mul_assoc, discr_def, pow_two]
 
-
+/-- Relation between `algebra.discr A ι b` and
+`algebra.discr A ((P.map (algebra_map A B)).mul_vec b)`. -/
 lemma discr_of_matrix_mul_vec [decidable_eq ι] (b : ι → B) (P : matrix ι ι A) :
   discr A ((P.map (algebra_map A B)).mul_vec b) = P.det ^ 2 * discr A b :=
 by rw [discr_def, trace_matrix_of_matrix_mul_vec, det_mul, det_mul, det_transpose,
@@ -102,6 +107,7 @@ variables [algebra K L] [algebra K E]
 variables [module.finite K L] [is_separable K L] [is_alg_closed E]
 variables (b : ι → L) (pb : power_basis K L)
 
+/-- Over a field, if `b` is linear independent, then `algebra.discr K b ≠ 0`. -/
 lemma discr_not_zero_of_linear_independent [nonempty ι]
   (hcard : fintype.card ι = finrank K L) (hli : linear_independent K b) : discr K b ≠ 0 :=
 begin
@@ -113,12 +119,17 @@ begin
   exact trace_form_nondegenerate _ _
 end
 
+/-- If `L/K` is a field extension and `b : ι → L`, then `discr K b` is the square of the
+determinant of the matrix whose `(i, j)` coefficient is `σⱼ (b i)`, where `σⱼ : L →ₐ[K] E` is the
+embedding in an algebraically closed field `E` corresponding to `j : ι` via a bijection
+`e : ι ≃ (L →ₐ[K] E)`. -/
 lemma discr_eq_det_embeddings_matrix_reindex_pow_two [decidable_eq ι]
   (e : ι ≃ (L →ₐ[K] E)) : algebra_map K E (discr K b) =
   (embeddings_matrix_reindex K E b e).det ^ 2 :=
 by rw [discr_def, ring_hom.map_det, ring_hom.map_matrix_apply,
     trace_matrix_eq_embeddings_matrix_reindex_mul_trans, det_mul, det_transpose, pow_two]
 
+/-- The discriminant of a power basis. -/
 lemma discr_power_basis_eq_prod (e : fin pb.dim ≃ (L →ₐ[K] E)) :
   algebra_map K E (discr K pb.basis) =
   ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j), (e j pb.gen- (e i pb.gen)) ^ 2 :=
@@ -129,6 +140,106 @@ begin
   rw [← prod_pow]
 end
 
+/-- A variation of `of_power_basis_eq_prod`. -/
+lemma of_power_basis_eq_prod' (e : fin pb.dim ≃ (L →ₐ[K] E)) :
+  algebra_map K E (discr K pb.basis) =
+  ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j),
+  -((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen))) :=
+begin
+  rw [discr_power_basis_eq_prod _ _ _ e],
+  congr, ext i, congr, ext j,
+  ring
+end
+
+local notation `n` := finrank K L
+
+/-- A variation of `of_power_basis_eq_prod`. -/
+lemma of_power_basis_eq_prod'' (e : fin pb.dim ≃ (L →ₐ[K] E)) :
+  algebra_map K E (discr K pb.basis) =
+  (-1) ^ (n * (n - 1) / 2) * ∏ i : fin pb.dim, ∏ j in finset.univ.filter (λ j, i < j),
+  ((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen))) :=
+begin
+  rw [of_power_basis_eq_prod' _ _ _ e],
+  simp_rw [λ i j, neg_eq_neg_one_mul ((e j pb.gen- (e i pb.gen)) * (e i pb.gen- (e j pb.gen))),
+    prod_mul_distrib],
+  congr,
+  simp only [prod_pow_eq_pow_sum, prod_const],
+  congr,
+  simp_rw [fin.card_filter_lt],
+  apply (@nat.cast_inj ℚ _ _ _ _ _).1,
+  rw [nat.cast_sum],
+  have : ∀ (x : fin pb.dim), (↑x + 1) ≤ pb.dim := by simp [nat.succ_le_iff, fin.is_lt],
+  simp_rw [nat.sub_sub],
+  simp only [nat.cast_sub, this, finset.card_fin, nsmul_eq_mul, sum_const, sum_sub_distrib,
+    nat.cast_add, nat.cast_one, sum_add_distrib, mul_one],
+  rw [← nat.cast_sum, ← @finset.sum_range ℕ _ pb.dim (λ i, i), sum_range_id ],
+  have hn : n = pb.dim,
+  { rw [← alg_hom.card K L E, ← fintype.card_fin pb.dim],
+    exact card_congr (equiv.symm e) },
+  have h₂ : 2 ∣ (pb.dim * (pb.dim - 1)) := even_iff_two_dvd.1 (nat.even_mul_self_pred _),
+  have hne : ((2 : ℕ) : ℚ) ≠ 0 := by simp,
+  have hle : 1 ≤ pb.dim,
+  { rw [← hn, nat.one_le_iff_ne_zero, ← zero_lt_iff, finite_dimensional.finrank_pos_iff],
+    apply_instance },
+  rw [hn, nat.cast_dvd h₂ hne, nat.cast_mul, nat.cast_sub hle],
+  field_simp,
+  ring,
+end
+
+/-- Formula for the discriminant of a power basis using the norm of the field extension. -/
+lemma of_power_basis_eq_norm : discr K pb.basis =
+  (-1) ^ (n * (n - 1) / 2) * (norm K (aeval pb.gen (minpoly K pb.gen).derivative)) :=
+begin
+  let E := algebraic_closure L,
+  letI := λ (a b : E), classical.prop_decidable (eq a b),
+
+  have e : fin pb.dim ≃ (L →ₐ[K] E),
+  { refine equiv_of_card_eq _,
+    rw [fintype.card_fin, alg_hom.card],
+    exact (power_basis.finrank pb).symm },
+  have hnodup : (map (algebra_map K E) (minpoly K pb.gen)).roots.nodup :=
+    nodup_roots (separable.map (is_separable.separable K pb.gen)),
+  have hroots : ∀ σ : L →ₐ[K] E, σ pb.gen ∈ (map (algebra_map K E) (minpoly K pb.gen)).roots,
+  { intro σ,
+    rw [mem_roots, is_root.def, eval_map, ← aeval_def, aeval_alg_hom_apply],
+    repeat { simp [minpoly.ne_zero (is_separable.is_integral K pb.gen)] } },
+
+  apply (algebra_map K E).injective,
+  rw [ring_hom.map_mul, ring_hom.map_pow, ring_hom.map_neg, ring_hom.map_one,
+    of_power_basis_eq_prod'' _ _ _ e],
+  congr,
+  rw [norm_eq_prod_embeddings, fin.prod_filter_lt_mul_neg_eq_prod_off_diag],
+  conv_rhs { congr, skip, funext,
+    rw [← aeval_alg_hom_apply, aeval_root_derivative_of_splits (minpoly.monic
+      (is_separable.is_integral K pb.gen)) (is_alg_closed.splits_codomain _) (hroots σ),
+      ← finset.prod_mk _ (multiset.nodup_erase_of_nodup _ hnodup)] },
+  rw [prod_sigma', prod_sigma'],
+  refine prod_bij (λ i hi, ⟨e i.2, e i.1 pb.gen⟩) (λ i hi, _) (λ i hi, by simp at hi)
+    (λ i j hi hj hij, _) (λ σ hσ, _),
+  { simp only [true_and, mem_mk, mem_univ, mem_sigma],
+    rw [multiset.mem_erase_of_ne (λ h, _)],
+    { exact hroots _ },
+    { simp only [true_and, mem_filter, mem_univ, ne.def, mem_sigma] at hi,
+      refine hi (equiv.injective e (equiv.injective (power_basis.lift_equiv pb) _)),
+      rw [← power_basis.lift_equiv_apply_coe, ← power_basis.lift_equiv_apply_coe] at h,
+      exact subtype.eq h } },
+  { simp only [equiv.apply_eq_iff_eq, heq_iff_eq] at hij,
+    have h := hij.2,
+    rw [← power_basis.lift_equiv_apply_coe, ← power_basis.lift_equiv_apply_coe] at h,
+    refine sigma.eq (equiv.injective e (equiv.injective _ (subtype.eq h))) (by simp [hij.1]) },
+  { simp only [true_and, mem_mk, mem_univ, mem_sigma] at hσ,
+    simp only [sigma.exists, true_and, exists_prop, mem_filter, mem_univ, ne.def, mem_sigma],
+    refine ⟨e.symm (power_basis.lift pb σ.2 _), e.symm σ.1, ⟨λ h, _, sigma.eq _ _⟩⟩,
+    { rw [aeval_def, eval₂_eq_eval_map, ← is_root.def, ← mem_roots],
+      { exact multiset.erase_subset _ _ hσ },
+      { simp [minpoly.ne_zero (is_separable.is_integral K pb.gen)] } },
+    { replace h := alg_hom.congr_fun (equiv.injective _ h) pb.gen,
+      rw [power_basis.lift_gen] at h,
+      rw [← h] at hσ,
+      refine multiset.mem_erase_of_nodup hnodup hσ, },
+    all_goals { simp } }
+end
+
 end field
 
 end discr