Module

ArtinianSocleFiniteLength.lean

Nyll.EtaleFundamentalGroups.Purity.ArtinianSocleFiniteLength

1 declaration indexed from sourceView source ↗

Module documentation

Finite length of an Artinian socle

The submodule killed by the maximal ideal has its canonical residue-field module structure. An Artinian module over this field is finitely generated; restriction of scalars then makes it finite over the original Noetherian ring.

Imports7

Mathlib.Algebra.Module.Torsion.Basic
Mathlib.RingTheory.FiniteLength
Mathlib.RingTheory.Finiteness.Basic
Mathlib.RingTheory.HopkinsLevitzki
Mathlib.RingTheory.Ideal.Quotient.Basic
Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
Mathlib.RingTheory.Noetherian.Basic

Imported by3

theorem

isFiniteLength_torsionBySet_maximalIdeal_of_artinian

L30 ↗

EtaleFundamentalGroups.Purity.isFiniteLength_torsionBySet_maximalIdeal_of_artinian

Documentation

An Artinian socle over a Noetherian local ring has finite length.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R] [IsLocalRing R]

Lean source · statement

theorem isFiniteLength_torsionBySet_maximalIdeal_of_artinian
    [IsNoetherianRing R] (M : Type v) [AddCommGroup M] [Module R M]
    [IsArtinian R (Submodule.torsionBySet R M (IsLocalRing.maximalIdeal R))] :
    IsFiniteLength R (Submodule.torsionBySet R M (IsLocalRing.maximalIdeal R))

Module documentation

Finite length of an Artinian socle

Declarations

isFiniteLength_torsionBySet_maximalIdeal_of_artinian