feat(field_theory/separable): definition and basic properties (#3155)

src/field_theory/separable.lean

@@ -0,0 +1,71 @@
+/-
+Copyright (c) 2020 Kenny Lau. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kenny Lau.
+-/
+
+import ring_theory.polynomial
+
+/-!
+
+# Separable polynomials
+
+We define a polynomial to be separable if it is coprime with its derivative. We prove basic
+properties about separable polynomials here.
+
+-/
+
+universes u v w
+open_locale classical
+
+namespace polynomial
+
+section comm_semiring
+
+variables {R : Type u} [comm_semiring R]
+
+/-- A polynomial is separable iff it is coprime with its derivative. -/
+def separable (f : polynomial R) : Prop :=
+is_coprime f f.derivative
+
+lemma separable_def (f : polynomial R) :
+  f.separable ↔ is_coprime f f.derivative :=
+iff.rfl
+
+lemma separable_def' (f : polynomial R) :
+  f.separable ↔ ∃ a b : polynomial R, a * f + b * f.derivative = 1 :=
+iff.rfl
+
+lemma separable_one : (1 : polynomial R).separable :=
+is_coprime_one_left
+
+lemma separable_X_add_C (a : R) : (X + C a).separable :=
+by { rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero],
+  exact is_coprime_one_right }
+
+lemma separable_X : (X : polynomial R).separable :=
+by { rw [separable_def, derivative_X], exact is_coprime_one_right }
+
+lemma separable.of_mul_left {f g : polynomial R} (h : (f * g).separable) : f.separable :=
+begin
+  have := h.of_mul_left_left, rw derivative_mul at this,
+  exact is_coprime.of_mul_right_left (is_coprime.of_add_mul_left_right this)
+end
+
+lemma separable.of_mul_right {f g : polynomial R} (h : (f * g).separable) : g.separable :=
+by { rw mul_comm at h, exact h.of_mul_left }
+
+end comm_semiring
+
+section comm_ring
+
+variables {R : Type u} [comm_ring R]
+
+lemma separable.mul {f g : polynomial R} (hf : f.separable) (hg : g.separable)
+  (h : is_coprime f g) : (f * g).separable :=
+by { rw [separable_def, derivative_mul], exact ((hf.mul_right h).add_mul_left_right _).mul_left
+  ((h.symm.mul_right hg).mul_add_right_right _) }
+
+end comm_ring
+
+end polynomial

src/ring_theory/coprime.lean

@@ -24,6 +24,8 @@ open_locale classical big_operators
 
 universes u v
 
+section comm_semiring
+
 variables {R : Type u} [comm_semiring R] (x y z : R)
 
 /-- The proposition that `x` and `y` are coprime, defined to be the existence of `a` and `b` such
@@ -162,3 +164,91 @@ show is_coprime x (x * k), from hk ▸ H
 theorem is_coprime.map (H : is_coprime x y) {S : Type v} [comm_semiring S] (f : R →+* S) :
   is_coprime (f x) (f y) :=
 let ⟨a, b, h⟩ := H in ⟨f a, f b, by rw [← f.map_mul, ← f.map_mul, ← f.map_add, h, f.map_one]⟩
