Mathlib.RingTheory.Noetherian.Basic

isNoetherian_of_surjective theorem

(f : M →ₗ[R] P) (hf : LinearMap.range f = ⊤) [IsNoetherian R M] : IsNoetherian R P

Full source

theorem isNoetherian_of_surjective (f : M →ₗ[R] P) (hf : LinearMap.range f = ⊤) [IsNoetherian R M] :
    IsNoetherian R P :=
  ⟨fun s =>
    have : (s.comap f).map f = s := Submodule.map_comap_eq_self <| hf.symm ▸ le_top
    this ▸ (noetherian _).map _⟩

Noetherian Property Preserved under Surjective Linear Maps

Informal description

Let $R$ be a ring, and let $M$ and $P$ be $R$-modules. Given a surjective $R$-linear map $f \colon M \to P$ (i.e., $\operatorname{range}(f) = P$) and assuming $M$ is a Noetherian $R$-module, then $P$ is also a Noetherian $R$-module.

isNoetherian_range instance

(f : M →ₗ[R] P) [IsNoetherian R M] : IsNoetherian R (LinearMap.range f)

Full source

instance isNoetherian_range (f : M →ₗ[R] P) [IsNoetherian R M] :
    IsNoetherian R (LinearMap.range f) :=
  isNoetherian_of_surjective _ _ f.range_rangeRestrict

Noetherian Property of the Range of a Linear Map

Informal description

For any ring $R$ and $R$-modules $M$ and $P$, if $M$ is a Noetherian $R$-module and $f \colon M \to P$ is an $R$-linear map, then the range of $f$ is also a Noetherian $R$-module.

isNoetherian_quotient instance

 {A M : Type*} [Ring A] [AddCommGroup M] [SMul R A] [Module R M] [Module A M] [IsScalarTower R A M] (N : Submodule A M)
  [IsNoetherian R M] : IsNoetherian R (M ⧸ N)

Full source

instance isNoetherian_quotient {A M : Type*} [Ring A] [AddCommGroup M] [SMul R A] [Module R M]
    [Module A M] [IsScalarTower R A M] (N : Submodule A M) [IsNoetherian R M] :
    IsNoetherian R (M ⧸ N) :=
  isNoetherian_of_surjective M ((Submodule.mkQ N).restrictScalars R) <|
    LinearMap.range_eq_top.mpr N.mkQ_surjective

Noetherian Property of Quotient Modules

Informal description

Let $R$ be a ring, $A$ be another ring with a scalar multiplication by $R$, and $M$ be a module over both $R$ and $A$ such that the actions are compatible via the scalar tower condition. For any submodule $N$ of $M$ as an $A$-module, if $M$ is a Noetherian $R$-module, then the quotient module $M ⧸ N$ is also a Noetherian $R$-module.

isNoetherian_of_linearEquiv theorem

(f : M ≃ₗ[R] P) [IsNoetherian R M] : IsNoetherian R P

Full source

theorem isNoetherian_of_linearEquiv (f : M ≃ₗ[R] P) [IsNoetherian R M] : IsNoetherian R P :=
  isNoetherian_of_surjective _ f.toLinearMap f.range

Noetherian Property Preserved under Linear Equivalence

Informal description

Let $R$ be a ring, and let $M$ and $P$ be $R$-modules. Given a linear equivalence $f \colon M \simeq P$ (i.e., a bijective $R$-linear map) and assuming $M$ is a Noetherian $R$-module, then $P$ is also a Noetherian $R$-module.

LinearEquiv.isNoetherian_iff theorem

(f : M ≃ₗ[R] P) : IsNoetherian R M ↔ IsNoetherian R P

Full source

theorem LinearEquiv.isNoetherian_iff (f : M ≃ₗ[R] P) : IsNoetherianIsNoetherian R M ↔ IsNoetherian R P :=
  ⟨fun _ ↦ isNoetherian_of_linearEquiv f, fun _ ↦ isNoetherian_of_linearEquiv f.symm⟩

Noetherian Property is Preserved under Linear Equivalence

Informal description

Let $R$ be a ring, and let $M$ and $P$ be $R$-modules. Given a linear equivalence $f \colon M \simeq P$ (i.e., a bijective $R$-linear map), the module $M$ is Noetherian if and only if $P$ is Noetherian.

isNoetherian_top_iff theorem

: IsNoetherian R (⊤ : Submodule R M) ↔ IsNoetherian R M

Full source

