mathlib3 documentation

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.

References #

Tags #

local cohomology, local cohomology modules

Future work #

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
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
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
source
noncomputable def local_cohomology.diagram_comp {R : Type (max u v v')} [comm_ring R] {D : Type v} [category_theory.small_category D] {E : Type v'} [category_theory.small_category E] (I' : E ⥤ D) (I : D ⥤ ideal R) (i : ℕ) :
local_cohomology.diagram (I' ⋙ I) i ≅ I'.op ⋙ local_cohomology.diagram I i

Local cohomology along a composition of diagrams.

Equations
source
noncomputable def local_cohomology.iso_of_final {R : Type (max u v v')} [comm_ring R] {D : Type v} [category_theory.small_category D] {E : Type v'} [category_theory.small_category E] (I' : E ⥤ D) (I : D ⥤ ideal R) [I'.initial] (i : ℕ) :
local_cohomology.of_diagram (I' ⋙ I) i ≅ local_cohomology.of_diagram I i

Local cohomology agrees along precomposition with a cofinal diagram.

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

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

Showing equivalence of different definitions of local cohomology.

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
Instances for local_cohomology.ideal_powers_to_self_le_radical
source
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.

source
@[protected, instance]
def local_cohomology.ideal_powers_initial {R : Type u} [comm_ring R] {J : ideal R} [hR : is_noetherian R R] :
(local_cohomology.ideal_powers_to_self_le_radical J).initial

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

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

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

Equations
source
def local_cohomology.self_le_radical.cast {R : Type u} [comm_ring R] {J K : ideal R} (hJK : J.radical = K.radical) :
local_cohomology.self_le_radical J ⥤ local_cohomology.self_le_radical K

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

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

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

Local cohomology agrees on ideals with the same radical.

Equations