feat(number_theory/cyclotomic/discriminant): add discr_zeta_eq_discr_…

…zeta_sub_one (#12710)

We add `discr_zeta_eq_discr_zeta_sub_one`: the discriminant of the power basis given by a primitive root of unity `ζ` is the same as the
discriminant of the power basis given by `ζ - 1`.

from flt-regular

src/number_theory/cyclotomic/basic.lean

@@ -54,7 +54,8 @@ All results are in the `is_cyclotomic_extension` namespace.
 Note that some results, for example `is_cyclotomic_extension.trans`,
 `is_cyclotomic_extension.finite`, `is_cyclotomic_extension.number_field`,
 `is_cyclotomic_extension.finite_dimensional`, `is_cyclotomic_extension.is_galois` and
-`cyclotomic_field.algebra_base` are lemmas, but they can be made local instances.
+`cyclotomic_field.algebra_base` are lemmas, but they can be made local instances. Some of them are
+included in the `cyclotomic` locale.
 
 -/
 
@@ -217,6 +218,8 @@ lemma number_field [h : number_field K] [fintype S] [is_cyclotomic_extension S K
     (@algebra_rat L _ (char_zero_of_injective_algebra_map (algebra_map K L).injective)) _ _
     h.to_finite_dimensional (finite S K L) }
 
+localized "attribute [instance] is_cyclotomic_extension.number_field" in cyclotomic
+
 /-- A finite cyclotomic extension of an integral noetherian domain is integral -/
 lemma integral [is_domain B] [is_noetherian_ring A] [fintype S] [is_cyclotomic_extension S A B] :
   algebra.is_integral A B :=
@@ -227,6 +230,8 @@ lemma finite_dimensional (C : Type z) [fintype S] [comm_ring C] [algebra K C] [i
   [is_cyclotomic_extension S K C] : finite_dimensional K C :=
 finite S K C
 
+localized "attribute [instance] is_cyclotomic_extension.finite_dimensional" in cyclotomic
+
 end fintype
 
 section
@@ -350,6 +355,8 @@ lemma splitting_field_X_pow_sub_one : is_splitting_field K L (X ^ (n : ℕ) - 1)
       n.pos _), is_root.def, eval_sub, eval_pow, eval_C, eval_X, sub_eq_zero]
   end }
 
+localized "attribute [instance] is_cyclotomic_extension.splitting_field_X_pow_sub_one" in cyclotomic
+
 include n
 
 lemma is_galois : is_galois K L :=
@@ -359,6 +366,8 @@ begin
     (ne_zero.ne _ : ((n : ℕ) : K) ≠ 0)),
 end
 
+localized "attribute [instance] is_cyclotomic_extension.is_galois" in cyclotomic
+
 /-- If `is_cyclotomic_extension {n} K L` and `ne_zero ((n : ℕ) : K)`, then `L` is the splitting
 field of `cyclotomic n K`. -/
 lemma splitting_field_cyclotomic : is_splitting_field K L (cyclotomic n K) :=
@@ -373,6 +382,8 @@ lemma splitting_field_cyclotomic : is_splitting_field K L (cyclotomic n K) :=
     refine adjoin_roots_cyclotomic_eq_adjoin_nth_roots n hζ
   end }
 
+localized "attribute [instance] is_cyclotomic_extension.splitting_field_cyclotomic" in cyclotomic
+
 end singleton
 
 end field

src/number_theory/cyclotomic/discriminant.lean

@@ -20,15 +20,41 @@ We compute the discriminant of a `p`-th cyclotomic extension.
 -/
 
 universes u v
-variables {p : ℕ+} (k : ℕ) {K : Type u} {L : Type v} {ζ : L} [field K] [field L]
-variables [algebra K L] [ne_zero ((p : ℕ) : K)]
 
-open algebra polynomial nat is_primitive_root
+open algebra polynomial nat is_primitive_root power_basis
+
+open_locale polynomial cyclotomic
+
+namespace is_primitive_root
+
+variables {n : ℕ+} {K : Type u} [field K] [char_zero K] {ζ : K}
+variables [is_cyclotomic_extension {n} ℚ K]
+
+/-- The discriminant of the power basis given by a primitive root of unity `ζ` is the same as the
+discriminant of the power basis given by `ζ - 1`. -/
+lemma discr_zeta_eq_discr_zeta_sub_one (hζ : is_primitive_root ζ n) :
+  discr ℚ (hζ.power_basis ℚ).basis = discr ℚ (hζ.sub_one_power_basis ℚ).basis :=
+begin
+  have H₁ : (aeval (hζ.power_basis ℚ).gen) (X - 1 : ℤ[X]) = (hζ.sub_one_power_basis ℚ).gen :=
+    by simp,
+  have H₂ : (aeval (hζ.sub_one_power_basis ℚ).gen) (X + 1 : ℤ[X]) = (hζ.power_basis ℚ).gen :=
+    by simp,
+  refine discr_eq_discr_of_to_matrix_coeff_is_integral _
+    (λ i j, to_matrix_is_integral H₁ _  _ _ _)
+    (λ i j, to_matrix_is_integral H₂ _  _ _ _),
+  { exact hζ.is_integral n.pos },
+  { refine minpoly.gcd_domain_eq_field_fractions _ (hζ.is_integral n.pos) },
+  { exact is_integral_sub (hζ.is_integral n.pos) is_integral_one },
+  { refine minpoly.gcd_domain_eq_field_fractions _ _,
+    exact is_integral_sub (hζ.is_integral n.pos) is_integral_one }
+end
+
+end is_primitive_root
 
 namespace is_cyclotomic_extension
 
