English
The diagram directLimitDiagram encodes an unbundled direct limit of modules: it assigns G(i) to i and maps f(i,j) to arrows G(i) → G(j).
Русский
Диаграмма directLimitDiagram кодирует неразвернутый прямой предел модулей: каждому i ставится G(i), а стрелкам сопоставляются линейные отображения f(i,j).
LaTeX
$$$\\text{directLimitDiagram}: ι \\mapsto \\mathrm{ModuleCat}.of(R)(G(i)), \\; hij \\mapsto \\mathrm{ofHom}(f_i_j)$$$$
Lean4
/-- The diagram (in the sense of `CategoryTheory`) of an unbundled `directLimit` of modules. -/
@[simps]
def directLimitDiagram : ι ⥤ ModuleCat R where
obj i := ModuleCat.of R (G i)
map hij := ofHom (f _ _ hij.le)
map_id
i := by
ext
apply Module.DirectedSystem.map_self
map_comp hij
hjk := by
ext
symm
apply Module.DirectedSystem.map_map f
