isoOfEq_inv_ι

Mathlib.AlgebraicGeometry.Restrict

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

← MathLib Explorer

English

If U = V inside a scheme X, then the inverse of X.isoOfEq e composed with U.ι equals V.ι.

Русский

Если U = V внутри схемы X, то (X.isoOfEq e).inv ∘ U.ι = V.ι.

LaTeX

$$$(X.isoOfEq e).inv \\circ U.\\iota = V.\\iota$$$

Lean4

@[reassoc (attr := simp)]
theorem isoOfEq_inv_ι (X : Scheme.{u}) {U V : X.Opens} (e : U = V) : (X.isoOfEq e).inv ≫ U.ι = V.ι :=
  IsOpenImmersion.isoOfRangeEq_inv_fac _ _ _

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

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

Разделы

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

Аффилиация

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