[Merged by Bors] - feat: a polynomial over a perfect field is separable iff it is square-free

Mathlib.lean

@@ -477,7 +477,8 @@ import Mathlib.Algebra.Ring.ULift
 import Mathlib.Algebra.Ring.Units
 import Mathlib.Algebra.RingQuot
 import Mathlib.Algebra.SMulWithZero
-import Mathlib.Algebra.Squarefree
+import Mathlib.Algebra.Squarefree.Basic
+import Mathlib.Algebra.Squarefree.UniqueFactorizationDomain
 import Mathlib.Algebra.Star.Basic
 import Mathlib.Algebra.Star.BigOperators
 import Mathlib.Algebra.Star.CHSH

Mathlib/Algebra/Squarefree.lean → Mathlib/Algebra/Squarefree/Basic.lean

@@ -85,6 +85,14 @@ theorem Squarefree.squarefree_of_dvd [CommMonoid R] {x y : R} (hdvd : x ∣ y) (
     Squarefree x := fun _ h => hsq _ (h.trans hdvd)
 #align squarefree.squarefree_of_dvd Squarefree.squarefree_of_dvd
 
+theorem Squarefree.eq_zero_or_one_of_pow_of_not_isUnit [CommMonoid R] {x : R} {n : ℕ}
+    (h : Squarefree (x ^ n)) (h' : ¬ IsUnit x) :
+    n = 0 ∨ n = 1 := by
+  contrapose! h'
+  replace h' : 2 ≤ n := by omega
+  have : x * x ∣ x ^ n := by rw [← sq]; exact pow_dvd_pow x h'
+  exact h.squarefree_of_dvd this x (refl _)
+
 section SquarefreeGcdOfSquarefree
 
 variable {α : Type*} [CancelCommMonoidWithZero α] [GCDMonoid α]

Mathlib/Algebra/Squarefree/UniqueFactorizationDomain.lean

@@ -0,0 +1,105 @@
+/-
+Copyright (c) 2024 Oliver Nash. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Oliver Nash
+-/
+import Mathlib.Algebra.Squarefree.Basic
+import Mathlib.RingTheory.UniqueFactorizationDomain
+
+/-!
+# Square-free elements of unique factorization monoids
+
+## Main results:
+ * `squarefree_mul_iff`: `x * y` is square-free iff `x` and `y` have no common factors and are
+   themselves square-free.
+
+-/
+
+variable {R : Type*} [CancelCommMonoidWithZero R] [UniqueFactorizationMonoid R] {x y p d : R}
+
+open UniqueFactorizationMonoid
+
+theorem squarefree_iff (hx₀ : x ≠ 0) (hxu : ¬ IsUnit x) :
+    Squarefree x ↔ ∀ p, Prime p → ¬ (p * p ∣ x) := by
+  refine ⟨fun h p hp hp' ↦ hp.not_unit (h p hp'), fun h d hd ↦ ?_⟩
+  induction' d using induction_on_prime with u hu z p _ hp _
+  · obtain ⟨p, hp⟩ := exists_prime_iff.mpr ⟨x, ⟨hx₀, hxu⟩⟩
+    rw [mul_zero, zero_dvd_iff] at hd
+    simpa [hd] using h p hp
+  · assumption
+  · specialize h p hp
+    replace hd : p * p ∣ x := by rw [mul_mul_mul_comm] at hd; exact dvd_of_mul_right_dvd hd
+    contradiction
+
+namespace Squarefree
+
+theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right {k : ℕ}
+    (hx : Squarefree x) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) :
+    p ^ k ∣ y := by
+  nontriviality R
+  rcases eq_or_ne x 0 with rfl | hx₀
+  · have := not_squarefree_zero hx; contradiction
+  wlog hxu : ¬ IsUnit x
+  · rw [not_not] at hxu; rw [hxu.dvd_mul_left] at h; rw [pow_succ] at h; exact dvd_of_mul_left_dvd h
+  rw [squarefree_iff hx₀ hxu] at hx
+  by_cases hxp : p ∣ x
+  · obtain ⟨x', rfl⟩ := hxp
+    have hx' : ¬ p ∣ x' := by
+      specialize hx p hp
+      contrapose! hx
+      exact mul_dvd_mul_left p hx
+    replace h : p ^ k ∣ x' * y := by
+      rw [pow_succ, mul_assoc] at h
+      exact (mul_dvd_mul_iff_left hp.ne_zero).mp h
+    exact hp.pow_dvd_of_dvd_mul_left _ hx' h
+  · exact dvd_trans (pow_dvd_pow _ (k.le_add_right 1)) (hp.pow_dvd_of_dvd_mul_left _ hxp h)
+
+theorem pow_dvd_of_squarefree_of_pow_succ_dvd_mul_left {k : ℕ}
+    (hy : Squarefree y) (hp : Prime p) (h : p ^ (k + 1) ∣ x * y) :
+    p ^ k ∣ x := by
+  rw [mul_comm] at h
+  exact pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hy hp h
+
+theorem dvd_of_squarefree_of_mul_dvd_mul_right
+    (hx : Squarefree x) (h : d * d ∣ x * y) :
+    d ∣ y := by
+  nontriviality R
+  rcases eq_or_ne x 0 with rfl | hx₀
+  · have := not_squarefree_zero hx; contradiction
+  induction' d using UniqueFactorizationMonoid.induction_on_coprime with u hu p k hp a b hab' ha hb
+  · simpa [hx₀] using h
+  · exact hu.dvd
+  · cases' k with k; · simp
+    apply pow_dvd_of_squarefree_of_pow_succ_dvd_mul_right hx hp
+    rw [← pow_add] at h
+    suffices p ^ ((k + 1) + 1) ∣ p ^ ((k + 1) + (k + 1)) by exact dvd_trans this h
+    apply pow_dvd_pow
+    omega
+  · rw [mul_mul_mul_comm] at h
+    exact mul_dvd_of_coprime hab' (ha <| dvd_of_mul_right_dvd h) (hb <| dvd_of_mul_left_dvd h)
+
+theorem dvd_of_squarefree_of_mul_dvd_mul_left
+    (hy : Squarefree y) (h : d * d ∣ x * y) :
+    d ∣ x := by
+  rw [mul_comm x y] at h
+  exact dvd_of_squarefree_of_mul_dvd_mul_right hy h
+
+end Squarefree
+
+theorem squarefree_mul_iff :
+    Squarefree (x * y) ↔ (∀ d, d ∣ x → d ∣ y → IsUnit d) ∧ Squarefree x ∧ Squarefree y := by
+  nontriviality R
+  refine ⟨fun h ↦ ⟨fun d hx hy ↦ h d (mul_dvd_mul hx hy),
+    h.of_mul_left, h.of_mul_right⟩, fun ⟨hxy, hx, hy⟩ ↦ ?_⟩
+  intro d
+  induction' d using UniqueFactorizationMonoid.induction_on_prime with _ hu _ p _ hp _
+  · simp [hx.ne_zero, hy.ne_zero]
+  · exact fun _ ↦ hu
+  · intro contra
+    exfalso
+    apply hp.not_unit
+    suffices p ∣ x ∧ p ∣ y by exact hxy p this.1 this.2
+    replace contra : p * p ∣ x * y := by
+      rw [mul_mul_mul_comm] at contra; exact dvd_of_mul_right_dvd contra
+    exact ⟨hy.dvd_of_squarefree_of_mul_dvd_mul_left contra,
+      hx.dvd_of_squarefree_of_mul_dvd_mul_right contra⟩

