# 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.

## 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} [] {D : Type v} (I : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
Equations
• =
def localCohomology.diagram {R : Type u} [] {D : Type v} (I : ) (i : ) :

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

Equations
Instances For
theorem localCohomology.hasColimitDiagram {R : Type (max u v)} [] {D : Type v} (I : ) (i : ) :
def localCohomology.ofDiagram {R : Type (max u v)} [] {D : Type v} (I : ) (i : ) :

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.

Equations
• = let_fun this := ;
Instances For
def localCohomology.diagramComp {R : Type (max u v v')} [] {D : Type v} {E : Type v'} (I' : ) (I : ) (i : ) :
localCohomology.diagram (I'.comp I) i I'.op.comp

Local cohomology along a composition of diagrams.

Equations
Instances For
def localCohomology.isoOfFinal {R : Type (max u v v')} [] {D : Type v} {E : Type v'} (I' : ) (I : ) [I'.Initial] (i : ) :

Local cohomology agrees along precomposition with a cofinal diagram.

Equations
• One or more equations did not get rendered due to their size.
Instances For

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

Equations
• = { obj := fun (t : ) => , map := fun {X Y : } (w : X Y) => { down := { down := } }, map_id := , map_comp := }
Instances For
def localCohomology.SelfLERadical {R : Type u} [] (J : ) :

The full subcategory of all ideals with radical containing J

Equations
Instances For
instance localCohomology.instCategorySelfLERadical {R : Type u} [] (J : ) :
Equations
instance localCohomology.SelfLERadical.inhabited {R : Type u} [] (J : ) :
Equations
• = { default := { obj := J, property := } }

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.

Equations
Instances For

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).

def localCohomology {R : Type u} [] (J : ) (i : ) :

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 : ℕ.

Equations
Instances For
def localCohomology.ofSelfLERadical {R : Type u} [] (J : ) (i : ) :

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

Equations
Instances For

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.

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

Equations
Instances For
theorem localCohomology.Ideal.exists_pow_le_of_le_radical_of_fG {R : Type u} [] {I : } {J : } (hIJ : I J.radical) (hJ : J.radical.FG) :
∃ (k : ), I ^ k J

The lemma below essentially says that idealPowersToSelfLERadical I is initial in selfLERadicalDiagram I.

Porting note: This lemma should probably be moved to Mathlib/RingTheory/Finiteness to be near Ideal.exists_radical_pow_le_of_fg, which it generalizes.

instance localCohomology.ideal_powers_initial {R : Type u} [] {J : } [hR : ] :
.Initial

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

Equations
• =
def localCohomology.isoSelfLERadical {R : Type u} [] (J : ) [] (i : ) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
def localCohomology.SelfLERadical.cast {R : Type u} [] {J : } {K : } (hJK : J.radical = K.radical) :

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

Equations
Instances For
def localCohomology.SelfLERadical.castEquivalence {R : Type u} [] {J : } {K : } (hJK : J.radical = K.radical) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
instance localCohomology.SelfLERadical.cast_isEquivalence {R : Type u} [] {J : } {K : } (hJK : J.radical = K.radical) :
.IsEquivalence
Equations
• =
The natural isomorphism between local cohomology defined using the of_self_le_radical diagram, assuming J.radical = K.radical.