theorem isNoetherian_top_iff : IsNoetherianIsNoetherian R (⊤ : Submodule R M) ↔ IsNoetherian R M :=
  Submodule.topEquiv.isNoetherian_iff

Noetherian Property of Module and its Top Submodule

Informal description

For a ring $R$ and an $R$-module $M$, the top submodule $\top$ (i.e., $M$ itself) is Noetherian if and only if $M$ is Noetherian.

isNoetherian_of_injective theorem

[IsNoetherian R P] (f : M →ₗ[R] P) (hf : Function.Injective f) : IsNoetherian R M

Full source

theorem isNoetherian_of_injective [IsNoetherian R P] (f : M →ₗ[R] P) (hf : Function.Injective f) :
    IsNoetherian R M :=
  isNoetherian_of_linearEquiv (LinearEquiv.ofInjective f hf).symm

Noetherian Property via Injective Linear Map

Informal description

Let $R$ be a ring, and let $M$ and $P$ be $R$-modules. If $P$ is a Noetherian $R$-module and there exists an injective $R$-linear map $f \colon M \to P$, then $M$ is also a Noetherian $R$-module.

fg_of_injective theorem

[IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P) (hf : Function.Injective f) : N.FG

Full source

theorem fg_of_injective [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P)
    (hf : Function.Injective f) : N.FG :=
  haveI := isNoetherian_of_injective f hf
  IsNoetherian.noetherian N

Finitely Generated Submodules via Injective Maps from Noetherian Modules

Informal description

Let $R$ be a ring, $M$ and $P$ be $R$-modules with $P$ Noetherian, and $N$ be a submodule of $M$. If there exists an injective $R$-linear map $f \colon M \to P$, then $N$ is finitely generated.

isNoetherian_of_finite instance

[Finite M] : IsNoetherian R M

Full source

instance (priority := 80) _root_.isNoetherian_of_finite [Finite M] : IsNoetherian R M :=
  ⟨fun s => ⟨(s : Set M).toFinite.toFinset, by rw [Set.Finite.coe_toFinset, Submodule.span_eq]⟩⟩

Finite Modules are Noetherian

Informal description

Every finite $R$-module $M$ is Noetherian.

Module.IsNoetherian.finite instance

[IsNoetherian R M] : Module.Finite R M

Full source

instance (priority := 100) IsNoetherian.finite [IsNoetherian R M] : Module.Finite R M :=
  ⟨IsNoetherian.noetherian ⊤⟩

Noetherian Modules are Finitely Generated

Informal description

Every Noetherian $R$-module $M$ is finitely generated.

Module.instFiniteSubtypeMemIdealOfIsNoetherian instance

 {R₁ S : Type*} [CommSemiring R₁] [Semiring S] [Algebra R₁ S] [IsNoetherian R₁ S] (I : Ideal S) : Module.Finite R₁ I

Full source

instance {R₁ S : Type*} [CommSemiring R₁] [Semiring S] [Algebra R₁ S]
    [IsNoetherian R₁ S] (I : Ideal S) : Module.Finite R₁ I :=
  IsNoetherian.finite R₁ ((I : Submodule S S).restrictScalars R₁)

Ideals in Noetherian Algebras are Finitely Generated

Informal description

For any commutative semiring $R_1$, semiring $S$ with an $R_1$-algebra structure, if $S$ is Noetherian as an $R_1$-module, then every ideal $I$ of $S$ is finitely generated as an $R_1$-module.

Module.Finite.of_injective theorem

[IsNoetherian R N] (f : M →ₗ[R] N) (hf : Function.Injective f) : Module.Finite R M

Full source

theorem Finite.of_injective [IsNoetherian R N] (f : M →ₗ[R] N) (hf : Function.Injective f) :
    Module.Finite R M :=
  ⟨fg_of_injective f hf⟩

Finitely Generated Module via Injective Map from Noetherian Module

Informal description

Let $R$ be a ring, and let $M$ and $N$ be $R$-modules with $N$ Noetherian. If there exists an injective $R$-linear map $f \colon M \to N$, then $M$ is finitely generated as an $R$-module.

isNoetherian_of_ker_bot theorem

[IsNoetherian R P] (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) : IsNoetherian R M

Full source

theorem isNoetherian_of_ker_bot [IsNoetherian R P] (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) :
    IsNoetherian R M :=
  isNoetherian_of_linearEquiv (LinearEquiv.ofInjective f <| LinearMap.ker_eq_bot.mp hf).symm

Noetherian Property via Injective Linear Map

Informal description

