toScheme_presheaf_obj

Mathlib.AlgebraicGeometry.Restrict

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Opens.toScheme_presheaf_obj

English

For an open U ⊆ X, the range of ι matches U itself.

Русский

Для открытого подмножества U диапазон ι совпадает с U.

LaTeX

$$U.ι.opensRange = U$$

Lean4

theorem toScheme_presheaf_obj (V) : Γ(U, V) = Γ(X, U.ι ''ᵁ V) :=
  rfl

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

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

Разделы

Аффилиация

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