+
+variables {x y z}
+
+lemma is_coprime.of_add_mul_left_left (h : is_coprime (x + y * z) y) : is_coprime x y :=
+let ⟨a, b, H⟩ := h in ⟨a, a * z + b, by simpa only [add_mul, mul_add,
+    add_assoc, add_comm, add_left_comm, mul_assoc, mul_comm, mul_left_comm] using H⟩
+
+lemma is_coprime.of_add_mul_right_left (h : is_coprime (x + z * y) y) : is_coprime x y :=
+by { rw mul_comm at h, exact h.of_add_mul_left_left }
+
+lemma is_coprime.of_add_mul_left_right (h : is_coprime x (y + x * z)) : is_coprime x y :=
+by { rw is_coprime_comm at h ⊢, exact h.of_add_mul_left_left }
+
+lemma is_coprime.of_add_mul_right_right (h : is_coprime x (y + z * x)) : is_coprime x y :=
+by { rw mul_comm at h, exact h.of_add_mul_left_right }
+
+lemma is_coprime.of_mul_add_left_left (h : is_coprime (y * z + x) y) : is_coprime x y :=
+by { rw add_comm at h, exact h.of_add_mul_left_left }
+
+lemma is_coprime.of_mul_add_right_left (h : is_coprime (z * y + x) y) : is_coprime x y :=
+by { rw add_comm at h, exact h.of_add_mul_right_left }
+
+lemma is_coprime.of_mul_add_left_right (h : is_coprime x (x * z + y)) : is_coprime x y :=
+by { rw add_comm at h, exact h.of_add_mul_left_right }
+
+lemma is_coprime.of_mul_add_right_right (h : is_coprime x (z * x + y)) : is_coprime x y :=
+by { rw add_comm at h, exact h.of_add_mul_right_right }
+
+end comm_semiring
+
+namespace is_coprime
+
+section comm_ring
+
+variables {R : Type u} [comm_ring R]
+
+lemma add_mul_left_left {x y : R} (h : is_coprime x y) (z : R) : is_coprime (x + y * z) y :=
+@of_add_mul_left_left R _ _ _ (-z) $
+by simpa only [mul_neg_eq_neg_mul_symm, add_neg_cancel_right] using h
+
+lemma add_mul_right_left {x y : R} (h : is_coprime x y) (z : R) : is_coprime (x + z * y) y :=
+by { rw mul_comm, exact h.add_mul_left_left z }
+
+lemma add_mul_left_right {x y : R} (h : is_coprime x y) (z : R) : is_coprime x (y + x * z) :=
+by { rw is_coprime_comm, exact h.symm.add_mul_left_left z }
+
+lemma add_mul_right_right {x y : R} (h : is_coprime x y) (z : R) : is_coprime x (y + z * x) :=
+by { rw is_coprime_comm, exact h.symm.add_mul_right_left z }
+
+lemma mul_add_left_left {x y : R} (h : is_coprime x y) (z : R) : is_coprime (y * z + x) y :=
+by { rw add_comm, exact h.add_mul_left_left z }
+
+lemma mul_add_right_left {x y : R} (h : is_coprime x y) (z : R) : is_coprime (z * y + x) y :=
+by { rw add_comm, exact h.add_mul_right_left z }
+
+lemma mul_add_left_right {x y : R} (h : is_coprime x y) (z : R) : is_coprime x (x * z + y) :=
+by { rw add_comm, exact h.add_mul_left_right z }
+
+lemma mul_add_right_right {x y : R} (h : is_coprime x y) (z : R) : is_coprime x (z * x + y) :=
+by { rw add_comm, exact h.add_mul_right_right z }
+
+lemma add_mul_left_left_iff {x y z : R} : is_coprime (x + y * z) y ↔ is_coprime x y :=
+⟨of_add_mul_left_left, λ h, h.add_mul_left_left z⟩
+
+lemma add_mul_right_left_iff {x y z : R} : is_coprime (x + z * y) y ↔ is_coprime x y :=
+⟨of_add_mul_right_left, λ h, h.add_mul_right_left z⟩
+
+lemma add_mul_left_right_iff {x y z : R} : is_coprime x (y + x * z) ↔ is_coprime x y :=
+⟨of_add_mul_left_right, λ h, h.add_mul_left_right z⟩
+
+lemma add_mul_right_right_iff {x y z : R} : is_coprime x (y + z * x) ↔ is_coprime x y :=
+⟨of_add_mul_right_right, λ h, h.add_mul_right_right z⟩
+
+lemma mul_add_left_left_iff {x y z : R} : is_coprime (y * z + x) y ↔ is_coprime x y :=
+⟨of_mul_add_left_left, λ h, h.mul_add_left_left z⟩
+
+lemma mul_add_right_left_iff {x y z : R} : is_coprime (z * y + x) y ↔ is_coprime x y :=
+⟨of_mul_add_right_left, λ h, h.mul_add_right_left z⟩
+
+lemma mul_add_left_right_iff {x y z : R} : is_coprime x (x * z + y) ↔ is_coprime x y :=
+⟨of_mul_add_left_right, λ h, h.mul_add_left_right z⟩
+
+lemma mul_add_right_right_iff {x y z : R} : is_coprime x (z * x + y) ↔ is_coprime x y :=
+⟨of_mul_add_right_right, λ h, h.mul_add_right_right z⟩
+
+end comm_ring
+
+end is_coprime