Documentation

Mathlib.Algebra.Homology.LocalCohomology

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

Instances For

    The diagram we will take the colimit of to define local cohomology, corresponding to the directed system determined by the functor I

    Instances For

      localCohomology.ofDiagram I i is 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.

      Instances For

        Local cohomology along a composition of diagrams.

        Instances For

          Local cohomology agrees along precomposition with a cofinal diagram.

          Instances For

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

            Instances For

              The full subcategory of all ideals with radical containing J

              Instances For

                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.

                Instances For

                  We give two models for the local cohomology with support in an ideal J: first in terms of the powers of J (localCohomology), then in terms of all ideals with radical containing J (localCohomology.ofSelfLERadical).

                  localCohomology 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 : ℕ.

                  Instances For

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

                    Instances For

                      Showing equivalence of different definitions of local cohomology.

                      Lifting idealPowersDiagram J from a diagram valued in ideals R to a diagram valued in SelfLERadical J.

                      Instances For
                        theorem localCohomology.Ideal.exists_pow_le_of_le_radical_of_fG {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (hIJ : I Ideal.radical J) (hJ : Ideal.FG (Ideal.radical J)) :
                        k, I ^ k J

                        The lemma below essentially says that idealPowersToSelfLERadical I is initial in selfLERadicalDiagram I.

                        PORTING NOTE: This lemma should probably be moved to Mathlib/RingTheory/Finiteness to be near Ideal.exists_radical_pow_le_of_fg, which it generalizes.

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

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

                        Instances For

                          Casting from the full subcategory of ideals with radical containing J to the full subcategory of ideals with radical containing K.

                          Instances For

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

                            Instances For

                              Local cohomology agrees on ideals with the same radical.

                              Instances For