-local attribute [instance] is_cyclotomic_extension.finite_dimensional
-local attribute [instance] is_cyclotomic_extension.is_galois
+variables {p : ℕ+} (k : ℕ) {K : Type u} {L : Type v} {ζ : L} [field K] [field L]
+variables [algebra K L] [ne_zero ((p : ℕ) : K)]
 
 /-- If `p` is an odd prime and `is_cyclotomic_extension {p} K L`, then
 `discr K (hζ.power_basis K).basis = (-1) ^ ((p - 1) / 2) * p ^ (p - 2)`. -/

src/number_theory/cyclotomic/gal.lean

@@ -45,6 +45,8 @@ variables {n : ℕ+} (K : Type*) [field K] {L : Type*} [field L] {μ : L} (hμ :
 
 open polynomial ne_zero is_cyclotomic_extension
 
+open_locale cyclotomic
+
 namespace is_primitive_root
 
 /-- `is_primitive_root.aut_to_pow` is injective in the case that it's considered over a cyclotomic
@@ -154,8 +156,6 @@ section gal
 
 variables (h : irreducible (cyclotomic n K)) {K}
 
-local attribute [instance] splitting_field_X_pow_sub_one splitting_field_cyclotomic
-
 /-- `is_cyclotomic_extension.aut_equiv_pow` repackaged in terms of `gal`. Asserts that the
 Galois group of `cyclotomic n K` is equivalent to `(zmod n)ˣ` if `n` does not divide the
 characteristic of `K`, and `cyclotomic n K` is irreducible in the base field. -/

src/ring_theory/adjoin/power_basis.lean

@@ -6,6 +6,7 @@ Authors: Anne Baanen
 
 import ring_theory.adjoin.basic
 import ring_theory.power_basis
+import linear_algebra.matrix.basis
 
 /-!
 # Power basis for `algebra.adjoin R {x}`
@@ -71,3 +72,122 @@ open algebra
 (algebra.adjoin.power_basis hint).map $
   (subalgebra.equiv_of_eq _ _ $ power_basis.adjoin_eq_top_of_gen_mem_adjoin hx).trans
   subalgebra.top_equiv
+
+section is_integral
+
+namespace power_basis
+
+open polynomial
+
+open_locale polynomial
+
+variables {R : Type*} [comm_ring R] [algebra R S] [algebra R K] [is_scalar_tower R K S]
+variables {A : Type*} [comm_ring A] [algebra R A] [algebra S A]
+variables [is_scalar_tower R S A] {B : power_basis S A} (hB : is_integral R B.gen)
+
+include hB
+
+/-- If `B : power_basis S A` is such that `is_integral R B.gen`, then
+`is_integral R (B.basis.repr (B.gen ^ n) i)` for all `i` if
+`minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)`. This is the case if `R` is a GCD domain
+and `S` is its fraction ring. -/
+lemma repr_gen_pow_is_integral [is_domain S]
+  (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)) (n : ℕ) :
+  ∀ i, is_integral R (B.basis.repr (B.gen ^ n) i) :=
+begin
+  intro i,
+  let Q := (X ^ n) %ₘ (minpoly R B.gen),
+  have : B.gen ^ n = aeval B.gen Q,
+  { rw [← @aeval_X_pow R _ _ _ _ B.gen, ← mod_by_monic_add_div (X ^ n) (minpoly.monic hB)],
+    simp },
+  by_cases hQ : Q = 0,
+  { simp [this, hQ, is_integral_zero] },
+  have hlt : Q.nat_degree < B.dim,
+  { rw [← B.nat_degree_minpoly, hmin, (minpoly.monic hB).nat_degree_map,
+      nat_degree_lt_nat_degree_iff hQ],
+    letI : nontrivial R := nontrivial.of_polynomial_ne hQ,
+    exact degree_mod_by_monic_lt _ (minpoly.monic hB),
+    apply_instance },
+  rw [this, aeval_eq_sum_range' hlt],
+  simp only [linear_equiv.map_sum, linear_equiv.map_smulₛₗ, ring_hom.id_apply, finset.sum_apply'],
+  refine is_integral.sum _ (λ j hj, _),
+  replace hj := finset.mem_range.1 hj,
+  rw [← fin.coe_mk hj, ← B.basis_eq_pow, algebra.smul_def,
+    is_scalar_tower.algebra_map_apply R S A, ← algebra.smul_def, linear_equiv.map_smul],
+  simp only [algebra_map_smul, finsupp.coe_smul, pi.smul_apply, B.basis.repr_self_apply],
+  by_cases hij : (⟨j, hj⟩ : fin _) = i,
+  { simp only [hij, eq_self_iff_true, if_true],
+    rw [algebra.smul_def, mul_one],
+    exact is_integral_algebra_map },
+  { simp [hij, is_integral_zero] }
+end
+
+variable {B}
+
+/-- Let `B : power_basis S A` be such that `is_integral R B.gen`, and let `x y : A` be elements with
+integral coordinates in the base `B.basis`. Then `is_integral R ((B.basis.repr (x * y) i)` for all
+`i` if `minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)`. This is the case if `R` is a GCD
+domain and `S` is its fraction ring. -/
+lemma repr_mul_is_integral [is_domain S] {x y : A} (hx : ∀ i, is_integral R (B.basis.repr x i))
+  (hy : ∀ i, is_integral R (B.basis.repr y i))
+  (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)) :
+  ∀ i, is_integral R ((B.basis.repr (x * y) i)) :=
+begin
+  intro i,
+  rw [← B.basis.sum_repr x, ← B.basis.sum_repr y, finset.sum_mul_sum, linear_equiv.map_sum,
+    finset.sum_apply'],
+  refine is_integral.sum _ (λ I hI, _),
+  simp only [algebra.smul_mul_assoc, algebra.mul_smul_comm, linear_equiv.map_smulₛₗ,
+    ring_hom.id_apply, finsupp.coe_smul, pi.smul_apply, id.smul_eq_mul],
+  refine is_integral_mul (hy _) (is_integral_mul (hx _) _),
+  simp only [coe_basis, ← pow_add],
+  refine repr_gen_pow_is_integral hB hmin _ _,
+end
+
+/-- Let `B : power_basis S A` be such that `is_integral R B.gen`, and let `x : A` be and element
+with integral coordinates in the base `B.basis`. Then `is_integral R ((B.basis.repr (x ^ n) i)` for
+all `i` and all `n` if `minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)`. This is the case
+if `R` is a GCD domain and `S` is its fraction ring. -/
+lemma repr_pow_is_integral [is_domain S] {x : A} (hx : ∀ i, is_integral R (B.basis.repr x i))
+  (hmin : minpoly S B.gen = (minpoly R B.gen).map (algebra_map R S)) (n : ℕ) :
+  ∀ i, is_integral R ((B.basis.repr (x ^ n) i)) :=
+begin
+  by_cases htriv : nontrivial A, swap,
+  { intro i,
+    rw [subsingleton_iff.1 (not_nontrivial_iff_subsingleton.1 htriv) (x ^ n) 0],
+    simp [is_integral_zero] },
+  letI := htriv,
+  revert hx,
+  refine nat.case_strong_induction_on n _ (λ n hn, _),
+  { intros hx i,
+    rw [pow_zero, ← pow_zero B.gen, ← fin.coe_mk B.dim_pos, ← B.basis_eq_pow,
+      B.basis.repr_self_apply],
+    by_cases hi : (⟨0, B.dim_pos⟩ : fin _) = i,
+    { simp [hi, is_integral_one] },
+    { simp [hi, is_integral_zero] } },
+  { intros hx i,
+    rw [pow_succ],
+    refine repr_mul_is_integral hB hx (λ _, hn _ le_rfl (λ _, hx _) _) hmin _ }
+end
+
+/-- Let `B B' : power_basis K S` be such that `is_integral R B.gen`, and let `P : R[X]` be such that
+`aeval B.gen P = B'.gen`. Then `is_integral R (B.basis.to_matrix B'.basis i j)` for all `i` and `j`
+if `minpoly K B.gen = (minpoly R B.gen).map (algebra_map R L)`. This is the case
+if `R` is a GCD domain and `K` is its fraction ring. -/
+lemma to_matrix_is_integral {B B' : power_basis K S} {P : R[X]} (h : aeval B.gen P = B'.gen)
+  (hB : is_integral R B.gen) (hmin : minpoly K B.gen = (minpoly R B.gen).map (algebra_map R K)) :
+  ∀ i j, _root_.is_integral R (B.basis.to_matrix B'.basis i j) :=
+begin
+  intros i j,
+  rw [B.basis.to_matrix_apply, B'.coe_basis],
+  refine repr_pow_is_integral hB (λ i, _) hmin _ _,
+  rw [← h, aeval_eq_sum_range, linear_equiv.map_sum, finset.sum_apply'],
+  refine is_integral.sum _ (λ n hn, _),
+  rw [algebra.smul_def, is_scalar_tower.algebra_map_apply R K S, ← algebra.smul_def,
+    linear_equiv.map_smul, algebra_map_smul],
+  exact is_integral_smul _ (repr_gen_pow_is_integral hB hmin _ _),
+end
+
+end power_basis
+
+end is_integral