NYLL
Module

MaximalIdealPowerQuotientLength.lean

Nyll.EtaleFundamentalGroups.Purity.MaximalIdealPowerQuotientLength
1 declaration indexed from sourceView source ↗

Module documentation

Finite length of maximal-ideal-power quotients

A positive power of the maximal ideal has that same maximal ideal as its only minimal prime. Its quotient is Artinian, and restriction of scalars gives finite length over the original Noetherian local ring.

Imports6
  • Mathlib.RingTheory.Artinian.Module
  • Mathlib.RingTheory.FiniteLength
  • Mathlib.RingTheory.Ideal.KrullsHeightTheorem
  • Mathlib.RingTheory.Ideal.Operations
  • Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
  • Mathlib.RingTheory.Noetherian.Basic
Imported by3

Declarations

theorem

isFiniteLength_quotient_maximalIdeal_pow

L32 ↗
EtaleFundamentalGroups.Purity.isFiniteLength_quotient_maximalIdeal_pow
Documentation

Quotients of a Noetherian local ring by powers of its maximal ideal have finite length as modules over the original ring.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem isFiniteLength_quotient_maximalIdeal_pow (n : ℕ) :
    IsFiniteLength R (R ⧸ maximalIdeal R ^ n)

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