instHasCoequalizer

Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.LocallyRingedSpace.instHasCoequalizer

English

The category LocallyRingedSpace has all small colimits.

Русский

Категория LocallyRingedSpace имеет все малые колимиты.

LaTeX

$$HasColimits LocallyRingedSpace$$

Lean4

instance : HasCoequalizer f g :=
  ⟨⟨⟨_, coequalizerCoforkIsColimit f g⟩⟩⟩

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru