Module

ModuleDepthBound.lean

Nyll.SchemeTheory.RingTheory.ModuleDepthBound

3 declarations indexed from sourceView source ↗

Module documentation

Bounding module depth by Krull dimension

The depth of a nontrivial finite module over a Noetherian local ring is bounded by the Krull dimension of its support and hence by the Krull dimension of the ring.

Imports6

Nyll.SchemeTheory.RingTheory.LocalAlgebra
Mathlib.RingTheory.KrullDimension.Basic
Mathlib.RingTheory.KrullDimension.NonZeroDivisors
Mathlib.RingTheory.Support
Mathlib.RingTheory.Regular.RegularSequence
Mathlib.RingTheory.Ideal.Quotient.Operations

Imported by3

lemma

depth_le_krullDim_support'

L45 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_depth_le_ringKrullDim.Module.depth_le_krullDim_support'

Source context 8 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_depth_le_ringKrullDim
open IsLocalRing RingTheory
namespace Module
open _root_.Module
open _root_.Module
variable (R M : Type*) [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M]
open scoped Pointwise in

Lean source · statement

lemma depth_le_krullDim_support' [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ Order.krullDim (Module.support R M)

lemma

depth_le_dim_annihilator'

L139 ↗

AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_depth_le_ringKrullDim.Module.depth_le_dim_annihilator'

Source context 7 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_depth_le_ringKrullDim
open IsLocalRing RingTheory
namespace Module
open _root_.Module
open _root_.Module
variable (R M : Type*) [CommRing R] [IsLocalRing R] [AddCommGroup M] [Module R M]

Lean source · statement

lemma depth_le_dim_annihilator' [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ ringKrullDim (R ⧸ Module.annihilator R M)

theorem

depth_le_ringKrullDim

L146 ↗

Module.depth_le_ringKrullDim

Source context 3 commands

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

section ProofImplementation
namespace AlgebraicCurves.Foundations.CommutativeAlgebra.Proofs.Module_depth_le_ringKrullDim
open IsLocalRing RingTheory

Lean source · statement

theorem _root_.Module.depth_le_ringKrullDim {R M : Type*} [CommRing R] [IsLocalRing R]
    [AddCommGroup M] [Module R M] [Nontrivial M] [Module.Finite R M] :
    .some (Module.depth R M) ≤ ringKrullDim R

Module documentation

Bounding module depth by Krull dimension

Declarations

depth_le_krullDim_support'

depth_le_dim_annihilator'

depth_le_ringKrullDim