Depth of localized Hom modules #
For finite modules over a Noetherian ring, localization commutes with taking linear maps. Consequently a bound at most two on the depth of the localized target also bounds the depth of the localized Hom module. In particular a depth bound on the local ring passes to duals. This is useful for extending maps across subsets of codimension at least two.
References #
- Stacks Project, Lemma 15.24.10 (Tag 0AV5).
theorem
Ideal.le_depth_localizedModule_hom
{R M N : Type u}
[CommRing R]
[IsNoetherianRing R]
[AddCommGroup M]
[Module R M]
[Module.Finite R M]
[AddCommGroup N]
[Module R N]
[Module.Finite R N]
(p : Ideal R)
[p.IsPrime]
{N' : Type u}
[AddCommGroup N']
[Module R N']
[Module (Localization.AtPrime p) N']
[IsScalarTower R (Localization.AtPrime p) N']
(g : N →ₗ[R] N')
[IsLocalizedModule p.primeCompl g]
{n : ℕ}
(hn : n ≤ 2)
(hdepth : ↑n ≤ IsLocalRing.depth ↧N')
:
A depth bound at most two on a localized finite target passes to the localization of the module of linear maps from any finite module.
theorem
Ideal.le_depth_localizedModule_dual
{R M : Type u}
[CommRing R]
[IsNoetherianRing R]
[AddCommGroup M]
[Module R M]
[Module.Finite R M]
(p : Ideal R)
[p.IsPrime]
{n : ℕ}
(hn : n ≤ 2)
(hdepth : ↑n ≤ IsLocalRing.depth ↧(Localization.AtPrime p))
:
A depth bound at most two on a local ring passes to the localization of the dual of any finite module.