feat(ring_theory/nilpotent): add lemma module.End.is_nilpotent_mapq (…

…#11831)

Together with the other lemmas necessary for its proof.

src/linear_algebra/basic.lean

@@ -633,6 +633,14 @@ rfl
 lemma comap_mono {f : M →ₛₗ[σ₁₂] M₂} {q q' : submodule R₂ M₂} :
   q ≤ q' → comap f q ≤ comap f q' := preimage_mono
 
+lemma le_comap_pow_of_le_comap (p : submodule R M) {f : M →ₗ[R] M} (h : p ≤ p.comap f) (k : ℕ) :
+  p ≤ p.comap (f^k) :=
+begin
+  induction k with k ih,
+  { simp [linear_map.one_eq_id], },
+  { simp [linear_map.iterate_succ, comap_comp, h.trans (comap_mono ih)], },
+end
+
 section
 variables [ring_hom_surjective σ₁₂]
 

src/linear_algebra/quotient.lean

@@ -264,6 +264,35 @@ p.liftq (q.mkq.comp f) $ by simpa [ker_comp] using h
 theorem mapq_mkq (f : M →ₛₗ[τ₁₂] M₂) {h} : (mapq p q f h).comp p.mkq = q.mkq.comp f :=
 by ext x; refl
 
+@[simp] lemma mapq_zero (h : p ≤ q.comap (0 : M →ₛₗ[τ₁₂] M₂) := by simp) :
+  p.mapq q (0 : M →ₛₗ[τ₁₂] M₂) h = 0 :=
+by { ext, simp, }
+
+/-- Given submodules `p ⊆ M`, `p₂ ⊆ M₂`, `p₃ ⊆ M₃` and maps `f : M → M₂`, `g : M₂ → M₃` inducing
+`mapq f : M ⧸ p → M₂ ⧸ p₂` and `mapq g : M₂ ⧸ p₂ → M₃ ⧸ p₃` then
+`mapq (g ∘ f) = (mapq g) ∘ (mapq f)`. -/
+lemma mapq_comp {R₃ M₃ : Type*} [ring R₃] [add_comm_group M₃] [module R₃ M₃]
+  (p₂ : submodule R₂ M₂) (p₃ : submodule R₃ M₃)
+  {τ₂₃ : R₂ →+* R₃} {τ₁₃ : R →+* R₃} [ring_hom_comp_triple τ₁₂ τ₂₃ τ₁₃]
+  (f : M →ₛₗ[τ₁₂] M₂) (g : M₂ →ₛₗ[τ₂₃] M₃) (hf : p ≤ p₂.comap f) (hg : p₂ ≤ p₃.comap g)
+  (h := (hf.trans (comap_mono hg))) :
+  p.mapq p₃ (g.comp f) h = (p₂.mapq p₃ g hg).comp (p.mapq p₂ f hf) :=
+by { ext, simp, }
+
+@[simp] lemma mapq_id (h : p ≤ p.comap linear_map.id := by simp) :
+  p.mapq p linear_map.id h = linear_map.id :=
+by { ext, simp, }
+
+lemma mapq_pow {f : M →ₗ[R] M} (h : p ≤ p.comap f) (k : ℕ)
+  (h' : p ≤ p.comap (f^k) := p.le_comap_pow_of_le_comap h k) :
+  p.mapq p (f^k) h' = (p.mapq p f h)^k :=
+begin
+  induction k with k ih,
+  { simp [linear_map.one_eq_id], },
+  { simp only [linear_map.iterate_succ, ← ih],
+    apply p.mapq_comp, },
+end
+
 theorem comap_liftq (f : M →ₛₗ[τ₁₂] M₂) (h) :
   q.comap (p.liftq f h) = (q.comap f).map (mkq p) :=
 le_antisymm

src/ring_theory/nilpotent.lean

@@ -180,3 +180,17 @@ begin
 end
 
 end algebra
+
+namespace module.End
+
+variables {M : Type v} [ring R] [add_comm_group M] [module R M]
+variables {f : module.End R M} {p : submodule R M} (hp : p ≤ p.comap f)
+
+lemma is_nilpotent.mapq (hnp : is_nilpotent f) : is_nilpotent (p.mapq p f hp) :=
+begin
+  obtain ⟨k, hk⟩ := hnp,
+  use k,
+  simp [← p.mapq_pow, hk],
+end
+
+end module.End