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][hochsterunpublished]
• [R. Hartshorne, Local cohomology: A seminar given by A. Grothendieck][hartshorne61]
• [M. Brodmann and R. Sharp, Local cohomology: An algebraic introduction with geometric applications][brodmannsharp13]
• [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
• Establish long exact sequence(s) in local cohomology

def localCohomology.ringModIdeals {R : Type u} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] (I : CategoryTheory.Functor D (Ideal R)) : CategoryTheory.Functor D (ModuleCat 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

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

instance localCohomology.moduleCat_enoughProjectives' {R : Type u} [CommRing R] : CategoryTheory.EnoughProjectives (ModuleCat R)

Equations

• ⋯ = ⋯

def localCohomology.diagram {R : Type u} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) : CategoryTheory.Functor Dᵒᵖ (CategoryTheory.Functor (ModuleCat R) (ModuleCat R))

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

Equations

• localCohomology.diagram I i = (localCohomology.ringModIdeals I).op.comp (Ext R (ModuleCat R) i)

theorem localCohomology.hasColimitDiagram {R : Type (max u v)} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) : CategoryTheory.Limits.HasColimit (localCohomology.diagram I i)

def localCohomology.ofDiagram {R : Type (max u v)} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) : CategoryTheory.Functor (ModuleCatMax R) (ModuleCatMax R)

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

• localCohomology.ofDiagram I i = let_fun this := ⋯; CategoryTheory.Limits.colimit (localCohomology.diagram I i)

def localCohomology.diagramComp {R : Type (max u v v')} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] {E : Type v'} [CategoryTheory.SmallCategory E] (I' : CategoryTheory.Functor E D) (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) : localCohomology.diagram (I'.comp I) i ≅ I'.op.comp (localCohomology.diagram I i)

Local cohomology along a composition of diagrams.

Equations

• localCohomology.diagramComp I' I i = CategoryTheory.Iso.refl (localCohomology.diagram (I'.comp I) i)

def localCohomology.isoOfFinal {R : Type (max u v v')} [CommRing R] {D : Type v} [CategoryTheory.SmallCategory D] {E : Type v'} [CategoryTheory.SmallCategory E] (I' : CategoryTheory.Functor E D) (I : CategoryTheory.Functor D (Ideal R)) [I'.Initial] (i : ℕ) : localCohomology.ofDiagram (I'.comp I) i ≅ localCohomology.ofDiagram I i

Local cohomology agrees along precomposition with a cofinal diagram.

Equations

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

def localCohomology.idealPowersDiagram {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.Functor ℕᵒᵖ (Ideal R)

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

Equations

• localCohomology.idealPowersDiagram J = { obj := fun (t : ℕᵒᵖ) => J ^ t.unop, map := fun {X Y : ℕᵒᵖ} (w : X ⟶ Y) => { down := { down := ⋯ } }, map_id := ⋯, map_comp := ⋯ }

def localCohomology.SelfLERadical {R : Type u} [CommRing R] (J : Ideal R) : Type u

The full subcategory of all ideals with radical containing J

Equations

• localCohomology.SelfLERadical J = CategoryTheory.FullSubcategory fun (J' : Ideal R) => J ≤ J'.radical

instance localCohomology.instCategorySelfLERadical {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.Category.{u, u} (localCohomology.SelfLERadical J)

Equations

• localCohomology.instCategorySelfLERadical J = CategoryTheory.FullSubcategory.category fun (J' : Ideal R) => J ≤ J'.radical

instance localCohomology.SelfLERadical.inhabited {R : Type u} [CommRing R] (J : Ideal R) : Inhabited (localCohomology.SelfLERadical J)

Equations

• localCohomology.SelfLERadical.inhabited J = { default := { obj := J, property := ⋯ } }

def localCohomology.selfLERadicalDiagram {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.Functor (localCohomology.SelfLERadical 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

• localCohomology.selfLERadicalDiagram J = CategoryTheory.fullSubcategoryInclusion fun (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 (localCohomology), then in terms of all ideals with radical containing J (localCohomology.ofSelfLERadical).

def localCohomology {R : Type u} [CommRing R] (J : Ideal R) (i : ℕ) : CategoryTheory.Functor (ModuleCat R) (ModuleCat R)

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

• localCohomology J i = localCohomology.ofDiagram (localCohomology.idealPowersDiagram J) i

def localCohomology.ofSelfLERadical {R : Type u} [CommRing R] (J : Ideal R) (i : ℕ) : CategoryTheory.Functor (ModuleCat R) (ModuleCat R)

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

Equations

• localCohomology.ofSelfLERadical J i = localCohomology.ofDiagram (localCohomology.selfLERadicalDiagram J) i

Showing equivalence of different definitions of local cohomology.

• localCohomology.isoSelfLERadical gives the isomorphism localCohomology J i ≅ localCohomology.ofSelfLERadical J i
• localCohomology.isoOfSameRadical gives the isomorphism localCohomology J i ≅ localCohomology K i when J.radical = K.radical.

def localCohomology.idealPowersToSelfLERadical {R : Type u} [CommRing R] (J : Ideal R) : CategoryTheory.Functor ℕᵒᵖ (localCohomology.SelfLERadical J)

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

Equations

• localCohomology.idealPowersToSelfLERadical J = CategoryTheory.FullSubcategory.lift (fun (J' : Ideal R) => J ≤ J'.radical) (localCohomology.idealPowersDiagram J) ⋯

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.

instance localCohomology.ideal_powers_initial {R : Type u} [CommRing R] {J : Ideal R} [hR : IsNoetherian R R] : (localCohomology.idealPowersToSelfLERadical J).Initial

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

Equations

• ⋯ = ⋯

def localCohomology.isoSelfLERadical {R : Type u} [CommRing R] (J : Ideal R) [IsNoetherian R R] (i : ℕ) : localCohomology.ofSelfLERadical J i ≅ localCohomology J i

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.

def localCohomology.SelfLERadical.cast {R : Type u} [CommRing R] {J : Ideal R} {K : Ideal R} (hJK : J.radical = K.radical) : CategoryTheory.Functor (localCohomology.SelfLERadical J) (localCohomology.SelfLERadical K)

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

Equations

• localCohomology.SelfLERadical.cast hJK = CategoryTheory.FullSubcategory.map ⋯

instance localCohomology.SelfLERadical.castIsEquivalence {R : Type u} [CommRing R] {J : Ideal R} {K : Ideal R} (hJK : J.radical = K.radical) : (localCohomology.SelfLERadical.cast hJK).IsEquivalence

Equations

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

def localCohomology.SelfLERadical.isoOfSameRadical {R : Type u} [CommRing R] {J : Ideal R} {K : Ideal R} (hJK : J.radical = K.radical) (i : ℕ) : localCohomology.ofSelfLERadical J i ≅ localCohomology.ofSelfLERadical K i

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

Equations

• localCohomology.SelfLERadical.isoOfSameRadical hJK i = (localCohomology.isoOfFinal (localCohomology.SelfLERadical.cast ⋯) (localCohomology.selfLERadicalDiagram J) i).symm

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

Local cohomology agrees on ideals with the same radical.

Equations

• localCohomology.isoOfSameRadical hJK i = (localCohomology.isoSelfLERadical J i).symm.trans ((localCohomology.SelfLERadical.isoOfSameRadical hJK i).trans (localCohomology.isoSelfLERadical K i))