instAB4StarModuleCat — Mathlib

English

In the category of left modules over a ring R, the AB4* property holds: small products preserve exact sequences, i.e., products of exact sequences are exact.

Русский

В категории левых модулей над кольцом R выполняется свойство AB4*: произведения точных последовательностей сохраняют точность.

LaTeX

$$$\mathrm{AB4}^*(\mathrm{ModuleCat}(R))$$$

Lean4

instance : AB4Star (ModuleCat.{u} R) where
  ofShape J := HasExactLimitsOfShape.domain_of_functor (Discrete J) (forget₂ (ModuleCat R) AddCommGrpCat.{u})

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