subschemeι_apply — Mathlib

English

Let I be an ideal sheaf data on a scheme X. For the inclusion I.subscheme → X, the base map on a point x ∈ I.subscheme is just the underlying point in X; i.e., the inclusion on points is the projection to the first coordinate.

Русский

Пусть I — данные идеала sheaf на схеме X. Включение I.subscheme → X на точке x ∈ I.subscheme даёт ту же точку в X; то есть отображение на точках соответствует проекции на первый компонент.

LaTeX

$$$\forall x \in I.subscheme,\ I.subschemeι.base(x) = x.1$$$

Lean4

theorem subschemeι_apply (x : I.subscheme) : I.subschemeι.base x = x.1 :=
  rfl

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