hasFiniteColimits — Mathlib

English

PresheafOfModules has finite colimits; this extends the existence of finite colimits from the base category to presheaves of modules.

Русский

PresheafOfModules имеет конечные колимиты; следствие распространения существования конечных колимитов на прешейфы модулей.

LaTeX

$$$\\text{HasFiniteColimits}(\\text{PresheafOfModules}(R))$$$

Lean4

instance hasFiniteColimits : HasFiniteColimits (PresheafOfModules.{v} R) :=
  ⟨fun _ => inferInstance⟩

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