ideal_le_comap_ideal

Mathlib.AlgebraicGeometry.IdealSheaf.Basic

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

← MathLib Explorer

English

For U ≤ V, I.ideal(V) ≤ comap(res map)(I.ideal(U)).

Русский

Для U ≤ V: I.ideal(V) ≤ comap(ограничение)(I.ideal(U)).

LaTeX

$$$ I.ideal V \le (I.ideal U).comap (X.presheaf.map (homOfLE h).op).hom $$$

Lean4

theorem ideal_le_comap_ideal {U V : X.affineOpens} (h : U ≤ V) :
    I.ideal V ≤ (I.ideal U).comap (X.presheaf.map (homOfLE h).op).hom := by
  rw [← Ideal.map_le_iff_le_comap, ← I.map_ideal h]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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