# mathlib3documentation

algebra.homology.local_cohomology

# Local cohomology. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 local_cohomology.ring_mod_ideals {R : Type u} [comm_ring R] {D : Type v} (I : D ) :
D

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

Equations
@[protected, instance]
noncomputable def local_cohomology.diagram {R : Type u} [comm_ring R] {D : Type v} (I : D ) (i : ) :

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

Equations
noncomputable def local_cohomology.of_diagram {R : Type (max u v)} [comm_ring R] {D : Type v} (I : D ) (i : ) :

local_cohomology.of_diagram I i is the 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
noncomputable def local_cohomology.diagram_comp {R : Type (max u v v')} [comm_ring R] {D : Type v} {E : Type v'} (I' : E D) (I : D ) (i : ) :

Local cohomology along a composition of diagrams.

Equations
noncomputable def local_cohomology.iso_of_final {R : Type (max u v v')} [comm_ring R] {D : Type v} {E : Type v'} (I' : E D) (I : D ) [I'.initial] (i : ) :

Local cohomology agrees along precomposition with a cofinal diagram.

Equations

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

Equations
@[protected, instance]

The full subcategory of all ideals with radical containing J

Equations
Instances for local_cohomology.self_le_radical
@[protected, instance]
Equations

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

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

noncomputable def local_cohomology {R : Type u} [comm_ring R] (J : ideal R) (i : ) :

local_cohomology 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
noncomputable def local_cohomology.of_self_le_radical {R : Type u} [comm_ring R] (J : ideal R) (i : ) :

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

Equations

Showing equivalence of different definitions of local cohomology.

• local_cohomology.iso_self_le_radical gives the isomorphism local_cohomology J i ≅ local_cohomology.of_self_le_radical J i
• local_cohomology.iso_of_same_radical gives the isomorphism local_cohomology J i ≅ local_cohomology K i when J.radical = K.radical.

Lifting ideal_powers_diagram J from a diagram valued in ideals R to a diagram valued in self_le_radical J.

Equations
Instances for local_cohomology.ideal_powers_to_self_le_radical
theorem local_cohomology.ideal.exists_pow_le_of_le_radical_of_fg {R : Type u} [comm_ring R] {I J : ideal R} (hIJ : I J.radical) (hJ : J.radical.fg) :
(k : ), I ^ k J

PORTING NOTE: This lemma should probably be moved to ring_theory/finiteness.lean to be near ideal.exists_radical_pow_le_of_fg, which it generalizes.

@[protected, instance]
def local_cohomology.ideal_powers_initial {R : Type u} [comm_ring R] {J : ideal R} [hR : R] :

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

noncomputable def local_cohomology.iso_self_le_radical {R : Type u} [comm_ring R] (J : ideal R) [ R] (i : ) :

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

Equations
def local_cohomology.self_le_radical.cast {R : Type u} [comm_ring R] {J K : ideal R} (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 local_cohomology.self_le_radical.cast
@[protected, instance]
Equations
noncomputable def local_cohomology.self_le_radical.iso_of_same_radical {R : Type u} [comm_ring R] {J K : ideal R} (hJK : J.radical = K.radical) (i : ) :

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

Equations
noncomputable def local_cohomology.iso_of_same_radical {R : Type u} [comm_ring R] {J K : ideal R} [ R] (hJK : J.radical = K.radical) (i : ) :

Local cohomology agrees on ideals with the same radical.

Equations