ringModIdeals — Mathlib

English

For a diagram I: D ⥤ Ideal R, and a fixed i, one constructs a directed system of modules Ext^i(R/J, M) along I, forming a diagram valued in module categories.

Русский

Для диаграммы I: D ⥤ Ideal R и фиксированного i строится направленная система модулей Ext^i(R/J, M) вдоль I, образующая диаграмму значений в модулях.

LaTeX

$$$\\text{diagram } I\, i : D^{op} \\to \\text{ModuleCat } R$$$

Lean4

/-- The directed system of `R`-modules of the form `R/J`, where `J` is an ideal of `R`,
determined by the functor `I` -/
def ringModIdeals (I : D ⥤ Ideal R) : D ⥤ ModuleCat.{u} R
    where
  obj t := ModuleCat.of R <| R ⧸ I.obj t
  map w := ModuleCat.ofHom <| Submodule.mapQ _ _ LinearMap.id (I.map w).down.down

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