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
- Prove that local cohomology depends only on the radical of the ideal
- 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
- local_cohomology.ring_mod_ideals I = {obj := λ (t : D), Module.of R (R ⧸ I.obj t), map := λ (s t : D) (w : s ⟶ t), submodule.mapq (I.obj s) (I.obj t) linear_map.id _, map_id' := _, map_comp' := _}
The diagram we will take the colimit of to define local cohomology, corresponding to the
directed system determined by the functor I
Equations
- local_cohomology.diagram I i = (local_cohomology.ring_mod_ideals I).op ⋙ Ext R (Module 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
The full subcategory of all ideals with radical containing J
Equations
- local_cohomology.self_le_radical J = category_theory.full_subcategory (λ (J' : ideal R), J ≤ J'.radical)
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
- local_cohomology.self_le_radical_diagram J = category_theory.full_subcategory_inclusion (λ (J' : ideal R), J ≤ J'.radical)
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
).
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
Lifting ideal_powers_diagram J
from a diagram valued in ideals R
to a diagram
valued in self_le_radical J
.
Equations
The composition with the inclusion into ideals R
is isomorphic to ideal_powers_diagram J
.
Equations
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.