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 https://dept.math.lsa.umich.edu/~hochster/615W22/lcc.pdf
• R. Hartshorne, Local cohomology: A seminar given by A. Grothendieck
• M. Brodmann and R. Sharp, Local cohomology: An algebraic introduction with geometric applications
• [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

@[implicit_reducible]

def localCohomology.ringModIdeals {R : Type u} [CommRing R] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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.

@[simp]

theorem localCohomology.ringModIdeals_map {R : Type u} [CommRing R] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (I : CategoryTheory.Functor D (Ideal R)) {X✝ Y✝ : D} (w : X✝ ⟶ Y✝) : (ringModIdeals I).map w = ModuleCat.ofHom (Submodule.mapQ (I.obj X✝) (I.obj Y✝) LinearMap.id ⋯)

@[simp]

theorem localCohomology.ringModIdeals_obj_carrier {R : Type u} [CommRing R] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (I : CategoryTheory.Functor D (Ideal R)) (t : D) : ↑((ringModIdeals I).obj t) = (R ⧸ I.obj t)

@[reducible, inline]

noncomputable abbrev localCohomology.diagram {R : Type u} [CommRing R] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} 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)

def localCohomology.ringModIdealComp {R : Type u} [CommRing R] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (I' : CategoryTheory.Functor E D) (I : CategoryTheory.Functor D (Ideal R)) : ringModIdeals (I'.comp I) ≅ I'.comp (ringModIdeals I)

The diagram ringModIdeals (I' ⋙ I) is isomorphism (in fact, definitionally equal) to the the diagram I' ⋙ ringModIdeals I.

Equations

• localCohomology.ringModIdealComp I' I = CategoryTheory.NatIso.ofComponents (fun (x : E) => CategoryTheory.Iso.refl ((localCohomology.ringModIdeals (I'.comp I)).obj x)) ⋯

@[reducible, inline]

noncomputable abbrev localCohomology.ofDiagram {R : Type u} [CommRing R] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] (I : CategoryTheory.Functor D (Ideal R)) (i : ℕ) [CategoryTheory.Limits.HasColimit (diagram I i)] : CategoryTheory.Functor (ModuleCat R) (ModuleCat 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 = CategoryTheory.Limits.colimit (localCohomology.diagram I i)

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

Local cohomology along a composition of diagrams.

Equations

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

@[reducible, inline]

noncomputable abbrev localCohomology.isoOfFinal {R : Type u} [CommRing R] {D : Type u₁} [CategoryTheory.Category.{v₁, u₁} D] {E : Type u₂} [CategoryTheory.Category.{v₂, u₂} E] (I' : CategoryTheory.Functor E D) (I : CategoryTheory.Functor D (Ideal R)) [I'.Initial] (i : ℕ) [CategoryTheory.Limits.HasColimit (diagram (I'.comp I) i)] [CategoryTheory.Limits.HasColimit (diagram I i)] : ofDiagram (I'.comp I) i ≅ 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 ^ Opposite.unop t, 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.ObjectProperty.FullSubcategory fun (J' : Ideal R) => J ≤ J'.radical

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Equations

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

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

noncomputable 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

noncomputable 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 ℕᵒᵖ (SelfLERadical J)

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

Equations

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

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

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

noncomputable def localCohomology.isoSelfLERadical {R : Type u} [CommRing R] (J : Ideal R) [IsNoetherian R R] (i : ℕ) : 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 K : Ideal R} (hJK : J.radical = K.radical) : CategoryTheory.Functor (SelfLERadical J) (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.ObjectProperty.ιOfLE ⋯

noncomputable def localCohomology.SelfLERadical.castEquivalence {R : Type u} [CommRing R] {J K : Ideal R} (hJK : J.radical = K.radical) : SelfLERadical J ≌ SelfLERadical K

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.

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

noncomputable def localCohomology.SelfLERadical.isoOfSameRadical {R : Type u} [CommRing R] {J K : Ideal R} (hJK : J.radical = K.radical) (i : ℕ) : ofSelfLERadical J i ≅ 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

noncomputable def localCohomology.isoOfSameRadical {R : Type u} [CommRing R] {J 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 ≪≫ localCohomology.SelfLERadical.isoOfSameRadical hJK i ≪≫ localCohomology.isoSelfLERadical K i