English
Local cohomology along a diagram is defined as the functor sending a module M to the colimit of the diagram diagram I i, i.e., Ext-directed system along J.
Русский
Локальная когомология вдоль диаграммы задаётся как предел (колимит) соответствующей диаграммы, получаемой из Ext-цепи по J.
LaTeX
$$$\\text{ofDiagram } I\; i := \\text{colim }( \\text{diagram } I\; i)$$$
Lean4
/-- `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`. -/
def ofDiagram (I : D ⥤ Ideal R) (i : ℕ) : ModuleCat.{max u v} R ⥤ ModuleCat.{max u v} R :=
have := hasColimitDiagram.{u, v} I i
colimit (diagram I i)