Let $R$ be a ring, and let $M$ and $P$ be $R$-modules. If $P$ is a Noetherian $R$-module and $f \colon M \to P$ is an injective $R$-linear map (i.e., $\ker f = 0$), then $M$ is also a Noetherian $R$-module.

fg_of_ker_bot theorem

[IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P) (hf : LinearMap.ker f = ⊥) : N.FG

Full source

theorem fg_of_ker_bot [IsNoetherian R P] {N : Submodule R M} (f : M →ₗ[R] P)
    (hf : LinearMap.ker f = ⊥) : N.FG :=
  haveI := isNoetherian_of_ker_bot f hf
  IsNoetherian.noetherian N

Finitely Generated Submodule via Injective Linear Map from Noetherian Module

Informal description

Let $R$ be a ring, $M$ and $P$ be $R$-modules, and $N$ be a submodule of $M$. If $P$ is a Noetherian $R$-module and $f \colon M \to P$ is an injective $R$-linear map (i.e., $\ker f = 0$), then $N$ is finitely generated.

isNoetherian_prod instance

[IsNoetherian R M] [IsNoetherian R P] : IsNoetherian R (M × P)

Full source

instance isNoetherian_prod [IsNoetherian R M] [IsNoetherian R P] : IsNoetherian R (M × P) :=
  ⟨fun s =>
    Submodule.fg_of_fg_map_of_fg_inf_ker (LinearMap.snd R M P) (noetherian _) <|
      have : s ⊓ LinearMap.ker (LinearMap.snd R M P) ≤ LinearMap.range (LinearMap.inl R M P) :=
        fun x ⟨_, hx2⟩ => ⟨x.1, Prod.ext rfl <| Eq.symm <| LinearMap.mem_ker.1 hx2⟩
      Submodule.map_comap_eq_self this ▸ (noetherian _).map _⟩

Noetherian Property of Direct Product Modules

Informal description

For any ring $R$ and Noetherian $R$-modules $M$ and $P$, the direct product module $M \times P$ is also Noetherian.

isNoetherian_sup instance

(M₁ M₂ : Submodule R P) [IsNoetherian R M₁] [IsNoetherian R M₂] : IsNoetherian R ↥(M₁ ⊔ M₂)

Full source

instance isNoetherian_sup (M₁ M₂ : Submodule R P) [IsNoetherian R M₁] [IsNoetherian R M₂] :
    IsNoetherian R ↥(M₁ ⊔ M₂) := by
  have := isNoetherian_range (M₁.subtype.coprod M₂.subtype)
  rwa [LinearMap.range_coprod, Submodule.range_subtype, Submodule.range_subtype] at this

Supremum of Noetherian Submodules is Noetherian

Informal description

For any ring $R$ and $R$-module $P$, if $M_1$ and $M_2$ are Noetherian submodules of $P$, then their supremum $M_1 \sqcup M_2$ is also a Noetherian submodule.

isNoetherian_pi instance

 :
  ∀ {M : ι → Type*} [∀ i, AddCommGroup (M i)] [∀ i, Module R (M i)] [∀ i, IsNoetherian R (M i)],
    IsNoetherian R (Π i, M i)

Full source

instance isNoetherian_pi :
    ∀ {M : ι → Type*} [∀ i, AddCommGroup (M i)]
      [∀ i, Module R (M i)] [∀ i, IsNoetherian R (M i)], IsNoetherian R (Π i, M i) := by
  apply Finite.induction_empty_option _ _ _ ι
  · exact fun e h ↦ isNoetherian_of_linearEquiv (LinearEquiv.piCongrLeft R _ e)
  · infer_instance
  · exact fun ih ↦ isNoetherian_of_linearEquiv (LinearEquiv.piOptionEquivProd R).symm

Noetherian Property of Product Modules

Informal description

For any ring $R$, index type $\iota$, and family of $R$-modules $M_i$ (each with an additive commutative group structure and $R$-module structure), if each $M_i$ is Noetherian, then the product module $\prod_{i \in \iota} M_i$ is also Noetherian.

isNoetherian_pi' instance

[IsNoetherian R M] : IsNoetherian R (ι → M)

Full source

/-- A version of `isNoetherian_pi` for non-dependent functions. We need this instance because
sometimes Lean fails to apply the dependent version in non-dependent settings (e.g., it fails to
prove that `ι → ℝ` is finite dimensional over `ℝ`). -/
instance isNoetherian_pi' [IsNoetherian R M] : IsNoetherian R (ι → M) :=
  isNoetherian_pi

Noetherian Property of Function Modules over Finite Index Types

Informal description

