moduleCategory — Mathlib

English

There is a category structure on ModuleCat(R): objects are R-modules, morphisms are module homomorphisms; composition is composition of linear maps and identities are identity maps.

Русский

Существует структура категории на ModuleCat(R): объекты — это R-модули, морфизмы — это гомоморфизмы модулей; композиция — это композиция линейных отображений, тождественные отображения — тождественные отображения.

LaTeX

$$$ \\mathrm{Hom}_{ModuleCat(R)}(M,N) = \\mathrm{Hom}_R(M,N), \\; \\mathrm{id}_M = \\mathrm{id}_{M}, \\; \\mathrm{comp}(f,g) = g \\circ f.$$$

Lean4

instance moduleCategory : Category.{v, max (v + 1) u} (ModuleCat.{v} R)
    where
  Hom M N := Hom M N
  id _ := ⟨LinearMap.id⟩
  comp f g := ⟨g.hom'.comp f.hom'⟩

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