feat(ring_theory/noetherian): Finitely generated idempotent ideal is …

…principal. (#15561)

src/algebra/ring/idempotents.lean

@@ -27,7 +27,7 @@ projection, idempotent
 
 variables {M N S M₀ M₁ R G G₀ : Type*}
 variables [has_mul M] [monoid N] [semigroup S] [mul_zero_class M₀] [mul_one_class M₁]
-  [non_assoc_ring R] [group G] [group_with_zero G₀]
+  [non_assoc_ring R] [group G] [cancel_monoid_with_zero G₀]
 
 /--
 An element `p` is said to be idempotent if `p * p = p`
@@ -70,8 +70,7 @@ begin
   refine iff.intro
     (λ h, or_iff_not_imp_left.mpr (λ hp, _))
     (λ h, h.elim (λ hp, hp.symm ▸ zero) (λ hp, hp.symm ▸ one)),
-  lift p to G₀ˣ using is_unit.mk0 _ hp,
-  exact_mod_cast iff_eq_one.mp (by exact_mod_cast h.eq),
+  exact mul_left_cancel₀ hp (h.trans (mul_one p).symm)
 end
 
 /-! ### Instances on `subtype is_idempotent_elem` -/

src/ring_theory/noetherian.lean

@@ -10,6 +10,7 @@ import order.order_iso_nat
 import ring_theory.ideal.operations
 import order.compactly_generated
 import linear_algebra.linear_independent
+import algebra.ring.idempotents
 
 /-!
 # Noetherian rings and modules
@@ -135,6 +136,15 @@ begin
     exact add_mem (smul_mem _ _ hci) (smul_mem _ _ hz) }
 end
 
+theorem exists_mem_and_smul_eq_self_of_fg_of_le_smul {R : Type*} [comm_ring R]
+  {M : Type*} [add_comm_group M] [module R M]
+  (I : ideal R) (N : submodule R M) (hn : N.fg) (hin : N ≤ I • N) :
+  ∃ r ∈ I, ∀ n ∈ N, r • n = n :=
+begin
+  obtain ⟨r, hr, hr'⟩ := N.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I hn hin,
+  exact ⟨-(r-1), I.neg_mem hr, λ n hn, by simpa [sub_smul] using hr' n hn⟩,
+end
+
 theorem fg_bot : (⊥ : submodule R M).fg :=
 ⟨∅, by rw [finset.coe_empty, span_empty]⟩
 
@@ -282,23 +292,6 @@ begin
   { rw [finset.coe_insert, submodule.span_insert], apply h₂; apply_assumption }
 end
 
-/-- An ideal of `R` is finitely generated if it is the span of a finite subset of `R`.
-
-This is defeq to `submodule.fg`, but unfolds more nicely. -/
-def _root_.ideal.fg (I : ideal R) : Prop := ∃ S : finset R, ideal.span ↑S = I
-
-/-- The image of a finitely generated ideal is finitely generated.
-
-This is the `ideal` version of `submodule.fg.map`. -/
-lemma _root_.ideal.fg.map {R S : Type*} [semiring R] [semiring S] {I : ideal R} (h : I.fg)
-  (f : R →+* S) : (I.map f).fg :=
-begin
-  classical,
-  obtain ⟨s, hs⟩ := h,
-  refine ⟨s.image f, _⟩,
-  rw [finset.coe_image, ←ideal.map_span, hs],
-end
-
 /-- The kernel of the composition of two linear maps is finitely generated if both kernels are and
 the first morphism is surjective. -/
 lemma fg_ker_comp {R M N P : Type*} [ring R] [add_comm_group M] [module R M]
@@ -321,19 +314,6 @@ begin
   exact submodule.span_eq_restrict_scalars R S M X h
 end
 
-lemma _root_.ideal.fg_ker_comp {R S A : Type*} [comm_ring R] [comm_ring S] [comm_ring A]
-  (f : R →+* S) (g : S →+* A) (hf : f.ker.fg) (hg : g.ker.fg) (hsur : function.surjective f) :
-  (g.comp f).ker.fg :=
-begin
-  letI : algebra R S := ring_hom.to_algebra f,
-  letI : algebra R A := ring_hom.to_algebra (g.comp f),
-  letI : algebra S A := ring_hom.to_algebra g,
-  letI : is_scalar_tower R S A := is_scalar_tower.of_algebra_map_eq (λ _, rfl),
-  let f₁ := algebra.linear_map R S,
-  let g₁ := (is_scalar_tower.to_alg_hom R S A).to_linear_map,
-  exact fg_ker_comp f₁ g₁ hf (fg_restrict_scalars g.ker hg hsur) hsur
-end
-
 /-- Finitely generated submodules are precisely compact elements in the submodule lattice. -/
 theorem fg_iff_compact (s : submodule R M) : s.fg ↔ complete_lattice.is_compact_element s :=
 begin
