restrict

Mathlib.AlgebraicGeometry.Morphisms.Basic

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsZariskiLocalAtTarget.restrict

English

For IsZariskiLocalAtTarget P, P(f) is equivalent to P on all components of an open cover.

Русский

Для IsZariskiLocalAtTarget P, P(f) эквивалентно P на всех компонентах открытого покрытия.

LaTeX

$$$P(f) \\iff (\\forall i, P(f|_{U_i}))$$$

Lean4

theorem restrict (hf : P f) (U : Y.Opens) : P (f ∣_ U) :=
  of_isPullback (isPullback_morphismRestrict f U).flip hf

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

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

Разделы

Аффилиация

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