range_subschemeι

Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme

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

English

The range of the base map I.subschemeι.base equals the support of I, i.e., Supp(I).

Русский

Область образа базисного отображения I.subschemeι.base равна поддержке I, то есть Supp(I).

LaTeX

$$$\mathrm{range}(I.subschemeι.base) = \mathrm{Supp}(I)$$$

Lean4

@[simp]
theorem range_subschemeι : Set.range I.subschemeι.base = I.support := by
  simp [← range_gluedTo, I.subschemeι_def, Set.range_comp]

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

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

Разделы

Аффилиация

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