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

Equations
  • One or more equations did not get rendered due to their size.
Instances For

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

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

      Equations
      Instances For

        Local cohomology along a composition of diagrams.

        Equations
        Instances For

          Local cohomology agrees along precomposition with a cofinal diagram.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

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

            Equations
            Instances For

              The full subcategory of all ideals with radical containing J

              Equations
              Instances For
                Equations

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

                  Equations
                  Instances For

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

                    Equations
                    Instances For

                      Showing equivalence of different definitions of local cohomology.

                      theorem localCohomology.Ideal.exists_pow_le_of_le_radical_of_fG {R : Type u} [CommRing R] {I : Ideal R} {J : Ideal R} (hIJ : I J.radical) (hJ : J.radical.FG) :
                      ∃ (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.

                      Equations
                      • =

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

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

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

                        Equations
                        Instances For

                          The equivalence of categories SelfLERadical J ≌ SelfLERadical K when J.radical = K.radical.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            instance localCohomology.SelfLERadical.cast_isEquivalence {R : Type u} [CommRing R] {J : Ideal R} {K : Ideal R} (hJK : J.radical = K.radical) :
                            Equations
                            • =

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

                            Equations
                            Instances For
                              def localCohomology.isoOfSameRadical {R : Type u} [CommRing R] {J : Ideal R} {K : Ideal R} [IsNoetherian R R] (hJK : J.radical = K.radical) (i : ) :

                              Local cohomology agrees on ideals with the same radical.

                              Equations
                              Instances For