For any ring $R$, module $M$ over $R$, and finite index type $\iota$, if $M$ is a Noetherian $R$-module, then the function module $\iota \to M$ is also a Noetherian $R$-module.

isNoetherian_iSup instance

: ∀ {M : ι → Submodule R P} [∀ i, IsNoetherian R (M i)], IsNoetherian R ↥(⨆ i, M i)

Full source

instance isNoetherian_iSup :
    ∀ {M : ι → Submodule R P} [∀ i, IsNoetherian R (M i)], IsNoetherian R ↥(⨆ i, M i) := by
  apply Finite.induction_empty_option _ _ _ ι
  · intro _ _ e h _ _; rw [← e.iSup_comp]; apply h
  · intros; rw [iSup_of_empty]; infer_instance
  · intro _ _ ih _ _; rw [iSup_option]; infer_instance

Noetherian Property of Supremum of Submodules

Informal description

For any ring $R$, $R$-module $P$, and family of submodules $M_i$ of $P$, if each $M_i$ is a Noetherian $R$-module, then the supremum $\bigsqcup_i M_i$ is also a Noetherian $R$-module.

isNoetherian_of_range_eq_ker theorem

 [IsNoetherian R M] [IsNoetherian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : LinearMap.range f = LinearMap.ker g) :
  IsNoetherian R N

Full source

/-- If the first and final modules in an exact sequence are Noetherian,
  then the middle module is also Noetherian. -/
theorem isNoetherian_of_range_eq_ker [IsNoetherian R M] [IsNoetherian R P]
    (f : M →ₗ[R] N) (g : N →ₗ[R] P) (h : LinearMap.range f = LinearMap.ker g) :
    IsNoetherian R N :=
  isNoetherian_mk <|
    wellFounded_gt_exact_sequence
      (LinearMap.range f)
      (Submodule.map ((LinearMap.ker f).liftQ f le_rfl))
      (Submodule.comap ((LinearMap.ker f).liftQ f le_rfl))
      (Submodule.comap g.rangeRestrict) (Submodule.map g.rangeRestrict)
      (Submodule.gciMapComap <| LinearMap.ker_eq_bot.mp <| Submodule.ker_liftQ_eq_bot _ _ _ le_rfl)
      (Submodule.giMapComap g.surjective_rangeRestrict)
      (by simp [Submodule.map_comap_eq, inf_comm, Submodule.range_liftQ])
      (by simp [Submodule.comap_map_eq, h])

Noetherian property of the middle module in an exact sequence with Noetherian endpoints

Informal description

Let $R$ be a ring, and let $M$, $N$, and $P$ be $R$-modules. Given linear maps $f \colon M \to N$ and $g \colon N \to P$ such that the range of $f$ equals the kernel of $g$, if $M$ and $P$ are Noetherian $R$-modules, then $N$ is also a Noetherian $R$-module.

isNoetherian_iff_submodule_quotient theorem

(S : Submodule R P) : IsNoetherian R P ↔ IsNoetherian R S ∧ IsNoetherian R (P ⧸ S)

Full source

theorem isNoetherian_iff_submodule_quotient (S : Submodule R P) :
    IsNoetherianIsNoetherian R P ↔ IsNoetherian R S ∧ IsNoetherian R (P ⧸ S) := by
  refine ⟨fun _ ↦ ⟨inferInstance, inferInstance⟩, fun ⟨_, _⟩ ↦ ?_⟩
  apply isNoetherian_of_range_eq_ker S.subtype S.mkQ
  rw [Submodule.ker_mkQ, Submodule.range_subtype]

Noetherian Module Criterion via Submodule and Quotient

Informal description

Let $R$ be a ring and $P$ an $R$-module with a submodule $S \subseteq P$. Then $P$ is Noetherian if and only if both $S$ and the quotient module $P/S$ are Noetherian.

isNoetherian_linearMap_pi instance

{ι : Type*} [Finite ι] : IsNoetherian R ((ι → R) →ₗ[R] M)

Full source

instance isNoetherian_linearMap_pi {ι : Type*} [Finite ι] : IsNoetherian R ((ι → R) →ₗ[R] M) :=
  let _i : Fintype ι := Fintype.ofFinite ι; isNoetherian_of_linearEquiv (Module.piEquiv ι R M)

Noetherian Property of Linear Maps from Free Modules to Noetherian Modules

Informal description

For any ring $R$, Noetherian $R$-module $M$, and finite index type $\iota$, the space of linear maps from the free module $\iota \to R$ to $M$ is a Noetherian $R$-module.

