stalk_iso

Mathlib.Geometry.RingedSpace.OpenImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.stalk_iso

English

There is a canonical IsIso instance for each stalk map in an open immersion.

Русский

Существуют канонические инстансы IsIso для каждого stalk map в открытом вложении.

LaTeX

$$$IsIso(f.stalkMap(x))\quad \text{for all } x$$$

Lean4

instance stalk_iso (x : X) : IsIso (f.stalkMap x) :=
  PresheafedSpace.IsOpenImmersion.stalk_iso f.1 x

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

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

Разделы

Аффилиация

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