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 #

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
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 along a composition of diagrams.

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

Showing equivalence of different definitions of local cohomology.

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]

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

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

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

Equations