feat(ring_theory/polynomial): decomposing the kernel of an endomorphism polynomial (#4174)

Author: abentkamp

src/algebra/ring/basic.lean

@@ -260,6 +260,13 @@ theorem coe_monoid_hom_injective : function.injective (coe : (α →+* β) → (
 /-- Ring homomorphisms preserve multiplication. -/
 @[simp] lemma map_mul (f : α →+* β) (a b : α) : f (a * b) = f a * f b := f.map_mul' a b
 
+/-- Ring homomorphisms preserve `bit0`. -/
+@[simp] lemma map_bit0 (f : α →+* β) (a : α) : f (bit0 a) = bit0 (f a) := map_add _ _ _
+
+/-- Ring homomorphisms preserve `bit1`. -/
+@[simp] lemma map_bit1 (f : α →+* β) (a : α) : f (bit1 a) = bit1 (f a) :=
+by simp [bit1]
+
 /-- `f : R →+* S` has a trivial codomain iff `f 1 = 0`. -/
 lemma codomain_trivial_iff_map_one_eq_zero : (0 : β) = 1 ↔ f 1 = 0 :=
 by rw [map_one, eq_comm]

src/data/polynomial/algebra_map.lean

@@ -95,7 +95,7 @@ end comp
 end comm_semiring
 
 section aeval
-variables [comm_semiring R] {p : polynomial R}
+variables [comm_semiring R] {p q : polynomial R}
 
 variables [semiring A] [algebra R A]
 variables {B : Type*} [semiring B] [algebra R B]
@@ -111,10 +111,37 @@ variables {R A}
 
 theorem aeval_def (p : polynomial R) : aeval x p = eval₂ (algebra_map R A) x p := rfl
 
+@[simp] lemma aeval_zero : aeval x (0 : polynomial R) = 0 :=
+alg_hom.map_zero (aeval x)
+
 @[simp] lemma aeval_X : aeval x (X : polynomial R) = x := eval₂_X _ x
 
 @[simp] lemma aeval_C (r : R) : aeval x (C r) = algebra_map R A r := eval₂_C _ x
 
+lemma aeval_monomial {n : ℕ} {r : R} : aeval x (monomial n r) = (algebra_map _ _ r) * x^n :=
+eval₂_monomial _ _
+
+@[simp] lemma aeval_X_pow {n : ℕ} : aeval x ((X : polynomial R)^n) = x^n :=
+eval₂_X_pow _ _
+
+@[simp] lemma aeval_add : aeval x (p + q) = aeval x p + aeval x q :=
+alg_hom.map_add _ _ _
+
+@[simp] lemma aeval_one : aeval x (1 : polynomial R) = 1 :=
+alg_hom.map_one _
+
+@[simp] lemma aeval_bit0 : aeval x (bit0 p) = bit0 (aeval x p) :=
+alg_hom.map_bit0 _ _
+
+@[simp] lemma aeval_bit1 : aeval x (bit1 p) = bit1 (aeval x p) :=
+alg_hom.map_bit1 _ _
+
+@[simp] lemma aeval_nat_cast (n : ℕ) : aeval x (n : polynomial R) = n :=
+alg_hom.map_nat_cast _ _
+
+lemma aeval_mul : aeval x (p * q) = aeval x p * aeval x q :=
+alg_hom.map_mul _ _ _
+
 theorem eval_unique (φ : polynomial R →ₐ[R] A) (p) :
   φ p = eval₂ (algebra_map R A) (φ X) p :=
 begin
@@ -221,6 +248,9 @@ lemma aeval_endomorphism {M : Type*}
   [comm_ring R] [add_comm_group M] [module R M]
   (f : M →ₗ[R] M) (v : M) (p : polynomial R) :
   aeval f p v = p.sum (λ n b, b • (f ^ n) v) :=
-eval₂_endomorphism_algebra_map f v p
+begin
+  rw [aeval_def, eval₂],
+  exact (finset.sum_hom p.support (λ h : M →ₗ[R] M, h v)).symm
+end
 
 end polynomial

src/data/polynomial/eval.lean

@@ -580,15 +580,6 @@ by apply is_ring_hom.of_semiring
 
 instance eval.is_ring_hom {x : R} : is_ring_hom (eval x) := eval₂.is_ring_hom _
 
-lemma eval₂_endomorphism_algebra_map {M : Type w}
-  [add_comm_group M] [module R M]
-  (f : M →ₗ[R] M) (v : M) (p : polynomial R) :
-  p.eval₂ (algebra_map R (M →ₗ[R] M)) f v = p.sum (λ n b, b • (f ^ n) v) :=
-begin
-  dunfold polynomial.eval₂ finsupp.sum,
-  exact (finset.sum_hom p.support (λ h : M →ₗ[R] M, h v)).symm
-end
-
 end comm_ring
 
 end polynomial

src/linear_algebra/basic.lean

@@ -388,10 +388,14 @@ end comm_semiring
 
 section ring
 
-instance endomorphism_ring [ring R] [add_comm_group M] [semimodule R M] : ring (M →ₗ[R] M) :=
+variables [ring R] [add_comm_group M] [semimodule R M]
+
+instance endomorphism_ring : ring (M →ₗ[R] M) :=
 by refine {mul := (*), one := 1, ..linear_map.add_comm_group, ..};
   { intros, apply linear_map.ext, simp {proj := ff} }
 
+@[simp] lemma mul_apply (f g : M →ₗ[R] M) (x : M) : (f * g) x = f (g x) := rfl
+
 end ring
 
 section comm_ring

src/ring_theory/algebra.lean

@@ -431,6 +431,12 @@ lemma map_sum {ι : Type*} (f : ι → A) (s : finset ι) :
 @[simp] lemma map_nat_cast (n : ℕ) : φ n = n :=
 φ.to_ring_hom.map_nat_cast n
 
+@[simp] lemma map_bit0 (x) : φ (bit0 x) = bit0 (φ x) :=
+φ.to_ring_hom.map_bit0 x
+
+@[simp] lemma map_bit1 (x) : φ (bit1 x) = bit1 (φ x) :=
+φ.to_ring_hom.map_bit1 x
+
 section
 
 variables (R A)

src/ring_theory/polynomial/basic.lean

@@ -429,13 +429,77 @@ exists_irreducible_of_nat_degree_pos $ nat.pos_of_ne_zero hf
 lemma linear_independent_powers_iff_eval₂
   (f : M →ₗ[R] M) (v : M) :
   linear_independent R (λ n : ℕ, (f ^ n) v)
-    ↔ ∀ (p : polynomial R), polynomial.aeval f p v = 0 → p = 0 :=
+    ↔ ∀ (p : polynomial R), aeval f p v = 0 → p = 0 :=
 begin
   rw linear_independent_iff,
   simp only [finsupp.total_apply, aeval_endomorphism],
   refl
 end
 
+lemma disjoint_ker_aeval_of_coprime
+  (f : M →ₗ[R] M) {p q : polynomial R} (hpq : is_coprime p q) :
+  disjoint (aeval f p).ker (aeval f q).ker :=
+begin
+  intros v hv,
+  rcases hpq with ⟨p', q', hpq'⟩,
+  simpa [linear_map.mem_ker.1 (submodule.mem_inf.1 hv).1,
+         linear_map.mem_ker.1 (submodule.mem_inf.1 hv).2]
+    using congr_arg (λ p : polynomial R, aeval f p v) hpq'.symm,
+end
+
+lemma sup_aeval_range_eq_top_of_coprime
+  (f : M →ₗ[R] M) {p q : polynomial R} (hpq : is_coprime p q) :
+  (aeval f p).range ⊔ (aeval f q).range = ⊤ :=
+begin
+  rw eq_top_iff,
+  intros v hv,
+  rw submodule.mem_sup,
+  rcases hpq with ⟨p', q', hpq'⟩,
+  use aeval f (p * p') v,
+  use linear_map.mem_range.2 ⟨aeval f p' v, by simp only [linear_map.mul_app, aeval_mul]⟩,
+  use aeval f (q * q') v,
+  use linear_map.mem_range.2 ⟨aeval f q' v, by simp only [linear_map.mul_app, aeval_mul]⟩,
+  simpa only [mul_comm p p', mul_comm q q', aeval_one, aeval_add]
+    using congr_arg (λ p : polynomial R, aeval f p v) hpq'
+end
+
+lemma sup_ker_aeval_le_ker_aeval_mul {f : M →ₗ[R] M} {p q : polynomial R} :
+  (aeval f p).ker ⊔ (aeval f q).ker ≤ (aeval f (p * q)).ker :=
+begin
+  intros v hv,
+  rcases submodule.mem_sup.1 hv with ⟨x, hx, y, hy, hxy⟩,
+  have h_eval_x : aeval f (p * q) x = 0,
+  { rw [mul_comm, aeval_mul, linear_map.mul_apply, linear_map.mem_ker.1 hx, linear_map.map_zero] },
+  have h_eval_y : aeval f (p * q) y = 0,
+  { rw [aeval_mul, linear_map.mul_apply, linear_map.mem_ker.1 hy, linear_map.map_zero] },
+  rw [linear_map.mem_ker, ←hxy, linear_map.map_add, h_eval_x, h_eval_y, add_zero],
+end
+
+lemma sup_ker_aeval_eq_ker_aeval_mul_of_coprime
+  (f : M →ₗ[R] M) {p q : polynomial R} (hpq : is_coprime p q) :
+  (aeval f p).ker ⊔ (aeval f q).ker = (aeval f (p * q)).ker :=
+begin
+  apply le_antisymm sup_ker_aeval_le_ker_aeval_mul,
+  intros v hv,
+  rw submodule.mem_sup,
+  rcases hpq with ⟨p', q', hpq'⟩,
+  have h_eval₂_qpp' := calc
+    aeval f (q * (p * p')) v = aeval f (p' * (p * q)) v :
+      by rw [mul_comm, mul_assoc, mul_comm, mul_assoc, mul_comm q p]
+    ... = 0 :
+      by rw [aeval_mul, linear_map.mul_apply, linear_map.mem_ker.1 hv, linear_map.map_zero],
+  have h_eval₂_pqq' := calc
+    aeval f (p * (q * q')) v = aeval f (q' * (p * q)) v :
+      by rw [←mul_assoc, mul_comm]
+    ... = 0 :
+      by rw [aeval_mul, linear_map.mul_apply, linear_map.mem_ker.1 hv, linear_map.map_zero],
+  rw aeval_mul at h_eval₂_qpp' h_eval₂_pqq',
+  refine ⟨aeval f (q * q') v, linear_map.mem_ker.1 h_eval₂_pqq',
+          aeval f (p * p') v, linear_map.mem_ker.1 h_eval₂_qpp', _⟩,
+  rw [add_comm, mul_comm p p', mul_comm q q'],
+  simpa using congr_arg (λ p : polynomial R, aeval f p v) hpq'
+end
+
 end polynomial
 
 namespace mv_polynomial