isNoetherian_linearMap instance

: IsNoetherian R (N →ₗ[R] M)

Full source

instance isNoetherian_linearMap : IsNoetherian R (N →ₗ[R] M) := by
  obtain ⟨n, f, hf⟩ := Module.Finite.exists_fin' R N
  let g : (N →ₗ[R] M) →ₗ[R] (Fin n → R) →ₗ[R] M := (LinearMap.llcomp R (Fin n → R) N M).flip f
  exact isNoetherian_of_injective g hf.injective_linearMapComp_right

Noetherian Property of Linear Maps Between Noetherian Modules

Informal description

For any ring $R$ and Noetherian $R$-modules $M$ and $N$, the $R$-module of linear maps from $N$ to $M$ is Noetherian.

IsNoetherian.induction theorem

[IsNoetherian R M] {P : Submodule R M → Prop} (hgt : ∀ I, (∀ J > I, P J) → P I) (I : Submodule R M) : P I

Full source

/-- If `∀ I > J, P I` implies `P J`, then `P` holds for all submodules. -/
theorem IsNoetherian.induction [IsNoetherian R M] {P : Submodule R M → Prop}
    (hgt : ∀ I, (∀ J > I, P J) → P I) (I : Submodule R M) : P I :=
  IsWellFounded.induction _ I hgt

Noetherian Induction Principle for Submodules

Informal description

Let $M$ be a Noetherian $R$-module and $P$ be a predicate on submodules of $M$. If for every submodule $I$, the implication $(\forall J > I, P(J)) \to P(I)$ holds, then $P(I)$ holds for every submodule $I$ of $M$.

LinearMap.isNoetherian_iff_of_bijective theorem

 {S P} [Semiring S] [AddCommMonoid P] [Module S P] {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] P)
  (hl : Function.Bijective l) : IsNoetherian R M ↔ IsNoetherian S P

Full source

