homOfLE_ι

Mathlib.AlgebraicGeometry.Restrict

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.homOfLE_ι

← MathLib Explorer

English

If U ≤ V, then the restriction morphism X.homOfLE e factors through V.ι.

Русский

Если U ⊆ V, тогдa ограничивающий морфизм x.homOfLE факtorизуется через V.ι.

LaTeX

$$$ X.homOfLE e ≫ V.ι = U.ι $$$

Lean4

@[reassoc (attr := simp)]
theorem homOfLE_ι (X : Scheme.{u}) {U V : X.Opens} (e : U ≤ V) : X.homOfLE e ≫ V.ι = U.ι :=
  IsOpenImmersion.lift_fac _ _ _

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

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

Разделы

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

Аффилиация

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