NYLL
Module

CompleteLocalPowerTorsionArtinian.lean

Nyll.EtaleFundamentalGroups.Purity.CompleteLocalPowerTorsionArtinian
3 declarations indexed from sourceView source ↗

Module documentation

Artinianness from the socle over a complete local ring

Constructing an Artinian injective hull of the residue field shows that any module with a finite-length essential submodule is Artinian. In a maximal-ideal-power torsion module the socle is essential, so it suffices that the socle be Artinian. In particular an Artinian scalar kernel for a member of the maximal ideal suffices.

Imports14
Imported by2

Declarations

theorem

isArtinian_of_completeLocal_finiteLength_essential_submodule

L44 ↗
EtaleFundamentalGroups.Purity.isArtinian_of_completeLocal_finiteLength_essential_submodule
Documentation

Over a complete Noetherian local ring, a finite-length essential submodule forces the entire module to be Artinian.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
variable {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem isArtinian_of_completeLocal_finiteLength_essential_submodule
    (N : Submodule R M) (hN : IsEssentialSubmodule N) (hlen : IsFiniteLength R N) :
    IsArtinian R M
theorem

isArtinian_of_maximalIdealPower_torsion_of_artinian_socle

L55 ↗
EtaleFundamentalGroups.Purity.isArtinian_of_maximalIdealPower_torsion_of_artinian_socle
Documentation

Maximal-ideal-power torsion and an Artinian socle imply that a module over a complete Noetherian local ring is Artinian.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
variable {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem isArtinian_of_maximalIdealPower_torsion_of_artinian_socle
    [IsArtinian R (Submodule.torsionBySet R M (maximalIdeal R))]
    (hM : ∀ z : M, ∃ n : ℕ, ∀ a ∈ maximalIdeal R ^ n, a • z = 0) :
    IsArtinian R M
theorem

isArtinian_of_maximalIdealPower_torsion_of_artinian_scalarKernel

L66 ↗
EtaleFundamentalGroups.Purity.isArtinian_of_maximalIdealPower_torsion_of_artinian_scalarKernel
Documentation

A scalar kernel containing the socle gives the Artinian criterion used with coefficient exact sequences in local cohomology.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

namespace EtaleFundamentalGroups.Purity
universe u v
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
variable {M : Type v} [AddCommGroup M] [Module R M]
Lean source · statement
theorem isArtinian_of_maximalIdealPower_torsion_of_artinian_scalarKernel
    (x : R) (hx : x ∈ maximalIdeal R)
    [IsArtinian R (LinearMap.ker (x • (LinearMap.id : M →ₗ[R] M)))]
    (hM : ∀ z : M, ∃ n : ℕ, ∀ a ∈ maximalIdeal R ^ n, a • z = 0) :
    IsArtinian R M

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.