Module

DerivedLocalCohomologyRadical.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyRadical

6 declarations indexed from sourceView source ↗

Module documentation

Radical invariance of derived local cohomology

The diagram of powers of an ideal is initial in the diagram of all ideals whose radical contains it. Applying the same cofinality argument as for Mathlib's legacy local cohomology shows that the derived-Ext colimit depends only on the radical of its support ideal.

Imports1

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomology

Imported by7

def

derivedLocalCohomologyDiagramComp

L28 ↗

EtaleFundamentalGroups.derivedLocalCohomologyDiagramComp

Documentation

Precomposing an ideal diagram gives the corresponding precomposition of the contravariant derived-Ext diagrams.

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v v'

Lean source · statement

def derivedLocalCohomologyDiagramComp
    {R : Type max u v v'} [CommRing R]
    {D : Type v} [SmallCategory D]
    {E : Type v'} [SmallCategory E]
    (F : E ⥤ D) (I : D ⥤ Ideal R)
    (M : ModuleCat.{max u v v'} R) (i : ℕ) :
    derivedLocalCohomologyDiagram (F ⋙ I) M i ≅
      F.op ⋙ derivedLocalCohomologyDiagram I M i

def

derivedLocalCohomologyIsoOfInitial

L41 ↗

EtaleFundamentalGroups.derivedLocalCohomologyIsoOfInitial

Documentation

Derived local cohomology is unchanged after precomposition by an initial functor (equivalently, after precomposition of the opposite diagram by a final functor).

Source context 4 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v v'

Lean source · statement

def derivedLocalCohomologyIsoOfInitial
    {R : Type max u v v'} [CommRing R]
    {D : Type v} [SmallCategory D]
    {E : Type v'} [SmallCategory E]
    (F : E ⥤ D) [Functor.Initial F] (I : D ⥤ Ideal R)
    (M : ModuleCat.{max u v v'} R) (i : ℕ) :
    derivedLocalCohomologyOfDiagram.{max u v, v'} (F ⋙ I) M i ≅
      derivedLocalCohomologyOfDiagram.{max u v', v} I M i

def

derivedLocalCohomologyOfSelfLERadical

L59 ↗

EtaleFundamentalGroups.derivedLocalCohomologyOfSelfLERadical

Documentation

The derived Ext colimit over all ideals whose radical contains I.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v v'
section Noetherian
variable {R : Type u} [CommRing R] [IsNoetherian R R]

Lean source · statement

def derivedLocalCohomologyOfSelfLERadical
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) : AddCommGrpCat.{u}

def

derivedLocalCohomologyIsoSelfLERadical

L65 ↗

EtaleFundamentalGroups.derivedLocalCohomologyIsoSelfLERadical

Documentation

The all-supports and powers models of derived local cohomology agree.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v v'
section Noetherian
variable {R : Type u} [CommRing R] [IsNoetherian R R]

Lean source · statement

def derivedLocalCohomologyIsoSelfLERadical
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    derivedLocalCohomologyOfSelfLERadical I M i ≅
      derivedLocalCohomology I M i

def

derivedLocalCohomologyOfSelfLERadicalIsoOfSameRadical

L76 ↗

EtaleFundamentalGroups.derivedLocalCohomologyOfSelfLERadicalIsoOfSameRadical

Documentation

The all-supports derived Ext colimits agree for ideals with the same radical.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v v'
section Noetherian
variable {R : Type u} [CommRing R] [IsNoetherian R R]

Lean source · statement

def derivedLocalCohomologyOfSelfLERadicalIsoOfSameRadical
    {I J : Ideal R} (hIJ : I.radical = J.radical)
    (M : ModuleCat.{u} R) (i : ℕ) :
    derivedLocalCohomologyOfSelfLERadical I M i ≅
      derivedLocalCohomologyOfSelfLERadical J M i

def

derivedLocalCohomologyIsoOfSameRadical

L87 ↗

EtaleFundamentalGroups.derivedLocalCohomologyIsoOfSameRadical

Documentation

The derived local-cohomology object depends only on the radical of its support ideal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u v v'
section Noetherian
variable {R : Type u} [CommRing R] [IsNoetherian R R]

Lean source · statement

def derivedLocalCohomologyIsoOfSameRadical
    {I J : Ideal R} (hIJ : I.radical = J.radical)
    (M : ModuleCat.{u} R) (i : ℕ) :
    derivedLocalCohomology I M i ≅ derivedLocalCohomology J M i

Module documentation

Radical invariance of derived local cohomology

Declarations

derivedLocalCohomologyDiagramComp

derivedLocalCohomologyIsoOfInitial

derivedLocalCohomologyOfSelfLERadical

derivedLocalCohomologyIsoSelfLERadical

derivedLocalCohomologyOfSelfLERadicalIsoOfSameRadical

derivedLocalCohomologyIsoOfSameRadical