mathlib documentation

algebra.homology.local_cohomology

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 #

Tags #

local cohomology, local cohomology modules

Future work #

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

Equations
noncomputable def local_cohomology.diagram {R : Type u} [comm_ring R] {D : Type v} [category_theory.small_category D] (I : D ideal R) (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} [category_theory.small_category D] (I : D ideal R) (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

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

Equations

The full subcategory of all ideals with radical containing J

Equations
Instances for local_cohomology.self_le_radical

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

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

Equations
theorem 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

The lemma below essentially says that ideal_powers_to_self_le_radical I is initial in self_le_radical_diagram I.

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.