more direct proof

Author: riccardobrasca

FltRegular/CaseII/InductionStep.lean

@@ -70,7 +70,7 @@ include hp hζ e hz in
 lemma x_plus_y_mul_ne_zero : x + y * η ≠ 0 := by
   intro hη
   have : x + y * η ∣ x ^ (p : ℕ) + y ^ (p : ℕ) := by
-    rw [pow_add_pow_eq_prod_add_zeta_runity_mul
+    rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _
       (hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)) hζ.unit'_coe]
     simp_rw [mul_comm _ y]
     exact Finset.dvd_prod_of_mem _ η.prop
@@ -90,7 +90,7 @@ lemma one_sub_zeta_dvd_zeta_pow_sub : π ∣ x + y * η := by
   letI := IsCyclotomicExtension.numberField {p} ℚ K
   have h := zeta_sub_one_dvd hζ e
   replace h : ∏ _η in nthRootsFinset p (𝓞 K), Ideal.Quotient.mk 𝔭 (x + y * η : 𝓞 K) = 0 := by
-    rw [pow_add_pow_eq_prod_add_zeta_runity_mul (hpri.out.eq_two_or_odd.resolve_left
+    rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _ (hpri.out.eq_two_or_odd.resolve_left
       (PNat.coe_injective.ne hp)) hζ.unit'_coe, ← Ideal.Quotient.eq_zero_iff_dvd, map_prod] at h
     convert h using 2 with η' hη'
     rw [map_add, map_add, map_mul, map_mul, IsPrimitiveRoot.eq_one_mod_one_sub' hζ.unit'_coe hη',
@@ -249,7 +249,7 @@ lemma exists_ideal_pow_eq_c_aux :
 /- The ∏_η,  𝔠 η = (𝔷' 𝔭^m)^p with 𝔷 = 𝔪 𝔷' -/
 lemma prod_c : ∏ η in Finset.attach (nthRootsFinset p (𝓞 K)), 𝔠 η = (𝔷' * 𝔭 ^ m) ^ (p : ℕ) := by
   have e' := span_pow_add_pow_eq hζ e
-  rw [pow_add_pow_eq_prod_add_zeta_runity_mul
+  rw [pow_add_pow_eq_prod_add_zeta_runity_mul _ _
     (hpri.out.eq_two_or_odd.resolve_left (PNat.coe_injective.ne hp)) hζ.unit'_coe] at e'
   rw [← Ideal.prod_span_singleton, ← Finset.prod_attach] at e'
   simp_rw [mul_comm _ y, ← m_mul_c_mul_p hp hζ e hy,

FltRegular/NumberTheory/Cyclotomic/Factoring.lean

@@ -3,45 +3,59 @@ Copyright (c) 2021 Alex J. Best. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 
-! This file was ported from Lean 3 source module number_theory.cyclotomic.factoring
 -/
 import  Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
-import FltRegular.ReadyForMathlib.Homogenization
 
-open Polynomial Finset MvPolynomial
+open Polynomial Finset
+
+variable {R : Type*} [CommRing R] [IsDomain R] {ζ : R} {n : ℕ} (x y : R)
 
--- TODO might be nice to have an explicit two variable version of this factorization
--- in an mv_polynomial ring with two chosen variables
 /-- If there is a primitive `n`th root of unity in `K`, then `X ^ n - Y ^ n = ∏ (X - μ Y)`,
 where `μ` varies over the `n`-th roots of unity. -/
-theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul {K : Type _} [CommRing K] [IsDomain K] {ζ : K}
-    {n : ℕ} (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) (x y : K) :
-    x ^ (n : ℕ) - y ^ (n : ℕ) = ∏ ζ : K in nthRootsFinset n K, (x - ζ * y) := by
-  -- suffices to show the identity in a multivariate polynomial ring with two generators over K
-  suffices
-    (X 0 : MvPolynomial (Fin 2) K) ^ (n : ℕ) - X 1 ^ (n : ℕ) =
-      ∏ ζ in nthRootsFinset n K, (X 0 - MvPolynomial.C ζ * X 1)
-    by
-    apply_fun MvPolynomial.eval fun i : Fin 2 => if i = 0 then x else y at this
-    simpa [MvPolynomial.eval_prod] using this
-  -- we know the univariate / one argument version of the identity
-  have := X_pow_sub_one_eq_prod hpos h
-  -- transfer this to a polynomial ring with two variables
-  have := congr_arg (Polynomial.aeval (X 0 : MvPolynomial (Fin 2) K)) this
-  simp only [map_prod, aeval_X_pow, Polynomial.aeval_X, aeval_one, Polynomial.aeval_C,
-    map_sub] at this
-  -- the homogenization of the identity is also true
-  have := congr_arg (homogenization 1) this
-  -- simplify to get the result we want
-  simpa [homogenization_prod, Polynomial.algebraMap_eq, hpos]
+theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul_field {K : Type*} [Field K] {ζ : K} (x y : K)
+    (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
+    x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n K, (x - ζ * y) := by
+  by_cases hy : y = 0
+  · simp only [hy, zero_pow (Nat.not_eq_zero_of_lt hpos), sub_zero, mul_zero, prod_const]
+    congr
+    rw [h.card_nthRootsFinset]
+  have := congr_arg (eval (x/y)) <| X_pow_sub_one_eq_prod hpos h
+  rw [eval_sub, eval_pow, eval_one, eval_X, eval_prod] at this
+  simp_rw [eval_sub, eval_X, eval_C] at this
+  apply_fun (· * y ^ n) at this
+  rw [sub_mul, one_mul, div_pow, div_mul_cancel₀ _ (pow_ne_zero n hy)] at this
+  nth_rw 4 [← h.card_nthRootsFinset] at this
+  rw [mul_comm, pow_card_mul_prod] at this
+  convert this using 2
+  field_simp [hy]
+  rw [mul_comm]
+
+/-- If there is a primitive `n`th root of unity in `R`, then `X ^ n - Y ^ n = ∏ (X - μ Y)`,
+where `μ` varies over the `n`-th roots of unity. -/
+theorem pow_sub_pow_eq_prod_sub_zeta_runity_mul (hpos : 0 < n) (h : IsPrimitiveRoot ζ n) :
+    x ^ n - y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x - ζ * y) := by
+  let K := FractionRing R
+  apply NoZeroSMulDivisors.algebraMap_injective R K
+  rw [map_sub, map_pow, map_pow, map_prod]
+  simp_rw [map_sub, map_mul]
+  have h' : IsPrimitiveRoot (algebraMap R K ζ) n :=
+    h.map_of_injective <| NoZeroSMulDivisors.algebraMap_injective R K
+  rw [pow_sub_pow_eq_prod_sub_zeta_runity_mul_field _ _ hpos h']
+  symm
+  refine prod_nbij (algebraMap R K) (fun a ha ↦ ?_) (fun a _ b _ H ↦
+    NoZeroSMulDivisors.algebraMap_injective R K H) (fun a ha ↦ ?_) (fun _ _ ↦ rfl)
+  · rw [mem_nthRootsFinset hpos, ← map_pow, (mem_nthRootsFinset hpos).1 ha, map_one]
+  · rw [mem_coe, mem_nthRootsFinset hpos] at ha
+    simp only [Set.mem_image, mem_coe]
+    obtain ⟨i, -, hζ⟩ := h'.eq_pow_of_pow_eq_one ha hpos
+    refine ⟨ζ ^ i, ?_, by rwa [map_pow]⟩
+    rw [mem_nthRootsFinset hpos, ← pow_mul, mul_comm, pow_mul, h.pow_eq_one, one_pow]
 
 /-- If there is a primitive `n`th root of unity in `K` and `n` is odd, then
 `X ^ n + Y ^ n = ∏ (X + μ Y)`, where `μ` varies over the `n`-th roots of unity. -/
-theorem pow_add_pow_eq_prod_add_zeta_runity_mul {K : Type _} [CommRing K] [IsDomain K] {ζ : K}
-    {n : ℕ} (hodd : n % 2 = 1) (h : IsPrimitiveRoot ζ n) (x y : K) :
-    x ^ (n : ℕ) + y ^ (n : ℕ) = ∏ ζ : K in nthRootsFinset n K, (x + ζ * y) :=
-  by
-  have := pow_sub_pow_eq_prod_sub_zeta_runity_mul (Nat.odd_iff.mpr hodd).pos h x (-y)
+theorem pow_add_pow_eq_prod_add_zeta_runity_mul (hodd : n % 2 = 1) (h : IsPrimitiveRoot ζ n) :
+    x ^ n + y ^ n = ∏ ζ ∈ nthRootsFinset n R, (x + ζ * y) :=  by
+  have := pow_sub_pow_eq_prod_sub_zeta_runity_mul x (-y) (Nat.odd_iff.mpr hodd).pos h
   simp only [mul_neg, sub_neg_eq_add] at this
   rw [neg_pow, neg_one_pow_eq_pow_mod_two] at this
   simpa [hodd] using this