theorem LinearMap.isNoetherian_iff_of_bijective {S P} [Semiring S] [AddCommMonoid P] [Module S P]
    {σ : R →+* S} [RingHomSurjective σ] (l : M →ₛₗ[σ] P) (hl : Function.Bijective l) :
    IsNoetherianIsNoetherian R M ↔ IsNoetherian S P := by
  simp_rw [isNoetherian_iff']
  let e := Submodule.orderIsoMapComapOfBijective l hl
  exact ⟨fun _ ↦ e.symm.strictMono.wellFoundedGT, fun _ ↦ e.strictMono.wellFoundedGT⟩

Noetherian Module Equivalence under Bijective Linear Map

Informal description

Let $R$ and $S$ be semirings, $M$ be an $R$-module, and $P$ be an $S$-module. Given a ring homomorphism $\sigma : R \to S$ that is surjective as a map of additive monoids, and a $\sigma$-linear map $l : M \to P$ that is bijective, then $M$ is Noetherian as an $R$-module if and only if $P$ is Noetherian as an $S$-module.

Submodule.finite_ne_bot_of_iSupIndep theorem

{ι : Type*} {N : ι → Submodule R M} (h : iSupIndep N) : Set.Finite {i | N i ≠ ⊥}

Full source

lemma Submodule.finite_ne_bot_of_iSupIndep {ι : Type*} {N : ι → Submodule R M}
    (h : iSupIndep N) :
    Set.Finite {i | N i ≠ ⊥} :=
  WellFoundedGT.finite_ne_bot_of_iSupIndep h

Finiteness of Nonzero Submodules in a Supremum Independent Family

Informal description

Let $M$ be a module over a ring $R$ and let $\{N_i\}_{i \in \iota}$ be a family of submodules of $M$ that is supremum independent (i.e., for each $i$, $N_i$ is disjoint from the supremum of all other $N_j$). Then the set $\{i \in \iota \mid N_i \neq 0\}$ is finite.

LinearIndependent.finite_of_isNoetherian theorem

[Nontrivial R] {ι} {v : ι → M} (hv : LinearIndependent R v) : Finite ι

Full source

/-- A linearly-independent family of vectors in a module over a non-trivial ring must be finite if
the module is Noetherian. -/
theorem LinearIndependent.finite_of_isNoetherian [Nontrivial R] {ι} {v : ι → M}
    (hv : LinearIndependent R v) : Finite ι := by
  refine WellFoundedGT.finite_of_iSupIndep
    hv.iSupIndep_span_singleton
    fun i contra => ?_
  apply hv.ne_zero i
  have : v i ∈ R ∙ v i := Submodule.mem_span_singleton_self (v i)
  rwa [contra, Submodule.mem_bot] at this

Finiteness of Linearly Independent Families in Noetherian Modules

Informal description

Let $R$ be a nontrivial ring and $M$ be a Noetherian $R$-module. If $v : \iota \to M$ is a linearly independent family of vectors in $M$, then the index set $\iota$ is finite.

LinearIndependent.set_finite_of_isNoetherian theorem

[Nontrivial R] {s : Set M} (hi : LinearIndependent R ((↑) : s → M)) : s.Finite

Full source

theorem LinearIndependent.set_finite_of_isNoetherian [Nontrivial R] {s : Set M}
    (hi : LinearIndependent R ((↑) : s → M)) : s.Finite :=
  @Set.toFinite _ _ hi.finite_of_isNoetherian

Finiteness of Linearly Independent Subsets in Noetherian Modules

Informal description

Let $R$ be a nontrivial ring and $M$ be a Noetherian $R$-module. For any subset $s \subseteq M$, if the inclusion map $s \hookrightarrow M$ is linearly independent over $R$, then $s$ is finite.

IsNoetherian.disjoint_partialSups_eventually_bot theorem

 (f : ℕ → Submodule R M) (h : ∀ n, Disjoint (partialSups f n) (f (n + 1))) : ∃ n : ℕ, ∀ m, n ≤ m → f m = ⊥

Full source

/-- A sequence `f` of submodules of a noetherian module,
with `f (n+1)` disjoint from the supremum of `f 0`, ..., `f n`,
is eventually zero. -/
theorem IsNoetherian.disjoint_partialSups_eventually_bot
    (f : ℕ → Submodule R M) (h : ∀ n, Disjoint (partialSups f n) (f (n + 1))) :
    ∃ n : ℕ, ∀ m, n ≤ m → f m = ⊥ := by
  -- A little off-by-one cleanup first:
  suffices t : ∃ n : ℕ, ∀ m, n ≤ m → f (m + 1) = ⊥ by
    obtain ⟨n, w⟩ := t
    use n + 1
    rintro (_ | m) p
    · cases p
    · apply w
      exact Nat.succ_le_succ_iff.mp p
  obtain ⟨n, w⟩ := monotone_stabilizes_iff_noetherian.mpr inferInstance (partialSups f)
  refine ⟨n, fun m p ↦ (h m).eq_bot_of_ge <| sup_eq_left.mp ?_⟩
  simpa only [partialSups_add_one] using (w (m + 1) <| le_add_right p).symm.trans <| w m p

Disjoint Partial Suprema in Noetherian Modules Eventually Stabilize to Zero

Informal description

Let $M$ be a Noetherian $R$-module and let $(f_n)_{n \in \mathbb{N}}$ be a sequence of submodules of $M$ such that for each $n \in \mathbb{N}$, the submodule $f_{n+1}$ is disjoint from the supremum of the submodules $f_0, \dots, f_n$. Then there exists an index $N \in \mathbb{N}$ such that for all $m \geq N$, the submodule $f_m$ is trivial (i.e., $f_m = \bot$).

isNoetherian_of_subsingleton instance

(R M) [Subsingleton R] [Semiring R] [AddCommMonoid M] [Module R M] : IsNoetherian R M

Full source

/-- Modules over the trivial ring are Noetherian. -/
instance (priority := 100) isNoetherian_of_subsingleton (R M) [Subsingleton R] [Semiring R]
    [AddCommMonoid M] [Module R M] : IsNoetherian R M :=
  haveI := Module.subsingleton R M
  isNoetherian_of_finite R M

Modules over Trivial Rings are Noetherian

Informal description

For any semiring $R$ that is a subsingleton (i.e., has at most one element) and any $R$-module $M$, $M$ is a Noetherian $R$-module.

isNoetherian_of_submodule_of_noetherian theorem

(R M) [Semiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) (h : IsNoetherian R M) : IsNoetherian R N

Full source

theorem isNoetherian_of_submodule_of_noetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M]
    (N : Submodule R M) (h : IsNoetherian R M) : IsNoetherian R N :=
  isNoetherian_mk ⟨OrderEmbedding.wellFounded (Submodule.MapSubtype.orderEmbedding N).dual h.wf⟩

Submodules of Noetherian Modules are Noetherian

Informal description

Let $R$ be a semiring and $M$ be an $R$-module. If $M$ is Noetherian and $N$ is a submodule of $M$, then $N$ is also Noetherian.

