Documentation

Mathlib.RingTheory.Artinian

Artinian rings and modules #

A module satisfying these equivalent conditions is said to be an Artinian R-module if every decreasing chain of submodules is eventually constant, or equivalently, if the relation < on submodules is well founded.

A ring is said to be left (or right) Artinian if it is Artinian as a left (or right) module over itself, or simply Artinian if it is both left and right Artinian.

Main definitions #

Let R be a ring and let M and P be R-modules. Let N be an R-submodule of M.

Main results #

References #

Tags #

Artinian, artinian, Artinian ring, Artinian module, artinian ring, artinian module

@[reducible, inline]
abbrev IsArtinian (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :

IsArtinian R M is the proposition that M is an Artinian R-module, implemented as the well-foundedness of submodule inclusion.

Equations
Instances For
    theorem isArtinian_iff (R : Type u_1) (M : Type u_2) [Semiring R] [AddCommMonoid M] [Module R M] :
    IsArtinian R M WellFounded fun (x1 x2 : Submodule R M) => x1 < x2
    theorem isArtinian_of_injective {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (f : M →ₗ[R] P) (h : Function.Injective f) [IsArtinian R P] :
    instance isArtinian_submodule' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (N : Submodule R M) :
    IsArtinian R N
    Equations
    • =
    theorem isArtinian_of_le {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] {s : Submodule R M} {t : Submodule R M} [IsArtinian R t] (h : s t) :
    IsArtinian R s
    theorem isArtinian_of_surjective {R : Type u_1} (M : Type u_2) {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (f : M →ₗ[R] P) (hf : Function.Surjective f) [IsArtinian R M] :
    theorem isArtinian_of_linearEquiv {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] (f : M ≃ₗ[R] P) [IsArtinian R M] :
    theorem isArtinian_of_range_eq_ker {R : Type u_1} {M : Type u_2} {P : Type u_3} {N : Type u_4} [Ring R] [AddCommGroup M] [AddCommGroup P] [AddCommGroup N] [Module R M] [Module R P] [Module R N] [IsArtinian R M] [IsArtinian R P] (f : M →ₗ[R] N) (g : N →ₗ[R] P) (hf : Function.Injective f) (hg : Function.Surjective g) (h : LinearMap.range f = LinearMap.ker g) :
    instance isArtinian_prod {R : Type u_1} {M : Type u_2} {P : Type u_3} [Ring R] [AddCommGroup M] [AddCommGroup P] [Module R M] [Module R P] [IsArtinian R M] [IsArtinian R P] :
    IsArtinian R (M × P)
    Equations
    • =
    @[instance 100]
    instance isArtinian_of_finite {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Finite M] :
    Equations
    • =
    instance isArtinian_pi {R : Type u_5} {ι : Type u_6} [Finite ι] {M : ιType u_7} [Ring R] [(i : ι) → AddCommGroup (M i)] [(i : ι) → Module R (M i)] [∀ (i : ι), IsArtinian R (M i)] :
    IsArtinian R ((i : ι) → M i)
    Equations
    • =
    instance isArtinian_pi' {R : Type u_5} {ι : Type u_6} {M : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [Finite ι] [IsArtinian R M] :
    IsArtinian R (ιM)

    A version of isArtinian_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 ).

    Equations
    • =
    instance isArtinian_finsupp {R : Type u_5} {ι : Type u_6} {M : Type u_7} [Ring R] [AddCommGroup M] [Module R M] [Finite ι] [IsArtinian R M] :
    Equations
    • =
    theorem IsArtinian.finite_of_linearIndependent {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [Nontrivial R] [h : IsArtinian R M] {s : Set M} (hs : LinearIndependent R Subtype.val) :
    s.Finite
    theorem set_has_minimal_iff_artinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] :
    (∀ (a : Set (Submodule R M)), a.NonemptyM'a, Ia, ¬I < M') IsArtinian R M

    A module is Artinian iff every nonempty set of submodules has a minimal submodule among them.

    theorem IsArtinian.set_has_minimal {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (a : Set (Submodule R M)) (ha : a.Nonempty) :
    M'a, Ia, ¬I < M'
    theorem monotone_stabilizes_iff_artinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] :
    (∀ (f : →o (Submodule R M)ᵒᵈ), ∃ (n : ), ∀ (m : ), n mf n = f m) IsArtinian R M

    A module is Artinian iff every decreasing chain of submodules stabilizes.

    theorem IsArtinian.monotone_stabilizes {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : →o (Submodule R M)ᵒᵈ) :
    ∃ (n : ), ∀ (m : ), n mf n = f m
    theorem IsArtinian.eventuallyConst_of_isArtinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : →o (Submodule R M)ᵒᵈ) :
    Filter.EventuallyConst (⇑f) Filter.atTop
    theorem IsArtinian.induction {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] {P : Submodule R MProp} (hgt : ∀ (I : Submodule R M), (∀ J < I, P J)P I) (I : Submodule R M) :
    P I

    If ∀ I > J, P I implies P J, then P holds for all submodules.

    theorem LinearMap.eventually_codisjoint_ker_pow_range_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : M →ₗ[R] M) :
    ∀ᶠ (n : ) in Filter.atTop, Codisjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

    For any endomorphism of an Artinian module, any sufficiently high iterate has codisjoint kernel and range.

    theorem LinearMap.eventually_iInf_range_pow_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : Module.End R M) :
    ∀ᶠ (n : ) in Filter.atTop, ⨅ (m : ), LinearMap.range (f ^ m) = LinearMap.range (f ^ n)
    theorem LinearMap.eventually_isCompl_ker_pow_range_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (f : M →ₗ[R] M) :
    ∀ᶠ (n : ) in Filter.atTop, IsCompl (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

    This is the Fitting decomposition of the module M with respect to the endomorphism f.

    See also LinearMap.isCompl_iSup_ker_pow_iInf_range_pow for an alternative spelling.

    theorem LinearMap.isCompl_iSup_ker_pow_iInf_range_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] [IsNoetherian R M] (f : M →ₗ[R] M) :
    IsCompl (⨆ (n : ), LinearMap.ker (f ^ n)) (⨅ (n : ), LinearMap.range (f ^ n))

    This is the Fitting decomposition of the module M with respect to the endomorphism f.

    See also LinearMap.eventually_isCompl_ker_pow_range_pow for an alternative spelling.

    Any injective endomorphism of an Artinian module is surjective.

    Any injective endomorphism of an Artinian module is bijective.

    theorem IsArtinian.disjoint_partial_infs_eventually_top {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinian R M] (f : Submodule R M) (h : ∀ (n : ), Disjoint ((partialSups (OrderDual.toDual f)) n) (OrderDual.toDual (f (n + 1)))) :
    ∃ (n : ), ∀ (m : ), n mf m =

    A sequence f of submodules of an artinian module, with the supremum f (n+1) and the infimum of f 0, ..., f n being ⊤, is eventually ⊤.

    theorem IsArtinian.range_smul_pow_stabilizes {R : Type u_1} (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [IsArtinian R M] (r : R) :
    ∃ (n : ), ∀ (m : ), n mLinearMap.range (r ^ n LinearMap.id) = LinearMap.range (r ^ m LinearMap.id)
    theorem IsArtinian.exists_pow_succ_smul_dvd {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsArtinian R M] (r : R) (x : M) :
    ∃ (n : ) (y : M), r ^ n.succ y = r ^ n x
    @[reducible, inline]
    abbrev IsArtinianRing (R : Type u_1) [Ring R] :

    A ring is Artinian if it is Artinian as a module over itself.

    Strictly speaking, this should be called IsLeftArtinianRing but we omit the Left for convenience in the commutative case. For a right Artinian ring, use IsArtinian Rᵐᵒᵖ R.

    Equations
    Instances For
      Equations
      • =
      theorem Ring.isArtinian_of_zero_eq_one {R : Type u_1} [Ring R] (h01 : 0 = 1) :
      theorem isArtinian_of_submodule_of_artinian (R : Type u_1) (M : Type u_2) [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) :
      IsArtinian R MIsArtinian R N
      instance isArtinian_of_quotient_of_artinian (R : Type u_1) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] (N : Submodule R M) [IsArtinian R M] :
      IsArtinian R (M N)
      Equations
      • =
      theorem isArtinian_of_tower (R : Type u_1) {S : Type u_2} {M : Type u_3} [CommRing R] [Ring S] [AddCommGroup M] [Algebra R S] [Module S M] [Module R M] [IsScalarTower R S M] (h : IsArtinian R M) :

      If M / S / R is a scalar tower, and M / R is Artinian, then M / S is also Artinian.

      Equations
      • =
      theorem isArtinian_of_fg_of_artinian {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] (N : Submodule R M) [IsArtinianRing R] (hN : N.FG) :
      IsArtinian R N
      instance isArtinian_of_fg_of_artinian' {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R] [Module.Finite R M] :
      Equations
      • =
      theorem isArtinian_span_of_finite (R : Type u_1) {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R] {A : Set M} (hA : A.Finite) :

      In a module over an artinian ring, the submodule generated by finitely many vectors is artinian.

      theorem Function.Surjective.isArtinianRing {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] {F : Type u_3} [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective f) [H : IsArtinianRing R] :
      instance isArtinianRing_range {R : Type u_1} [Ring R] {S : Type u_2} [Ring S] (f : R →+* S) [IsArtinianRing R] :
      IsArtinianRing f.range
      Equations
      • =

      Localizing an artinian ring can only reduce the amount of elements.

      IsArtinianRing.localization_artinian can't be made an instance, as it would make S + R into metavariables. However, this is safe.

      Equations
      • =
      instance IsArtinianRing.isMaximal_of_isPrime {R : Type u_1} [CommRing R] [IsArtinianRing R] (p : Ideal R) [p.IsPrime] :
      p.IsMaximal
      Equations
      • =
      theorem IsArtinianRing.isPrime_iff_isMaximal {R : Type u_1} [CommRing R] [IsArtinianRing R] (p : Ideal R) :
      p.IsPrime p.IsMaximal
      theorem IsArtinianRing.primeSpectrum_finite (R : Type u_1) [CommRing R] [IsArtinianRing R] :
      {I : Ideal R | I.IsPrime}.Finite
      theorem IsArtinianRing.maximal_ideals_finite (R : Type u_1) [CommRing R] [IsArtinianRing R] :
      {I : Ideal R | I.IsMaximal}.Finite

      Stacks Lemma 00J7

      theorem IsArtinianRing.subtype_isMaximal_finite (R : Type u_1) [CommRing R] [IsArtinianRing R] :
      Finite {I : Ideal R | I.IsMaximal}
      noncomputable def IsArtinianRing.fieldOfSubtypeIsMaximal (R : Type u_1) [CommRing R] (I : {I : Ideal R | I.IsMaximal}) :
      Field (R I)

      A temporary field instance on the quotients by maximal ideals.

      Equations
      Instances For
        noncomputable def IsArtinianRing.quotNilradicalEquivPi (R : Type u_1) [CommRing R] [IsArtinianRing R] :
        R nilradical R ≃+* ((I : {I : Ideal R | I.IsMaximal}) → R I)

        The quotient of a commutative artinian ring by its nilradical is isomorphic to a finite product of fields, namely the quotients by the maximal ideals.

        Equations
        Instances For
          noncomputable def IsArtinianRing.equivPi (R : Type u_1) [CommRing R] [IsArtinianRing R] [IsReduced R] :
          R ≃+* ((I : {I : Ideal R | I.IsMaximal}) → R I)

          A reduced commutative artinian ring is isomorphic to a finite product of fields, namely the quotients by the maximal ideals.

          Equations
          Instances For