From 745cbfc611cd1f21f2b12f4180e602faa1f08bf2 Mon Sep 17 00:00:00 2001
From: Anne Baanen <vierkantor@vierkantor.com>
Date: Fri, 8 Oct 2021 14:22:16 +0000
Subject: [PATCH] =?UTF-8?q?feat(data/polynomial):=20%=E2=82=98=20as=20a=20?=
 =?UTF-8?q?linear=20map=20=20(#9532)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This PR bundles `(%ₘ) = polynomial.mod_by_monic` into a linear map. In a follow-up PR, I'll show this map descends to a linear map `adjoin_root q → polynomial R`, thereby (computably) assigning coefficients to each element in `adjoin_root q`.
---
 src/data/polynomial/ring_division.lean | 34 ++++++++++++++++++++++++++
 src/ring_theory/polynomial/basic.lean  | 14 +++++++++++
 2 files changed, 48 insertions(+)

diff --git a/src/data/polynomial/ring_division.lean b/src/data/polynomial/ring_division.lean
index de9547ad7be3a..a1c8fefcd571a 100644
--- a/src/data/polynomial/ring_division.lean
+++ b/src/data/polynomial/ring_division.lean
@@ -43,6 +43,40 @@ lemma aeval_mod_by_monic_eq_self_of_root [algebra R S]
   aeval x (p %ₘ q) = aeval x p :=
 eval₂_mod_by_monic_eq_self_of_root hq hx
 
+lemma mod_by_monic_eq_of_dvd_sub [nontrivial R] (hq : q.monic) {p₁ p₂ : polynomial R}
+  (h : q ∣ (p₁ - p₂)) :
+  p₁ %ₘ q = p₂ %ₘ q :=
+begin
+  obtain ⟨f, sub_eq⟩ := h,
+  refine (div_mod_by_monic_unique (p₂ /ₘ q + f) _ hq
+    ⟨_, degree_mod_by_monic_lt _ hq⟩).2,
+  rw [sub_eq_iff_eq_add.mp sub_eq, mul_add, ← add_assoc, mod_by_monic_add_div _ hq, add_comm]
+end
+
+lemma add_mod_by_monic [nontrivial R] (hq : q.monic)
+  (p₁ p₂ : polynomial R) : (p₁ + p₂) %ₘ q = p₁ %ₘ q + p₂ %ₘ q :=
+(div_mod_by_monic_unique (p₁ /ₘ q + p₂ /ₘ q) _ hq
+  ⟨by rw [mul_add, add_left_comm, add_assoc, mod_by_monic_add_div _ hq, ← add_assoc,
+          add_comm (q * _), mod_by_monic_add_div _ hq],
+    (degree_add_le _ _).trans_lt (max_lt (degree_mod_by_monic_lt _ hq)
+      (degree_mod_by_monic_lt _ hq))⟩).2
+
+lemma smul_mod_by_monic [nontrivial R] (hq : q.monic)
+  (c : R) (p : polynomial R) : (c • p) %ₘ q = c • (p %ₘ q) :=
+(div_mod_by_monic_unique (c • (p /ₘ q)) (c • (p %ₘ q)) hq
+  ⟨by rw [mul_smul_comm, ← smul_add, mod_by_monic_add_div p hq],
+   (degree_smul_le _ _).trans_lt (degree_mod_by_monic_lt _ hq)⟩).2
+
+/--
+`polynomial.mod_by_monic_hom (hq : monic (q : polynomial R))` is `_ %ₘ q` as a `R`-linear map.
+-/
+@[simps]
+def mod_by_monic_hom [nontrivial R] (hq : q.monic) :
+  polynomial R →ₗ[R] polynomial R :=
+{ to_fun := λ p, p %ₘ q,
+  map_add' := add_mod_by_monic hq,
+  map_smul' := smul_mod_by_monic hq }
+
 end comm_ring
 
 section no_zero_divisors
diff --git a/src/ring_theory/polynomial/basic.lean b/src/ring_theory/polynomial/basic.lean
index 91a811d61f52e..6efb2af4536ae 100644
--- a/src/ring_theory/polynomial/basic.lean
+++ b/src/ring_theory/polynomial/basic.lean
@@ -303,6 +303,20 @@ begin
   exact subtype.mem (coeff p n : T)
 end
 
+section mod_by_monic
+
+variables {q : polynomial R}
+
+lemma mem_ker_mod_by_monic [nontrivial R] (hq : q.monic) {p : polynomial R} :
+  p ∈ (mod_by_monic_hom hq).ker ↔ q ∣ p :=
+linear_map.mem_ker.trans (dvd_iff_mod_by_monic_eq_zero hq)
+
+@[simp] lemma ker_mod_by_monic_hom [nontrivial R] (hq : q.monic) :
+  (polynomial.mod_by_monic_hom hq).ker = (ideal.span {q}).restrict_scalars R :=
+submodule.ext (λ f, (mem_ker_mod_by_monic hq).trans ideal.mem_span_singleton.symm)
+
+end mod_by_monic
+
 end polynomial
 
 variables {R : Type u} {σ : Type v} {M : Type w} [comm_ring R] [add_comm_group M] [module R M]