hasColimitsOfSize — Mathlib

English

If AddCommGrpCat has ColimitsOfSize J, then ModuleCat R also has ColimitsOfSize J for rings R.

Русский

Если в AddCommGrpCat существуют колимиты заданного размера J, то в ModuleCat R тоже существуют колимиты размера J для колец R.

LaTeX

$$$$ \text{HasColimitsOfSize } J (\mathrm{ModuleCat}(R)) $$$$

Lean4

instance hasColimitsOfSize [HasColimitsOfSize.{v, u} AddCommGrpCat.{w'}] : HasColimitsOfSize.{v, u} (ModuleCat.{w'} R)
    where

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