diagram — Mathlib

English

For any functor I: D ⥤ Ideal R and any i, the diagram in modules has a colimit.

Русский

Для любой функторной схемы I: D ⥤ Ideal R и любого i диаграмма модулей обладает колимитом.

LaTeX

$$$HasColimit (diagram I i)$$$

Lean4

/-- The diagram we will take the colimit of to define local cohomology, corresponding to the
directed system determined by the functor `I` -/
def diagram (I : D ⥤ Ideal R) (i : ℕ) : Dᵒᵖ ⥤ ModuleCat.{u} R ⥤ ModuleCat.{u} R :=
  (ringModIdeals I).op ⋙ Ext R (ModuleCat.{u} R) i

Похожие утверждения