# 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*https://dept.math.lsa.umich.edu/~hochster/615W22/lcc.pdf - R. Hartshorne,
*Local cohomology: A seminar given by A. Grothendieck* - M. Brodmann and R. Sharp,
*Local cohomology: An algebraic introduction with geometric applications* - [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`

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

## Equations

- ⋯ = ⋯

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

## Equations

- localCohomology.diagram I i = (localCohomology.ringModIdeals I).op.comp (Ext R (ModuleCat R) 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`

.

## Equations

- localCohomology.ofDiagram I i = let_fun this := ⋯; CategoryTheory.Limits.colimit (localCohomology.diagram I i)

## Instances For

Local cohomology along a composition of diagrams.

## Equations

- localCohomology.diagramComp I' I i = CategoryTheory.Iso.refl (localCohomology.diagram (I'.comp I) i)

## Instances For

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

- localCohomology.idealPowersDiagram J = { obj := fun (t : ℕᵒᵖ) => J ^ Opposite.unop t, map := fun {X Y : ℕᵒᵖ} (w : X ⟶ Y) => { down := { down := ⋯ } }, map_id := ⋯, map_comp := ⋯ }

## Instances For

The full subcategory of all ideals with radical containing `J`

## Equations

- localCohomology.SelfLERadical J = CategoryTheory.FullSubcategory fun (J' : Ideal R) => J ≤ J'.radical

## Instances For

## Equations

- localCohomology.instCategorySelfLERadical J = CategoryTheory.FullSubcategory.category fun (J' : Ideal R) => J ≤ J'.radical

## Equations

- localCohomology.SelfLERadical.inhabited J = { 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

- localCohomology.selfLERadicalDiagram J = CategoryTheory.fullSubcategoryInclusion fun (J' : Ideal R) => J ≤ J'.radical

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

.

## Equations

## Instances For

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

- localCohomology.idealPowersToSelfLERadical J = CategoryTheory.FullSubcategory.lift (fun (J' : Ideal R) => J ≤ J'.radical) (localCohomology.idealPowersDiagram 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.

## Equations

- ⋯ = ⋯

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

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

## Equations

- ⋯ = ⋯

Local cohomology agrees on ideals with the same radical.