isNoetherian_of_tower theorem

 (R) {S M} [Semiring R] [Semiring S] [AddCommMonoid M] [SMul R S] [Module S M] [Module R M] [IsScalarTower R S M]
  (h : IsNoetherian R M) : IsNoetherian S M

Full source

/-- If `M / S / R` is a scalar tower, and `M / R` is Noetherian, then `M / S` is
also noetherian. -/
theorem isNoetherian_of_tower (R) {S M} [Semiring R] [Semiring S] [AddCommMonoid M] [SMul R S]
    [Module S M] [Module R M] [IsScalarTower R S M] (h : IsNoetherian R M) : IsNoetherian S M :=
  isNoetherian_mk ⟨(Submodule.restrictScalarsEmbedding R S M).dual.wellFounded h.wf⟩

Noetherian module property under scalar tower extension

Informal description

Let $R$, $S$, and $M$ be such that $R$ and $S$ are semirings, $M$ is an $S$-module and an $R$-module, and the scalar multiplication is compatible via $[IsScalarTower R S M]$. If $M$ is a Noetherian $R$-module, then $M$ is also a Noetherian $S$-module.

isNoetherian_of_isNoetherianRing_of_finite instance

(R M : Type*) [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] : IsNoetherian R M

Full source

instance isNoetherian_of_isNoetherianRing_of_finite (R M : Type*)
    [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] [Module.Finite R M] :
    IsNoetherian R M :=
  have ⟨_, _, h⟩ := Module.Finite.exists_fin' R M
  isNoetherian_of_surjective _ _ (LinearMap.range_eq_top.mpr h)

Finitely Generated Modules over Noetherian Rings are Noetherian

Informal description

Let $R$ be a Noetherian ring and $M$ a finitely generated $R$-module. Then $M$ is a Noetherian $R$-module.

isNoetherian_of_fg_of_noetherian theorem

 {R M} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [I : IsNoetherianRing R] (hN : N.FG) :
  IsNoetherian R N

Full source

theorem isNoetherian_of_fg_of_noetherian {R M} [Ring R] [AddCommGroup M] [Module R M]
    (N : Submodule R M) [I : IsNoetherianRing R] (hN : N.FG) : IsNoetherian R N := by
  rw [← Module.Finite.iff_fg] at hN; infer_instance

Finitely generated submodules over Noetherian rings are Noetherian

Informal description

Let $R$ be a Noetherian ring and $M$ an $R$-module. For any finitely generated submodule $N$ of $M$, the $R$-module $N$ is Noetherian.

isNoetherian_span_of_finite theorem

 (R) {M} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherianRing R] {A : Set M} (hA : A.Finite) :
  IsNoetherian R (Submodule.span R A)

Full source

/-- In a module over a Noetherian ring, the submodule generated by finitely many vectors is
Noetherian. -/
theorem isNoetherian_span_of_finite (R) {M} [Ring R] [AddCommGroup M] [Module R M]
    [IsNoetherianRing R] {A : Set M} (hA : A.Finite) : IsNoetherian R (Submodule.span R A) :=
  isNoetherian_of_fg_of_noetherian _ (Submodule.fg_def.mpr ⟨A, hA, rfl⟩)

Finite spans in Noetherian modules are Noetherian

Informal description

Let $R$ be a Noetherian ring and $M$ an $R$-module. For any finite subset $A \subseteq M$, the submodule $\operatorname{span}_R A$ is Noetherian.

IsNoetherianRing.of_finite theorem

 (R S) [Ring R] [Ring S] [Module R S] [IsScalarTower R S S] [IsNoetherianRing R] [Module.Finite R S] :
  IsNoetherianRing S

Full source

theorem IsNoetherianRing.of_finite (R S) [Ring R] [Ring S] [Module R S] [IsScalarTower R S S]
    [IsNoetherianRing R] [Module.Finite R S] : IsNoetherianRing S :=
  isNoetherian_of_tower R inferInstance

Noetherian Ring Property via Finite Module Extension

Informal description

Let $R$ and $S$ be rings such that $S$ is a finitely generated $R$-module and the scalar multiplication is compatible via $[IsScalarTower R S S]$. If $R$ is a Noetherian ring, then $S$ is also a Noetherian ring.

isNoetherianRing_of_surjective theorem

 (R) [Semiring R] (S) [Semiring S] (f : R →+* S) (hf : Function.Surjective f) [H : IsNoetherianRing R] :
  IsNoetherianRing S

Full source

