instIsZariskiLocalAtTargetDiagonalScheme

Mathlib.AlgebraicGeometry.Morphisms.Constructors

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsZariskiLocalAtTargetDiagonalScheme

← MathLib Explorer

English

If P has IsZariskiLocalAtTarget, then P.diagonal has IsZariskiLocalAtTarget.

Русский

Если P обладает свойством IsZariskiLocalAtTarget, то диагональ P.diagonal тоже локальна по Zariski на целевой схеме.

LaTeX

$$IsZariskiLocalAtTarget(P.diagonal)$$

Lean4

instance (P) [IsZariskiLocalAtTarget P] : IsZariskiLocalAtTarget P.diagonal :=
  letI := HasAffineProperty.of_isZariskiLocalAtTarget P
  inferInstance

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

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

Разделы

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

Аффилиация

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