le_map_comap

Mathlib.AlgebraicGeometry.IdealSheaf.Functorial

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

English

For I, J ideals with a fixed f, comap_map_le expresses a fundamental inequality between (I.map f).comap f and I.

Русский

Для идеалов I,J и фиксированного f, comap_map_le выражает неравенство между (I.map f).comap f и I.

LaTeX

$$(I.map f).comap f ≤ I$$

Lean4

theorem le_map_comap : J ≤ (J.comap f).map f :=
  (map_gc f).le_u_l J

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

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

Разделы

Аффилиация

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