instIsOverHomOfLE

Mathlib.AlgebraicGeometry.Restrict

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

English

For any inclusions U ≤ V, the morphism X.homOfLE e is over X, i.e., it is a morphism of subschemes over X.

Русский

При любой вложенности U ≤ V морфизм X.homOfLE e является над X, т.е. морфизм подсхем над X.

LaTeX

$$$ X.homOfLE e \\text{ IsOver } X $$$

Lean4

instance {U V : X.Opens} (h : U ≤ V) : (X.homOfLE h).IsOver X where

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

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

Разделы

Аффилиация

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