instIsMultiplicativeSchemeUniversallyClosed

Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsMultiplicativeSchemeUniversallyClosed

English

UniversallyClosed is multiplicative: the property is preserved under identity and composition of morphisms.

Русский

UniversallyClosed мультипликативно: свойство сохраняется при тождественных и композиционных морфизмах.

LaTeX

$$$\\mathrm{IsMultiplicative}(\\mathrm{UniversallyClosed})$$$

Lean4

instance : MorphismProperty.IsMultiplicative @UniversallyClosed where id_mem _ := inferInstance

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

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

Разделы

Аффилиация

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