strictMono_ideal

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal

English

If I < J for ideal data on a scheme X, then I.ideal < J.ideal.

Русский

Если I < J для данных идеалов на схеме X, то I.ideal < J.ideal.

LaTeX

$$$ I < J \Rightarrow I.ideal < J.ideal $$$

Lean4

theorem strictMono_ideal : StrictMono (ideal (X := X)) :=
  IdealSheafData.gci.strictMono_l

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

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

Разделы

Аффилиация

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