Basic depth of modules #
Mathlib defines the depth IsLocalRing.depth M of a module over a local ring R through the
vanishing of Ext (R β§Έ πͺ) M, and identifies it, for a finite nonzero module over a Noetherian local
ring, with the supremum of the lengths of M-regular sequences in πͺ. This file relates depth
to dimension, quotients by regular sequences, short exact sequences and modules of linear maps,
and, after localization, to associated primes. The short exact sequence bounds hold for
Ideal.depth I over any commutative ring; the other results are for Noetherian local rings
or, after localization, Noetherian rings.
The regular-sequence transfer lemmas for linear maps live in
TauCeti.RingTheory.Regular.LinearMap.
Main results #
RingTheory.Sequence.IsRegular.mem_maximalIdeal: over a local ring, every element of anM-regular sequence lies in the maximal ideal.IsLocalRing.depth_le_supportDim: the depth of a finite nonzero module over a Noetherian local ring is at most the dimension of its support (Stacks, Lemma 10.72.3 (00LK)), by the boundRingTheory.Sequence.IsRegular.length_le_supportDimfromTauCeti.RingTheory.KrullDimension.Regular.IsLocalRing.maximalIdeal_ne_bot_of_depth_ne_zero: a local ring of positive depth is not a field.Ideal.depth_min_snd_trd_add_one_le_fst_of_exact,Ideal.depth_min_snd_fst_sub_one_le_trd_of_exact, andIdeal.depth_min_fst_trd_le_snd_of_exact(withIsLocalRing.specializations): the depth inequalities for short exact sequences of linear maps, across module universes. They are the linear-map forms of Mathlib'sModuleCat.depth_min_snd_trd_add_one_le_fst_right,ModuleCat.depth_min_snd_fst_sub_one_le_trd_rightandModuleCat.depth_min_fst_trd_le_snd_right, transported throughModuleCat.shortComplexOfConj_shortExact.ModuleCat.depth_trd_add_one_le_fst_of_comp_mkβ_eq_zero: for a short exact sequence0 β Xβ β Xβ β Xβ β 0whose first map induces zero onExt N - nfor everyn, the depth ofXβis at least one more than that ofXβ. This sharpens Mathlib'sModuleCat.depth_min_snd_trd_add_one_le_fst_right.ModuleCat.depth_le_depth_of_support_subset: for finite modulesNandMover a Noetherian ring withSupp N β V(I),I.depth M β€ N.depth M.IsLocalRing.depth_prodandIsLocalRing.depth_eq_depth_self_of_free: the depth of a product is the minimum of the depths, so a nonzero finite free module has the depth of the ring.IsLocalRing.depth_add_one_le_depth_ker: for a free presentation0 β K β F β M β 0withKfinite free andK β πͺ F,depth M + 1 β€ depth K.IsLocalRing.depth_quotSMulTop_succ_eq_depth: dividing a finite module by anM-regular element of the maximal ideal lowers the depth by exactly one.IsLocalRing.depth_quotSMulTop_eq_of_surjectiveandIsLocalRing.depth_eq_add_one_of_surjective: the same statements for a moduleQpresented as the target of a surjection with kernelx M.IsLocalRing.depth_add_length_eq_depth_of_isRegular: dividing a finite module by anM-regular sequencerβ, β¦, rβlowers the depth by exactlyn.IsLocalRing.depth_eq_depth_of_surjective: along a surjective homomorphism of local ringsR β T, a finiteT-module has the same depth overRas overT.RingEquiv.depth_self_eq: isomorphic Noetherian local rings have the same depth over themselves.IsLocalRing.depth_hom_ge: depth at least one or two passes from the target module to the module of linear maps (Stacks, Lemma 15.24.10 (0AV5)).IsLocalRing.mem_span_singleton_of_forall_mul_mem_of_two_le_depth: in a Noetherian local ring of depth at least two,πͺ c β (b)for a nonzerodivisorbforcesc β (b), so the maximal ideal is not an associated prime ofR β§Έ (b).IsLocalRing.mem_range_algebraMap_of_two_le_depth: in a Noetherian local ring of depth at least two, an element of the total ring of fractions lying inR_pfor every primep β πͺlies inR.IsLocalRing.depth_le_ringKrullDim_quotient_of_isAssociatedPrime: the depth of a finite module is at mostdim (R β§Έ p)for every associated primepof the module (Matsumura, Theorem 17.2).IsLocalRing.depth_eq_zero_iff_nontrivial_linearMapandIsLocalRing.depth_eq_zero_iff_maximalIdeal_mem_associatedPrimes: the depth vanishes exactly when the residue field maps nontrivially to the module, that is, when the maximal ideal is an associated prime.Ideal.depth_localizedModule_self: the module localizationLocalizedModule p.primeCompl Rhas the depth of the local ringR_p.TauCeti.depth_localizedModule_eq_zero_iff:M_phas depth zero exactly whenpis an associated prime ofM, andTauCeti.one_le_depth_localizedModule_iffis its negation. This combines the depth-zero criterion withTauCeti.maximalIdeal_mem_associatedPrimes_localizedModule_ifffromTauCeti.RingTheory.Ideal.AssociatedPrime.Localization.TauCeti.depth_localizedModule_quotSMulTop_add_one: dividing a finite module by anM-regular element of a primeplowers the depth of the localization atpby exactly one.
The two quotient-depth results, together with Mathlib's
Module.supportDim_add_length_eq_supportDim_of_isRegular, make CohenβMacaulayness stable under
quotients by regular sequences.
Over a local ring, every element of an M-regular sequence lies in the maximal ideal.
In a short exact sequence 0 β Xβ β Xβ β Xβ β 0 whose first map induces the zero map
Ext N Xβ n β Ext N Xβ n for every n, the depth of Xβ with respect to N is at least one
more than that of Xβ: the connecting maps Ext N Xβ n β Ext N Xβ (n + 1) are surjective.
For finite modules N and M over a Noetherian ring with N supported in V(I), the depth
of M with respect to I is at most the depth N.depth M: Ext N M i vanishes for every
i < I.depth M. Unlike ModuleCat.depth_eq_depth_of_support_eq, this needs neither N β 0 nor
I M β M. The proof uses the Rees theorem ModuleCat.exists_isRegular_tfae (Matsumura,
Commutative Algebra, Theorem 28).
For a short exact sequence of linear maps, the source depth with respect to an ideal is at least the minimum of the middle depth and one plus the target depth. The modules may lie in different universes.
For a short exact sequence of linear maps, the target depth with respect to an ideal is at least the minimum of the middle depth and the source depth minus one. The modules may lie in different universes.
For a short exact sequence of linear maps, the middle depth with respect to an ideal is at least the minimum of the source and target depths. The modules may lie in different universes.
Local-ring form of Ideal.depth_min_snd_trd_add_one_le_fst_of_exact.
Local-ring form of Ideal.depth_min_snd_fst_sub_one_le_trd_of_exact.
Local-ring form of Ideal.depth_min_fst_trd_le_snd_of_exact.
The depth of a product of two modules over a local ring is the minimum of their depths.
A nonzero finite free module over a local ring has the same depth as the ring.
If 0 β K β F β M β 0 is a free presentation with K finite free and K β πͺ F, then
depth M + 1 β€ depth K.
The depth of a finite nonzero module M over a Noetherian local ring is at most the dimension
of its support. Stacks, Lemma 10.72.3 (00LK).
The depth of a module over a local ring is zero exactly when there is a nonzero linear map to
it from the residue field R β§Έ πͺ. This is Mathlib's
ModuleCat.depth_eq_zero_iff_nontrivial_linearMap with the universe-adjusting Shrink in the
definition of IsLocalRing.depth removed.
A local ring of positive depth is not a field: its maximal ideal is nonzero. No Noetherian hypothesis is needed.
Dividing a module M by an M-regular element x lowers the depth by at most one. No
finiteness or Noetherian hypothesis is needed.
Dividing a finite module M over a Noetherian local ring by an M-regular element x of the
maximal ideal lowers the depth by exactly one.
If g : M β Q is a surjective linear map with kernel x M, then M β§Έ x M and Q have the
same depth.
Over a Noetherian local ring, let x in the maximal ideal be regular on a finite module M
and let g : M β Q be a surjective linear map with kernel x M. Then the depth of M is one
more than the depth of Q. This is IsLocalRing.depth_quotSMulTop_succ_eq_depth with the
quotient replaced by an isomorphic module.
Dividing a finite module M over a Noetherian local ring by an M-regular sequence
rβ, β¦, rβ lowers the depth by exactly n.
The depth of a finite module M over a Noetherian local ring is at most dim (R β§Έ p) for
every associated prime p of M. H. Matsumura, Commutative Ring Theory, Theorem 17.2.
The depth of a module over a Noetherian local ring is zero exactly when the maximal ideal is an associated prime of the module, that is, when some nonzero element is killed by the maximal ideal.
Over a Noetherian local ring, depth at least n β€ 2 passes from a finite target module
to the module of linear maps from a finite module. Stacks, Lemma 15.24.10 (0AV5).
Depth is unchanged under restriction of scalars along a surjective homomorphism of local rings
R β T: a finite T-module M has the same depth over R as over T. The M-regular
sequences in the maximal ideal of T are exactly the images of those in the maximal ideal of
R.
In a Noetherian local ring R of depth at least two, the maximal ideal is not an associated
prime of R β§Έ (b) for a nonzerodivisor b: if πͺ c β (b), then c β (b).
Algebraic Hartogs principle for fractions. Let R be a Noetherian local ring of depth at
least two with total ring of fractions K. An element of K that lies in the image of R_p for
every prime p other than the maximal ideal lies in R: if for every such p some t β p has
t x β R, then x β R.
Isomorphic Noetherian local rings have the same depth over themselves.
For a prime p of a commutative ring R, the module localization LocalizedModule p.primeCompl R has the same depth over R_p as the local ring R_p itself.
For a module M over a Noetherian ring R and a prime p, the localization M_p has depth
zero over R_p exactly when p is an associated prime of M.
For a module M over a Noetherian ring R and a prime p, the localization M_p has depth
at least one over R_p exactly when p is not an associated prime of M.
Let M be a finite module over a Noetherian ring and a an M-regular element of a prime
p. Dividing by a lowers the depth of the localization at p by exactly one:
depth (M β§Έ a M)_p + 1 = depth M_p.