feat(ring_theory/discriminant): add discr_mul_is_integral_mem_adjoin (#…

…11396)

We add `discr_mul_is_integral_mem_adjoin`: let `K` be the fraction field of an integrally closed domain `R` and let `L` be a finite
separable extension of `K`. Let `B : power_basis K L` be such that `is_integral R B.gen`. Then for all `z : L` that are integral over `R`, we have `(discr K B.basis) • z ∈ adjoin R ({B.gen} : set L)`.

From flt-regular.

src/field_theory/intermediate_field.lean

@@ -37,7 +37,7 @@ A `subalgebra` is closed under all operations except `⁻¹`,
 intermediate field, field extension
 -/
 
-open finite_dimensional
+open finite_dimensional polynomial
 open_locale big_operators
 
 variables (K L : Type*) [field K] [field L] [algebra K L]
@@ -220,6 +220,24 @@ begin
   { simp [pow_succ, ih] }
 end
 
+@[simp, norm_cast]
+lemma coe_sum {ι : Type*} [fintype ι] (f : ι → S) : (↑∑ i, f i : L) = ∑ i, (f i : L) :=
+begin
+  classical,
+  induction finset.univ using finset.induction_on with i s hi H,
+  { simp },
+  { rw [finset.sum_insert hi, coe_add, H, finset.sum_insert hi] }
+end
+
+@[simp, norm_cast]
+lemma coe_prod {ι : Type*} [fintype ι] (f : ι → S) : (↑∏ i, f i : L) = ∏ i, (f i : L) :=
+begin
+  classical,
+  induction finset.univ using finset.induction_on with i s hi H,
+  { simp },
+  { rw [finset.prod_insert hi, coe_mul, H, finset.prod_insert hi] }
+end
+
 /-! `intermediate_field`s inherit structure from their `subalgebra` coercions. -/
 
 instance module' {R} [semiring R] [has_scalar R K] [module R L] [is_scalar_tower R K L] :
@@ -283,6 +301,29 @@ S.to_subalgebra.val
 lemma range_val : S.val.range = S.to_subalgebra :=
 S.to_subalgebra.range_val
 