theorem isNoetherianRing_of_surjective (R) [Semiring R] (S) [Semiring S] (f : R →+* S)
    (hf : Function.Surjective f) [H : IsNoetherianRing R] : IsNoetherianRing S :=
  isNoetherian_mk ⟨OrderEmbedding.wellFounded (Ideal.orderEmbeddingOfSurjective f hf).dual H.wf⟩

Noetherian Ring Property Preserved under Surjective Ring Homomorphism

Informal description

Let $R$ and $S$ be semirings, and let $f \colon R \to S$ be a surjective ring homomorphism. If $R$ is a Noetherian ring, then $S$ is also a Noetherian ring.

isNoetherianRing_rangeS instance

{R} [Semiring R] {S} [Semiring S] (f : R →+* S) [IsNoetherianRing R] : IsNoetherianRing f.rangeS

Full source

instance isNoetherianRing_rangeS {R} [Semiring R] {S} [Semiring S] (f : R →+* S)
    [IsNoetherianRing R] : IsNoetherianRing f.rangeS :=
  isNoetherianRing_of_surjective R f.rangeS f.rangeSRestrict f.rangeSRestrict_surjective

Noetherian Property of the Image of a Ring Homomorphism

Informal description

For any semirings $R$ and $S$ and a ring homomorphism $f \colon R \to S$, if $R$ is a Noetherian ring, then the image of $f$ (denoted $f.rangeS$) is also a Noetherian ring.

isNoetherianRing_range instance

{R} [Ring R] {S} [Ring S] (f : R →+* S) [IsNoetherianRing R] : IsNoetherianRing f.range

Full source

instance isNoetherianRing_range {R} [Ring R] {S} [Ring S] (f : R →+* S)
    [IsNoetherianRing R] : IsNoetherianRing f.range :=
  isNoetherianRing_rangeS f

Noetherian Property of the Range of a Ring Homomorphism

Informal description

For any rings $R$ and $S$ and a ring homomorphism $f \colon R \to S$, if $R$ is a Noetherian ring, then the range of $f$ is also a Noetherian ring.

isNoetherianRing_of_ringEquiv theorem

(R) [Semiring R] {S} [Semiring S] (f : R ≃+* S) [IsNoetherianRing R] : IsNoetherianRing S

Full source

theorem isNoetherianRing_of_ringEquiv (R) [Semiring R] {S} [Semiring S] (f : R ≃+* S)
    [IsNoetherianRing R] : IsNoetherianRing S :=
  isNoetherianRing_of_surjective R S f.toRingHom f.toEquiv.surjective

Noetherian Ring Property Preserved under Ring Isomorphism

Informal description

Let $R$ and $S$ be semirings, and let $f \colon R \simeq S$ be a ring isomorphism. If $R$ is a Noetherian ring, then $S$ is also a Noetherian ring.

instIsNoetherianRingProd instance

{R S} [Semiring R] [Semiring S] [IsNoetherianRing R] [IsNoetherianRing S] : IsNoetherianRing (R × S)

Full source

instance {R S} [Semiring R] [Semiring S] [IsNoetherianRing R] [IsNoetherianRing S] :
    IsNoetherianRing (R × S) := by
  rw [IsNoetherianRing, isNoetherian_iff'] at *
  exact Ideal.idealProdEquiv.toOrderEmbedding.wellFoundedGT

Product of Noetherian Semirings is Noetherian

Informal description

The product $R \times S$ of two Noetherian semirings $R$ and $S$ is also a Noetherian semiring.

instIsNoetherianRingForallOfFinite instance

 {ι} [Finite ι] : ∀ {R : ι → Type*} [Π i, Semiring (R i)] [∀ i, IsNoetherianRing (R i)], IsNoetherianRing (Π i, R i)

Full source

instance {ι} [Finite ι] : ∀ {R : ι → Type*} [Π i, Semiring (R i)] [∀ i, IsNoetherianRing (R i)],
    IsNoetherianRing (Π i, R i) := by
  apply Finite.induction_empty_option _ _ _ ι
  · exact fun e h ↦ isNoetherianRing_of_ringEquiv _ (.piCongrLeft _ e)
  · infer_instance
  · exact fun ih ↦ isNoetherianRing_of_ringEquiv _ (.symm .piOptionEquivProd)

Finite Product of Noetherian Rings is Noetherian

Informal description

For any finite index type $\iota$ and any family of semirings $R_i$ indexed by $\iota$, if each $R_i$ is a Noetherian ring, then the product semiring $\prod_{i} R_i$ is also Noetherian.

Mathlib.RingTheory.Noetherian.Basic

Main definitions

Main statements

References

Tags