instIsOpenImmersionToGlued

Mathlib.AlgebraicGeometry.Sites.Representability

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.LocalRepresentability.instIsOpenImmersionToGlued

English

For each i, the glue map from X_i to the glued object is an open immersion.

Русский

Для каждого i отображение toGlued hf i : X_i → Glued является открытым вложением.

LaTeX

$$$\\operatorname{IsOpenImmersion}(toGlued\\;hf\\;i)$$$

Lean4

instance : IsOpenImmersion (toGlued hf i) :=
  inferInstanceAs (IsOpenImmersion ((glueData hf).ι i))

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

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

Разделы

Аффилиация

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