Mathlib/Data/Nat/Squarefree.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import Mathlib.Algebra.Squarefree
+import Mathlib.Algebra.Squarefree.Basic
 import Mathlib.Data.Nat.Factorization.PrimePow
 import Mathlib.RingTheory.Int.Basic
 

Mathlib/FieldTheory/IsAlgClosed/Basic.lean

@@ -285,7 +285,7 @@ noncomputable instance (priority := 100) perfectRing (p : ℕ) [Fact p.Prime] [C
 
 noncomputable instance (priority := 100) perfectField [IsAlgClosed k] : PerfectField k := by
   obtain _ | ⟨p, _, _⟩ := CharP.exists' k
-  exacts [.ofCharZero k, PerfectRing.toPerfectField k p]
+  exacts [.ofCharZero, PerfectRing.toPerfectField k p]
 
 /-- Algebraically closed fields are infinite since `Xⁿ⁺¹ - 1` is separable when `#K = n` -/
 instance (priority := 500) {K : Type*} [Field K] [IsAlgClosed K] : Infinite K := by

Mathlib/FieldTheory/Perfect.lean

@@ -6,6 +6,7 @@ Authors: Oliver Nash
 import Mathlib.FieldTheory.Separable
 import Mathlib.FieldTheory.SplittingField.Construction
 import Mathlib.Algebra.CharP.Reduced
+import Mathlib.Algebra.Squarefree.UniqueFactorizationDomain
 
 /-!
 
@@ -24,6 +25,8 @@ prime characteristic.
    sense of Serre.
  * `PerfectField.ofCharZero`: all fields of characteristic zero are perfect.
  * `PerfectField.ofFinite`: all finite fields are perfect.
+ * `PerfectField.separable_iff_squarefree`: a polynomial over a perfect field is separable iff
+   it is square-free.
  * `Algebra.IsAlgebraic.isSeparable_of_perfectField`, `Algebra.IsAlgebraic.perfectField`:
    if `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable,
    and `L` is also a perfect field.
@@ -178,7 +181,7 @@ lemma PerfectRing.toPerfectField (K : Type*) (p : ℕ)
 
 namespace PerfectField
 
-variable (K : Type*) [Field K]
+variable {K : Type*} [Field K]
 
 instance ofCharZero [CharZero K] : PerfectField K := ⟨Irreducible.separable⟩
 
@@ -220,6 +223,23 @@ instance toPerfectRing (p : ℕ) [hp : Fact p.Prime] [CharP K p] : PerfectRing K
   rw [g.natDegree_map ι, ← Nat.pos_iff_ne_zero, natDegree_pos_iff_degree_pos]
   exact minpoly.degree_pos ha
 
+theorem separable_iff_squarefree {g : K[X]} : g.Separable ↔ Squarefree g := by
+  refine ⟨Separable.squarefree, ?_⟩
+  induction' g using UniqueFactorizationMonoid.induction_on_coprime with p hp p n hp p q _ ihp ihq
+  · simp
+  · obtain ⟨x, hx, rfl⟩ := isUnit_iff.mp hp
+    exact fun _ ↦ (separable_C x).mpr hx
+  · intro hpn
+    rcases hpn.eq_zero_or_one_of_pow_of_not_isUnit hp.not_unit with rfl | rfl; · simp
+    exact (pow_one p).symm ▸ PerfectField.separable_of_irreducible hp.irreducible
+  · intro hpq'
+    obtain ⟨h, hp, hq⟩ := squarefree_mul_iff.mp hpq'
+    apply (ihp hp).mul (ihq hq)
+    classical
+    apply EuclideanDomain.isCoprime_of_dvd
+    · rintro ⟨rfl, rfl⟩; simp at hp
+    · exact fun d hd _ hdp hdq ↦ mem_nonunits_iff.mpr hd <| h d hdp hdq
+
 end PerfectField
 
 /-- If `L / K` is an algebraic extension, `K` is a perfect field, then `L / K` is separable. -/

Mathlib/FieldTheory/Separable.lean

@@ -3,7 +3,7 @@ Copyright (c) 2020 Kenny Lau. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Kenny Lau
 -/
-import Mathlib.Algebra.Squarefree
+import Mathlib.Algebra.Squarefree.Basic
 import Mathlib.Data.Polynomial.Expand
 import Mathlib.Data.Polynomial.Splits
 import Mathlib.FieldTheory.Minpoly.Field
@@ -56,6 +56,7 @@ theorem not_separable_zero [Nontrivial R] : ¬Separable (0 : R[X]) := by
 theorem Separable.ne_zero [Nontrivial R] {f : R[X]} (h : f.Separable) : f ≠ 0 :=
   (not_separable_zero <| · ▸ h)
 
+@[simp]
 theorem separable_one : (1 : R[X]).Separable :=
   isCoprime_one_left
 #align polynomial.separable_one Polynomial.separable_one
@@ -173,6 +174,10 @@ theorem multiplicity_le_one_of_separable {p q : R[X]} (hq : ¬IsUnit q) (hsep :
   exact h
 #align polynomial.multiplicity_le_one_of_separable Polynomial.multiplicity_le_one_of_separable
 
+/-- A separable polynomial is square-free.
+
+See `PerfectField.separable_iff_squarefree` for the converse when the coefficients are a perfect
+field. -/
 theorem Separable.squarefree {p : R[X]} (hsep : Separable p) : Squarefree p := by
   rw [multiplicity.squarefree_iff_multiplicity_le_one p]
   exact fun f => or_iff_not_imp_right.mpr fun hunit => multiplicity_le_one_of_separable hunit hsep

Mathlib/RingTheory/ChainOfDivisors.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anne Baanen, Paul Lezeau
 -/
 import Mathlib.Algebra.IsPrimePow
-import Mathlib.Algebra.Squarefree
+import Mathlib.Algebra.Squarefree.Basic
 import Mathlib.Order.Hom.Bounded
 import Mathlib.Algebra.GCDMonoid.Basic
 

Mathlib/RingTheory/Coprime/Basic.lean

@@ -98,12 +98,14 @@ theorem isCoprime_one_right : IsCoprime x 1 :=
   ⟨0, 1, by rw [one_mul, zero_mul, zero_add]⟩
 #align is_coprime_one_right isCoprime_one_right
 
+/-- See also `UniqueFactorizationMonoid.dvd_of_coprime_of_dvd_mul_right`. -/
 theorem IsCoprime.dvd_of_dvd_mul_right (H1 : IsCoprime x z) (H2 : x ∣ y * z) : x ∣ y := by
   let ⟨a, b, H⟩ := H1
   rw [← mul_one y, ← H, mul_add, ← mul_assoc, mul_left_comm]
   exact dvd_add (dvd_mul_left _ _) (H2.mul_left _)
 #align is_coprime.dvd_of_dvd_mul_right IsCoprime.dvd_of_dvd_mul_right
 
+/-- See also `UniqueFactorizationMonoid.dvd_of_coprime_of_dvd_mul_left`. -/
 theorem IsCoprime.dvd_of_dvd_mul_left (H1 : IsCoprime x y) (H2 : x ∣ y * z) : x ∣ z := by
   let ⟨a, b, H⟩ := H1
   rw [← one_mul z, ← H, add_mul, mul_right_comm, mul_assoc b]
@@ -127,6 +129,7 @@ theorem IsCoprime.mul_right (H1 : IsCoprime x y) (H2 : IsCoprime x z) : IsCoprim
   exact H1.mul_left H2
 #align is_coprime.mul_right IsCoprime.mul_right
 
+/-- See also `UniqueFactorizationMonoid.mul_dvd`. -/
 theorem IsCoprime.mul_dvd (H : IsCoprime x y) (H1 : x ∣ z) (H2 : y ∣ z) : x * y ∣ z := by
   obtain ⟨a, b, h⟩ := H
   rw [← mul_one z, ← h, mul_add]

Mathlib/RingTheory/UniqueFactorizationDomain.lean

@@ -197,6 +197,15 @@ theorem exists_prime_factors (a : α) :
   apply WfDvdMonoid.exists_factors a
 #align unique_factorization_monoid.exists_prime_factors UniqueFactorizationMonoid.exists_prime_factors
 
+lemma exists_prime_iff :
+    (∃ (p : α), Prime p) ↔ ∃ (x : α), x ≠ 0 ∧ ¬ IsUnit x := by
+  refine ⟨fun ⟨p, hp⟩ ↦ ⟨p, hp.ne_zero, hp.not_unit⟩, fun ⟨x, hx₀, hxu⟩ ↦ ?_⟩
+  obtain ⟨f, hf, hf'⟩ := exists_prime_factors x hx₀
+  rcases f.empty_or_exists_mem with rfl | h
+  · have := associated_one_iff_isUnit.mp hf'.symm; contradiction
+  · obtain ⟨p, hp⟩ := h
+    exact ⟨p, hf _ hp⟩
+
 @[elab_as_elim]
 theorem induction_on_prime {P : α → Prop} (a : α) (h₁ : P 0) (h₂ : ∀ x : α, IsUnit x → P x)
     (h₃ : ∀ a p : α, a ≠ 0 → Prime p → P a → P (p * a)) : P a := by
@@ -1212,6 +1221,45 @@ theorem multiplicative_of_coprime (f : α → β) (a b : α) (h0 : f 0 = 0)
 
 end Multiplicative
 
+section Coprime
+
+variable {x y d : R}
+
+/-- See also `IsCoprime.dvd_of_dvd_mul_left`. -/
+theorem dvd_of_coprime_of_dvd_mul_left
+    (h : ∀ p, p ∣ x → p ∣ y → IsUnit p) (h' : y ∣ x * d) : y ∣ d := by
+  rcases eq_or_ne x 0 with rfl | hx
+  · replace h : IsUnit y := h y (dvd_zero y) (refl _); exact h.dvd
+  rcases eq_or_ne y 0 with rfl | hy
+  · simp only [zero_dvd_iff, mul_eq_zero, hx, false_or] at h'; simp [h']
+  induction' y using UniqueFactorizationMonoid.induction_on_coprime
+    with u hu p k hp a b _ ha hb generalizing x d
+  · simpa [hx] using h'
+  · exact hu.dvd
+  · rcases eq_or_ne k 0 with rfl | hk; · simp
+    replace h : ¬ p ∣ x := fun contra ↦ hp.not_unit <| h p contra (dvd_pow_self p hk)
+    exact Prime.pow_dvd_of_dvd_mul_left hp k h h'
+  · rw [ne_eq, mul_eq_zero, not_or] at hy
+    have hxa : ∀ p, p ∣ x → p ∣ a → IsUnit p := fun p h₁ h₂ ↦ h p h₁ (h₂.mul_right b)
+    have hxb : ∀ p, p ∣ x → p ∣ b → IsUnit p := fun p h₁ h₂ ↦ h p h₁ (h₂.mul_left a)
+    obtain ⟨a', rfl⟩ := @ha x d hxa (dvd_of_mul_right_dvd h') hx hy.1
+    rw [mul_left_comm, mul_dvd_mul_iff_left hy.1] at h'
+    exact mul_dvd_mul_left a (@hb x a' hxb h' hx hy.2)
+
+/-- See also `IsCoprime.dvd_of_dvd_mul_right`. -/
+theorem dvd_of_coprime_of_dvd_mul_right
+    (h : ∀ p, p ∣ x → p ∣ y → IsUnit p) (h' : y ∣ d * x) : y ∣ d := by
+  rw [mul_comm] at h'; exact dvd_of_coprime_of_dvd_mul_left h h'
+
+/-- See also `IsCoprime.mul_dvd`. -/
+theorem mul_dvd_of_coprime (h : ∀ p, p ∣ x → p ∣ y → IsUnit p) (hx : x ∣ d) (hy : y ∣ d) :
+    x * y ∣ d := by
+  obtain ⟨x', rfl⟩ := hx
+  suffices y ∣ x' by exact mul_dvd_mul_left x this
+  exact dvd_of_coprime_of_dvd_mul_left h hy
+
+end Coprime
+
 end UniqueFactorizationMonoid
 
 namespace Associates

Mathlib/RingTheory/ZMod.lean

@@ -3,7 +3,7 @@ Copyright (c) 2022 Alex J. Best. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Alex J. Best
 -/
-import Mathlib.Algebra.Squarefree
+import Mathlib.Algebra.Squarefree.Basic
 import Mathlib.Data.ZMod.Basic
 import Mathlib.RingTheory.Int.Basic