Local cohomology.

This file defines the i-th local cohomology module of an R-module M with support in an ideal I of R, where R is a commutative ring, as the direct limit of Ext modules:

Given a collection of ideals cofinal with the powers of I, consider the directed system of quotients of R by these ideals, and take the direct limit of the system induced on the i-th Ext into M. One can, of course, take the collection to simply be the integral powers of I.

References

• [M. Hochster, Local cohomology][hochsterunpublished] https://dept.math.lsa.umich.edu/~hochster/615W22/lcc.pdf
• [R. Hartshorne, Local cohomology: A seminar given by A. Grothendieck][hartshorne61]
• [M. Brodmann and R. Sharp, Local cohomology: An algebraic introduction with geometric applications][brodmannsharp13]
• [S. Iyengar, G. Leuschke, A. Leykin, Anton, C. Miller, E. Miller, A. Singh, U. Walther, Twenty-four hours of local cohomology][iyengaretal13]

Tags

local cohomology, local cohomology modules

Future work

• Prove that this definition is equivalent to:
  • the right-derived functor definition
  • the characterization as the limit of Koszul homology
  • the characterization as the cohomology of a Cech-like complex
• Establish long exact sequence(s) in local cohomology

def localCohomology.ringModIdeals {R : Type u} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] (I : CategoryTheory.Functor D (Ideal R)) : CategoryTheory.Functor D (ModuleCat R)

The directed system of R-modules of the form R/J, where J is an ideal of R, determined by the functor I

noncomputable def localCohomology.diagram {R : Type u} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) : CategoryTheory.Functor Dᵒᵖ (CategoryTheory.Functor (ModuleCat R) (ModuleCat R))

The diagram we will take the colimit of to define local cohomology, corresponding to the directed system determined by the functor I

theorem localCohomology.hasColimitDiagram {R : Type (max u v)} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) : CategoryTheory.Limits.HasColimit (diagram I i)

noncomputable def localCohomology.ofDiagram {R : Type (max u v)} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) : CategoryTheory.Functor (ModuleCat R) (ModuleCat R)

localCohomology.ofDiagram I i is the functor sending a module M over a commutative ring R to the direct limit of Ext^i(R/J, M), where J ranges over a collection of ideals of R, represented as a functor I.

noncomputable def localCohomology.diagramComp {R : Type (max u v v')} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] {E : Type v'} [CategoryTheory.SmallCategory E] (I' : CategoryTheory.Functor E D) (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) : diagram (I'.comp I) i ≅ I'.op.comp (diagram I i)

Local cohomology along a composition of diagrams.

noncomputable def localCohomology.isoOfFinal {R : Type (max u v v')} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] {E : Type v'} [CategoryTheory.SmallCategory E] (I' : CategoryTheory.Functor E D) (I : CategoryTheory.Functor D (Ideal R)) [I'.Initial] (i : ℕ) : ofDiagram (I'.comp I) i ≅ ofDiagram I i

Local cohomology agrees along precomposition with a cofinal diagram.

def localCohomology.idealPowersDiagram {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.Functor ℕᵒᵖ (Ideal R)

The functor sending a natural number i to the i-th power of the ideal J

def localCohomology.SelfLERadical {R : Type u} [CommRing R] (J : Ideal R) : Type u

The full subcategory of all ideals with radical containing J

@[implicit_reducible]

noncomputable instance localCohomology.instCategorySelfLERadical {R : Type u_1} [CommRing R] (J : Ideal R) : CategoryTheory.Category.{u_1, u_1} (SelfLERadical J)

@[implicit_reducible]

instance localCohomology.SelfLERadical.inhabited {R : Type u} [CommRing R] (J : Ideal R) : Inhabited (SelfLERadical J)

def localCohomology.selfLERadicalDiagram {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.Functor (SelfLERadical J) (Ideal R)

The diagram of all ideals with radical containing J, represented as a functor. This is the "largest" diagram that computes local cohomology with support in J.

We give two models for the local cohomology with support in an ideal J: first in terms of the powers of J (localCohomology), then in terms of all ideals with radical containing J (localCohomology.ofSelfLERadical).

noncomputable def localCohomology {R : Type u} [CommRing R] (J : Ideal R) (i : ℕ) : CategoryTheory.Functor (ModuleCat R) (ModuleCat R)

localCohomology J i is i-th the local cohomology module of a module M over a commutative ring R with support in the ideal J of R, defined as the direct limit of Ext^i(R/J^t, M) over all powers t : ℕ.

noncomputable def localCohomology.ofSelfLERadical {R : Type u} [CommRing R] (J : Ideal R) (i : ℕ) : CategoryTheory.Functor (ModuleCat R) (ModuleCat R)

Local cohomology as the direct limit of Ext^i(R/J', M) over all ideals J' with radical containing J.

Showing equivalence of different definitions of local cohomology.

• localCohomology.isoSelfLERadical gives the isomorphism localCohomology J i ≅ localCohomology.ofSelfLERadical J i
• localCohomology.isoOfSameRadical gives the isomorphism localCohomology J i ≅ localCohomology K i when J.radical = K.radical.

def localCohomology.idealPowersToSelfLERadical {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.Functor ℕᵒᵖ (SelfLERadical J)

Lifting idealPowersDiagram J from a diagram valued in ideals R to a diagram valued in SelfLERadical J.

instance localCohomology.ideal_powers_initial {R : Type u} [CommRing R] {J : Ideal R} [hR : IsNoetherian R R] : (idealPowersToSelfLERadical J).Initial

The diagram of powers of J is initial in the diagram of all ideals with radical containing J. This uses Noetherianness.

noncomputable def localCohomology.isoSelfLERadical {R : Type u} [CommRing R] (J : Ideal R) [IsNoetherian R R] (i : ℕ) : ofSelfLERadical J i ≅ localCohomology J i

Local cohomology (defined in terms of powers of J) agrees with local cohomology computed over all ideals with radical containing J.

def localCohomology.SelfLERadical.cast {R : Type u} [CommRing R] {J K : Ideal R} (hJK : J.radical = K.radical) : CategoryTheory.Functor (SelfLERadical J) (SelfLERadical K)

Casting from the full subcategory of ideals with radical containing J to the full subcategory of ideals with radical containing K.

noncomputable def localCohomology.SelfLERadical.castEquivalence {R : Type u} [CommRing R] {J K : Ideal R} (hJK : J.radical = K.radical) : SelfLERadical J ≌ SelfLERadical K

The equivalence of categories SelfLERadical J ≌ SelfLERadical K when J.radical = K.radical.

instance localCohomology.SelfLERadical.cast_isEquivalence {R : Type u} [CommRing R] {J K : Ideal R} (hJK : J.radical = K.radical) : (cast hJK).IsEquivalence

noncomputable def localCohomology.SelfLERadical.isoOfSameRadical {R : Type u} [CommRing R] {J K : Ideal R} (hJK : J.radical = K.radical) (i : ℕ) : ofSelfLERadical J i ≅ ofSelfLERadical K i

The natural isomorphism between local cohomology defined using the of_self_le_radical diagram, assuming J.radical = K.radical.

noncomputable def localCohomology.isoOfSameRadical {R : Type u} [CommRing R] {J K : Ideal R} [IsNoetherian R R] (hJK : J.radical = K.radical) (i : ℕ) : localCohomology J i ≅ localCohomology K i

Local cohomology agrees on ideals with the same radical.