instConcreteCategoryLinearMapIdCarrier

English

The category structure on ModuleCat(R) satisfies associativity and identity laws for composition and identities.

Русский

Структура категории на ModuleCat(R) удовлетворяет законам ассоциативности и тождественности для композиции и тождественных морфизмов.

LaTeX

$$$ \\text{Associativity and identity laws hold for composition in } \\mathrm{ModuleCat}(R). $$$

Lean4

instance : ConcreteCategory (ModuleCat.{v} R) (· →ₗ[R] ·)
    where
  hom := Hom.hom'
  ofHom := Hom.mk

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