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

source

def local_cohomology.ring_mod_ideals {R : Type u} [comm_ring R] {D : Type v} [category_theory.small_category D] (I : D ⥤ ideal R) :

D ⥤ Module R

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' := _}

source

@[protected, instance]

def local_cohomology.Module_enough_projectives' {R : Type u} [comm_ring R] :

category_theory.enough_projectives (Module R)

source

noncomputable def local_cohomology.diagram {R : Type u} [comm_ring R] {D : Type v} [category_theory.small_category D] (I : D ⥤ ideal R) (i : ℕ) :

Dᵒᵖ ⥤ Module R ⥤ Module R

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

source

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

Module R ⥤ Module R

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

local_cohomology.of_diagram I i = category_theory.limits.colimit (local_cohomology.diagram I i)

source

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

ℕ ᵒᵖ ⥤ ideal R

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

Equations

local_cohomology.ideal_powers_diagram J = {obj := λ (t : ℕ ᵒᵖ), J ^ opposite.unop t, map := λ (s t : ℕ ᵒᵖ) (w : s ⟶ t), {down := {down := _}}, map_id' := _, map_comp' := _}

source

@[protected, instance]

def local_cohomology.self_le_radical.category {R : Type u} [comm_ring R] (J : ideal R) :

category_theory.category (local_cohomology.self_le_radical J)

source

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

Type u

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

source

@[protected, instance]

def local_cohomology.self_le_radical.inhabited {R : Type u} [comm_ring R] (J : ideal R) :

inhabited (local_cohomology.self_le_radical J)

Equations

local_cohomology.self_le_radical.inhabited J = {default := {obj := J, property := _}}

source

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

local_cohomology.self_le_radical J ⥤ ideal R

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).

source

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

Module R ⥤ Module R

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

local_cohomology J i = local_cohomology.of_diagram (local_cohomology.ideal_powers_diagram J) i

source

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

Module R ⥤ Module R

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

Equations

local_cohomology.of_self_le_radical J i = local_cohomology.of_diagram (local_cohomology.self_le_radical_diagram J) i

source

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

ℕ ᵒᵖ ⥤ local_cohomology.self_le_radical J

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

Equations

local_cohomology.ideal_powers_to_self_le_radical J = category_theory.full_subcategory.lift (λ (J' : ideal R), J ≤ J'.radical) (local_cohomology.ideal_powers_diagram J) _

source

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

local_cohomology.ideal_powers_to_self_le_radical J ⋙ local_cohomology.self_le_radical_diagram J ≅ local_cohomology.ideal_powers_diagram J

The composition with the inclusion into ideals R is isomorphic to ideal_powers_diagram J.

Equations

local_cohomology.ideal_powers_to_self_le_radical_comp_inclusion J = category_theory.full_subcategory.lift_comp_inclusion (λ (J' : ideal R), J ≤ J'.radical) (local_cohomology.ideal_powers_diagram J) _

source

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.