feat(ring_theory/noetherian): a surjective endomorphism of a noetheri…

…an module is injective (#7676)





Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/linear_algebra/basic.lean

@@ -290,7 +290,6 @@ begin
       ← linear_map.comp_assoc, h, linear_map.comp_assoc, linear_map.mul_eq_comp], },
 end
 
-
 lemma coe_pow (f : M →ₗ[R] M) (n : ℕ) : ⇑(f^n) = (f^[n]) :=
 by { ext m, apply pow_apply, }
 
@@ -320,6 +319,7 @@ begin
   rw [← nat.succ_pred_eq_of_pos (pos_iff_ne_zero.mpr hn), iterate_succ, coe_comp] at h,
   exact injective.of_comp h,
 end
+
 end
 
 section
@@ -1467,6 +1467,21 @@ by rw [range_eq_map, map_le_iff_le_comap, eq_top_iff]
 lemma map_le_range {f : M →ₗ[R] M₂} {p : submodule R M} : map f p ≤ range f :=
 set_like.coe_mono (set.image_subset_range f p)
 
+/--
+The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.
+-/
+@[simps]
+def iterate_range {R M} [ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) :
+  ℕ →ₘ order_dual (submodule R M) :=
+⟨λ n, (f ^ n).range, λ n m w x h, begin
+  obtain ⟨c, rfl⟩ := le_iff_exists_add.mp w,
+  rw linear_map.mem_range at h,
+  obtain ⟨m, rfl⟩ := h,
+  rw linear_map.mem_range,
+  use (f ^ c) m,
+  rw [pow_add, linear_map.mul_apply],
+end⟩
+
 /-- Restrict the codomain of a linear map `f` to `f.range`.
 
 This is the bundled version of `set.range_factorization`. -/
@@ -1510,7 +1525,6 @@ theorem disjoint_ker {f : M →ₗ[R] M₂} {p : submodule R M} :
   disjoint p (ker f) ↔ ∀ x ∈ p, f x = 0 → x = 0 :=
 by simp [disjoint_def]
 
-
 theorem ker_eq_bot' {f : M →ₗ[R] M₂} :
   ker f = ⊥ ↔ (∀ m, f m = 0 → m = 0) :=
 by simpa [disjoint] using @disjoint_ker _ _ _ _ _ _ _ _ f ⊤
@@ -1576,6 +1590,18 @@ begin
   simpa [disjoint]
 end
 
+/--
+The increasing sequence of submodules consisting of the kernels of the iterates of a linear map.
+-/
+@[simps]
+def iterate_ker {R M} [ring R] [add_comm_group M] [module R M] (f : M →ₗ[R] M) :
+  ℕ →ₘ submodule R M :=
+⟨λ n, (f ^ n).ker, λ n m w x h, begin
+  obtain ⟨c, rfl⟩ := le_iff_exists_add.mp w,
+  rw linear_map.mem_ker at h,
+  rw [linear_map.mem_ker, add_comm, pow_add, linear_map.mul_apply, h, linear_map.map_zero],
+end⟩
+
 end add_comm_monoid
 
 section add_comm_group

src/ring_theory/noetherian.lean

@@ -471,12 +471,58 @@ theorem set_has_maximal_iff_noetherian {R M} [ring R] [add_comm_group M] [module
   is_noetherian R M :=
 by rw [is_noetherian_iff_well_founded, well_founded.well_founded_iff_has_max']
 
+/-- A module is Noetherian iff every increasing chain of submodules stabilizes. -/
+theorem monotone_stabilizes_iff_noetherian {R M} [ring R] [add_comm_group M] [module R M] :
+  (∀ (f : ℕ →ₘ submodule R M), ∃ n, ∀ m, n ≤ m → f n = f m)
+    ↔ is_noetherian R M :=
+by rw [is_noetherian_iff_well_founded, well_founded.monotone_chain_condition]
+
 /-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/
 lemma is_noetherian.induction {R M} [ring R] [add_comm_group M] [module R M] [is_noetherian R M]
   {P : submodule R M → Prop} (hgt : ∀ I, (∀ J > I, P J) → P I)
   (I : submodule R M) : P I :=
 well_founded.recursion (well_founded_submodule_gt R M) I hgt
 
+/--
+For any endomorphism of a Noetherian module, there is some nontrivial iterate
+with disjoint kernel and range.
+-/
+theorem is_noetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot
+   {R M} [ring R] [add_comm_group M] [module R M] [I : is_noetherian R M]
+  (f : M →ₗ[R] M) : ∃ n : ℕ, n ≠ 0 ∧ (f ^ n).ker ⊓ (f ^ n).range = ⊥ :=
+begin
+  obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr I
+    (f.iterate_ker.comp ⟨λ n, n+1, λ n m w, by linarith⟩),
+  specialize w (2 * n + 1) (by linarith),
+  dsimp at w,
+  refine ⟨n+1, nat.succ_ne_zero _, _⟩,
+  rw eq_bot_iff,
+  rintros - ⟨h, ⟨y, rfl⟩⟩,
+  rw [mem_bot, ←linear_map.mem_ker, w],
+  erw linear_map.mem_ker at h ⊢,
+  change ((f ^ (n + 1)) * (f ^ (n + 1))) y = 0 at h,
+  rw ←pow_add at h,
+  convert h using 3,
+  linarith,
+end
+
+/-- Any surjective endomorphism of a Noetherian module is injective. -/
+theorem is_noetherian.injective_of_surjective_endomorphism
+  {R M} [ring R] [add_comm_group M] [module R M] [I : is_noetherian R M]
+  (f : M →ₗ[R] M) (s : surjective f) : injective f :=
+begin
+  obtain ⟨n, ne, w⟩ := is_noetherian.exists_endomorphism_iterate_ker_inf_range_eq_bot f,
+  rw [linear_map.range_eq_top.mpr (linear_map.iterate_surjective s n), inf_top_eq,
+    linear_map.ker_eq_bot] at w,
+  exact linear_map.injective_of_iterate_injective ne w,
+end
+
+/-- Any surjective endomorphism of a Noetherian module is bijective. -/
+theorem is_noetherian.bijective_of_surjective_endomorphism
+  {R M} [ring R] [add_comm_group M] [module R M] [I : is_noetherian R M]
+  (f : M →ₗ[R] M) (s : surjective f) : bijective f :=
+⟨is_noetherian.injective_of_surjective_endomorphism f s, s⟩
+
 /--
 A ring is Noetherian if it is Noetherian as a module over itself,
 i.e. all its ideals are finitely generated.