# 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

The directed system of `R`

-modules of the form `R/J`

, where `J`

is an ideal of `R`

,
determined by the functor `I`

## Instances For

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

## Instances For

`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`

.

## Instances For

Local cohomology along a composition of diagrams.

## Instances For

Local cohomology agrees along precomposition with a cofinal diagram.

## Instances For

The functor sending a natural number `i`

to the `i`

-th power of the ideal `J`

## Instances For

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`

.

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

).

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

.

## Instances For

Local cohomology as the direct limit of `Ext^i(R/J', M)`

over *all* ideals `J'`

with radical
containing `J`

.

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

.

## Instances For

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.

The diagram of powers of `J`

is initial in the diagram of all ideals with
radical containing `J`

. This uses noetherianness.

Local cohomology (defined in terms of powers of `J`

) agrees with local
cohomology computed over all ideals with radical containing `J`

.

## Instances For

Casting from the full subcategory of ideals with radical containing `J`

to the full
subcategory of ideals with radical containing `K`

.

## Instances For

The natural isomorphism between local cohomology defined using the `of_self_le_radical`

diagram, assuming `J.radical = K.radical`

.

## Instances For

Local cohomology agrees on ideals with the same radical.