ΓRestrictAlgebra

Mathlib.AlgebraicGeometry.Restrict

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.ΓRestrictAlgebra

English

The stalk isomorphism is defined by restricting along the open immersion.

Русский

Изоморфизм сталков определяется ограничением вдоль открытого вложения.

LaTeX

$$$ U.stalkIso x : U.toScheme.presheaf.stalk x \\cong X.presheaf.stalk x.1 $$$

Lean4

instance ΓRestrictAlgebra {X : Scheme.{u}} (U : X.Opens) : Algebra (Γ(X, ⊤)) Γ(U, ⊤) :=
  U.ι.appTop.hom.toAlgebra

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

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

Разделы

Аффилиация

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