+lemma aeval_coe {R : Type*} [comm_ring R] [algebra R K] [algebra R L]
+  [is_scalar_tower R K L] (x : S) (P : polynomial R) : aeval (x : L) P = aeval x P :=
+begin
+  refine polynomial.induction_on' P (λ f g hf hg, _) (λ n r, _),
+  { rw [aeval_add, aeval_add, coe_add, hf, hg] },
+  { simp only [coe_mul, aeval_monomial, coe_pow, mul_eq_mul_right_iff],
+    left, refl }
+end
+
+lemma coe_is_integral_iff {R : Type*} [comm_ring R] [algebra R K] [algebra R L]
+  [is_scalar_tower R K L] {x : S} : is_integral R (x : L) ↔ _root_.is_integral R x :=
+begin
+  refine ⟨λ h, _, λ h, _⟩,
+  { obtain ⟨P, hPmo, hProot⟩ := h,
+    refine ⟨P, hPmo, (ring_hom.injective_iff _).1 (algebra_map ↥S L).injective _ _⟩,
+    letI : is_scalar_tower R S L := is_scalar_tower.of_algebra_map_eq (congr_fun rfl),
+    rwa [eval₂_eq_eval_map, ← eval₂_at_apply, eval₂_eq_eval_map, polynomial.map_map,
+      ← is_scalar_tower.algebra_map_eq, ← eval₂_eq_eval_map] },
+  { obtain ⟨P, hPmo, hProot⟩ := h,
+    refine ⟨P, hPmo, _⟩,
+    rw [← aeval_def, aeval_coe, aeval_def, hProot, coe_zero] },
+end
+
 variables {S}
 
 lemma to_subalgebra_injective {S S' : intermediate_field K L}

src/ring_theory/discriminant.lean

@@ -6,6 +6,7 @@ Authors: Riccardo Brasca
 
 import ring_theory.trace
 import ring_theory.norm
+import ring_theory.integrally_closed
 
 /-!
 # Discriminant of a family of vectors
@@ -32,6 +33,12 @@ Given an `A`-algebra `B` and `b`, an `ι`-indexed family of elements of `B`, we
   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)`.
 * `algebra.discr_of_power_basis_eq_prod` : the discriminant of a power basis.
+* `discr_is_integral` : if `K` and `L` are fields and `is_scalar_tower R K L`, is `b : ι → L`
+  satisfies ` ∀ i, is_integral R (b i)`, then `is_integral R (discr K b)`.
+* `discr_mul_is_integral_mem_adjoin` : let `K` be the fraction field of an integrally closed domain
+  `R` and let `L` be a finite separable extension of `K`. Let `B : power_basis K L` be such that
+  `is_integral R B.gen`. Then for all, `z : L` we have
+  `(discr K B.basis) • z ∈ adjoin R ({B.gen} : set L)`.
 
 ## Implementation details
 
@@ -43,7 +50,7 @@ universes u v w z
 
 open_locale matrix big_operators
 
-open matrix finite_dimensional fintype polynomial finset
+open matrix finite_dimensional fintype polynomial finset intermediate_field
 
 namespace algebra
 
@@ -104,10 +111,10 @@ section field
 
 variables (K : Type u) {L : Type v} (E : Type z) [field K] [field L] [field E]
 variables [algebra K L] [algebra K E]
-variables [module.finite K L] [is_separable K L] [is_alg_closed E]
+variables [module.finite K L]  [is_alg_closed E]
 
 /-- Over a field, if `b` is a basis, then `algebra.discr K b ≠ 0`. -/
-lemma discr_not_zero_of_basis (b : basis ι K L) : discr K b ≠ 0 :=
+lemma discr_not_zero_of_basis [is_separable K L] (b : basis ι K L) : discr K b ≠ 0 :=
 begin
   by_cases h : nonempty ι,
   { classical,
@@ -121,20 +128,24 @@ begin
   simp [discr],
 end
 
+/-- Over a field, if `b` is a basis, then `algebra.discr K b` is a unit. -/
+lemma discr_is_unit_of_basis [is_separable K L] (b : basis ι K L) : is_unit (discr K b) :=
+is_unit.mk0 _ (discr_not_zero_of_basis _ _)
+
 variables (b : ι → L) (pb : power_basis K L)
 
 /-- 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 ι]
+lemma discr_eq_det_embeddings_matrix_reindex_pow_two [decidable_eq ι] [is_separable K L]
   (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)) :
+lemma discr_power_basis_eq_prod (e : fin pb.dim ≃ (L →ₐ[K] E)) [is_separable K L] :
   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 :=
 begin
@@ -145,7 +156,7 @@ begin
 end
 
 /-- A variation of `of_power_basis_eq_prod`. -/
-lemma of_power_basis_eq_prod' (e : fin pb.dim ≃ (L →ₐ[K] E)) :
+lemma of_power_basis_eq_prod' [is_separable K L] (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))) :=
@@ -158,7 +169,7 @@ 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)) :
+lemma of_power_basis_eq_prod'' [is_separable K L] (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))) :=
@@ -191,7 +202,7 @@ begin
 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 =
+lemma of_power_basis_eq_norm [is_separable K L] : 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,
@@ -220,7 +231,7 @@ begin
   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],
+  { simp only [true_and, finset.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,
@@ -231,7 +242,7 @@ begin
     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 [true_and, finset.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],
@@ -244,6 +255,67 @@ begin
     all_goals { simp } }
 end
 
+section integral
+
+variables {R : Type z} [comm_ring R] [algebra R K] [algebra R L] [is_scalar_tower R K L]
+
+local notation `is_integral` := _root_.is_integral
+
+/-- If `K` and `L` are fields and `is_scalar_tower R K L`, and `b : ι → L` satisfies
+` ∀ i, is_integral R (b i)`, then `is_integral R (discr K b)`. -/
+lemma discr_is_integral {b : ι → L} (h : ∀ i, is_integral R (b i)) :
+  is_integral R (discr K b) :=
+begin
+  classical,
+  rw [discr_def],
+  exact is_integral.det (λ i j, is_integral_trace (is_integral_mul (h i) (h j)))
+end
+
+/-- Let `K` be the fraction field of an integrally closed domain `R` and let `L` be a finite
+separable extension of `K`. Let `B : power_basis K L` be such that `is_integral R B.gen`.
+Then for all, `z : L` that are integral over `R`, we have
+`(discr K B.basis) • z ∈ adjoin R ({B.gen} : set L)`. -/
+lemma discr_mul_is_integral_mem_adjoin [is_domain R] [is_separable K L] [is_integrally_closed R]
+  [is_fraction_ring R K] {B : power_basis K L} (hint : is_integral R B.gen) {z : L}
+  (hz : is_integral R z) : (discr K B.basis) • z ∈ adjoin R ({B.gen} : set L) :=
+begin
+  have hinv : is_unit (trace_matrix K B.basis).det :=
+    by simpa [← discr_def] using discr_is_unit_of_basis _ B.basis,
+
+  have H : (trace_matrix K B.basis).det • (trace_matrix K B.basis).mul_vec (B.basis.equiv_fun z) =
+    (trace_matrix K B.basis).det • (λ i, trace K L (z * B.basis i)),
+  { congr, exact trace_matrix_of_basis_mul_vec _ _ },
+  have cramer := mul_vec_cramer (trace_matrix K B.basis) (λ i, trace K L (z * B.basis i)),
+
+  suffices : ∀ i, ((trace_matrix K B.basis).det • (B.basis.equiv_fun z)) i ∈ (⊥ : subalgebra R K),
+  { rw [← B.basis.sum_repr z, finset.smul_sum],
+    refine subalgebra.sum_mem _ (λ i hi, _),
+    replace this := this i,
+    rw [← discr_def, pi.smul_apply, mem_bot] at this,
+    obtain ⟨r, hr⟩ := this,
+    rw [basis.equiv_fun_apply] at hr,
+    rw [← smul_assoc, ← hr, algebra_map_smul],
+    refine subalgebra.smul_mem _ _ _,
+    rw [B.basis_eq_pow i],
+    refine subalgebra.pow_mem _ (subset_adjoin (set.mem_singleton _)) _},
+  intro i,
+  rw [← H, ← mul_vec_smul] at cramer,
+  replace cramer := congr_arg (mul_vec (trace_matrix K B.basis)⁻¹) cramer,
+  rw [mul_vec_mul_vec, nonsing_inv_mul _ hinv, mul_vec_mul_vec, nonsing_inv_mul _ hinv,
+    one_mul_vec, one_mul_vec] at cramer,
+  rw [← congr_fun cramer i, cramer_apply, det_apply],
+  refine subalgebra.sum_mem _ (λ σ _, subalgebra.zsmul_mem _ (subalgebra.prod_mem _ (λ j _, _)) _),
+  by_cases hji : j = i,
+  { simp only [update_column_apply, hji, eq_self_iff_true, power_basis.coe_basis],
+    exact mem_bot.2 (is_integrally_closed.is_integral_iff.1 $ is_integral_trace $
+      is_integral_mul hz $ is_integral.pow hint _) },
+  { simp only [update_column_apply, hji, power_basis.coe_basis],
+    exact mem_bot.2 (is_integrally_closed.is_integral_iff.1 $ is_integral_trace
+      $ is_integral_mul (is_integral.pow hint _) (is_integral.pow hint _)) }
+end
+
+end integral
+
 end field
 
 end discr

src/ring_theory/integral_closure.lean

@@ -7,6 +7,7 @@ import linear_algebra.finite_dimensional
 import ring_theory.adjoin.fg
 import ring_theory.polynomial.scale_roots
 import ring_theory.polynomial.tower
+import linear_algebra.matrix.determinant
 
 /-!
 # Integral closure of a subring.
@@ -368,6 +369,14 @@ theorem mem_integral_closure_iff_mem_fg {r : A} :
 
 variables {R} {A}
 
+lemma adjoin_le_integral_closure {x : A} (hx : is_integral R x) :
+  algebra.adjoin R {x} ≤ integral_closure R A :=
+begin
+  rw [algebra.adjoin_le_iff],
+  simp only [set_like.mem_coe, set.singleton_subset_iff],
+  exact hx
+end
+
 lemma le_integral_closure_iff_is_integral {S : subalgebra R A} :
   S ≤ integral_closure R A ↔ algebra.is_integral R S :=
 set_like.forall.symm.trans (forall_congr (λ x, show is_integral R (algebra_map S A x)
@@ -443,6 +452,14 @@ lemma is_integral.sum {α : Type*} {s : finset α} (f : α → A) (h : ∀ x ∈
   is_integral R (∑ x in s, f x) :=
 (integral_closure R A).sum_mem h
 
+lemma is_integral.det {n : Type*} [fintype n] [decidable_eq n] {M : matrix n n A}
+  (h : ∀ i j, is_integral R (M i j)) :
+  is_integral R M.det :=
+begin
+  rw [matrix.det_apply],
+  exact is_integral.sum _ (λ σ hσ, is_integral.zsmul (is_integral.prod _ (λ i hi, h _ _)) _)
+end
+
 section
 
 variables (p : polynomial R) (x : S)

src/ring_theory/trace.lean

@@ -415,6 +415,26 @@ begin
   rw [trace_matrix, trace_form_apply, trace_form_to_matrix]
 end
 
+lemma trace_matrix_of_basis_mul_vec (b : basis ι A B) (z : B) :
+  (trace_matrix A b).mul_vec (b.equiv_fun z) = (λ i, trace A B (z * (b i))) :=
+begin
+  ext i,
+  rw [← col_apply ((trace_matrix A b).mul_vec (b.equiv_fun z)) i unit.star, col_mul_vec,
+    matrix.mul_apply, trace_matrix_def],
+  simp only [col_apply, trace_form_apply],
+  conv_lhs
+  { congr, skip, funext,
+    rw [mul_comm _ (b.equiv_fun z _), ← smul_eq_mul, ← linear_map.map_smul] },
+    rw [← linear_map.map_sum],
+    congr,
+    conv_lhs
+    { congr, skip, funext,
+      rw [← mul_smul_comm] },
+    rw [← finset.mul_sum, mul_comm z],
+    congr,
+    rw [b.sum_equiv_fun ]
+end
+
 variable (A)
 /-- `embeddings_matrix A C b : matrix κ (B →ₐ[A] C) C` is the matrix whose `(i, σ)` coefficient is
   `σ (b i)`. It is mostly useful for fields when `fintype.card κ = finrank A B` and `C` is