Spec_faithful

Mathlib.AlgebraicGeometry.AffineScheme

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.AffineScheme.Spec_faithful

English

The Spec functor is faithful, i.e., distinct morphisms are distinguished by their Spec-images.

Русский

Функтор Spec верен: различные морфизмы различаются по изображениям в Spec.

LaTeX

$$Spec.Faithful$$

Lean4

instance Spec_faithful : Spec.Faithful :=
  Functor.Faithful.toEssImage _

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

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

Разделы

Аффилиация

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