@@ -364,6 +344,74 @@ end
 
 end submodule
 
+namespace ideal
+
+variables {R : Type*} {M : Type*} [semiring R] [add_comm_monoid M] [module R M]
+
+/-- An ideal of `R` is finitely generated if it is the span of a finite subset of `R`.
+
+This is defeq to `submodule.fg`, but unfolds more nicely. -/
+def fg (I : ideal R) : Prop := ∃ S : finset R, ideal.span ↑S = I
+
+/-- The image of a finitely generated ideal is finitely generated.
+
+This is the `ideal` version of `submodule.fg.map`. -/
+lemma fg.map {R S : Type*} [semiring R] [semiring S] {I : ideal R} (h : I.fg)
+  (f : R →+* S) : (I.map f).fg :=
+begin
+  classical,
+  obtain ⟨s, hs⟩ := h,
+  refine ⟨s.image f, _⟩,
+  rw [finset.coe_image, ←ideal.map_span, hs],
+end
+
+lemma fg_ker_comp {R S A : Type*} [comm_ring R] [comm_ring S] [comm_ring A]
+  (f : R →+* S) (g : S →+* A) (hf : f.ker.fg) (hg : g.ker.fg) (hsur : function.surjective f) :
+  (g.comp f).ker.fg :=
+begin
+  letI : algebra R S := ring_hom.to_algebra f,
+  letI : algebra R A := ring_hom.to_algebra (g.comp f),
+  letI : algebra S A := ring_hom.to_algebra g,
+  letI : is_scalar_tower R S A := is_scalar_tower.of_algebra_map_eq (λ _, rfl),
+  let f₁ := algebra.linear_map R S,
+  let g₁ := (is_scalar_tower.to_alg_hom R S A).to_linear_map,
+  exact submodule.fg_ker_comp f₁ g₁ hf (submodule.fg_restrict_scalars g.ker hg hsur) hsur
+end
+
+/-- A finitely generated idempotent ideal is generated by an idempotent element -/
+lemma is_idempotent_elem_iff_of_fg {R : Type*} [comm_ring R] (I : ideal R)
+  (h : I.fg) :
+  is_idempotent_elem I ↔ ∃ e : R, is_idempotent_elem e ∧ I = R ∙ e :=
+begin
+  split,
+  { intro e,
+    obtain ⟨r, hr, hr'⟩ := submodule.exists_mem_and_smul_eq_self_of_fg_of_le_smul I I h
+      (by { rw [smul_eq_mul], exact e.ge }),
+    simp_rw smul_eq_mul at hr',
+    refine ⟨r, hr' r hr, antisymm _ ((submodule.span_singleton_le_iff_mem _ _).mpr hr)⟩,
+    intros x hx,
+    rw ← hr' x hx,
+    exact ideal.mem_span_singleton'.mpr ⟨_, mul_comm _ _⟩ },
+  { rintros ⟨e, he, rfl⟩,
+    simp [is_idempotent_elem, ideal.span_singleton_mul_span_singleton, he.eq] }
+end
+
+lemma is_idempotent_elem_iff_eq_bot_or_top {R : Type*} [comm_ring R] [is_domain R]
+  (I : ideal R) (h : I.fg) :
+  is_idempotent_elem I ↔ I = ⊥ ∨ I = ⊤ :=
+begin
+  split,
+  { intro H,
+    obtain ⟨e, he, rfl⟩ := (I.is_idempotent_elem_iff_of_fg h).mp H,
+    simp only [ideal.submodule_span_eq, ideal.span_singleton_eq_bot],
+    apply or_of_or_of_imp_of_imp (is_idempotent_elem.iff_eq_zero_or_one.mp he) id,
+    rintro rfl,
+    simp },
+  { rintro (rfl|rfl); simp [is_idempotent_elem] }
+end
+
+end ideal
+
 /--
 `is_noetherian R M` is the proposition that `M` is a Noetherian `R`-module,
 implemented as the predicate that all `R`-submodules of `M` are finitely generated.