fromGlued_open_immersion

Mathlib.AlgebraicGeometry.Gluing

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.Cover.fromGlued_open_immersion

English

FromGlued is an open immersion via glue data (simplicially stated).

Русский

FromGlued является открытым вложением через данные склейки (упрощенно).

LaTeX

$$$$ \text{FromGlued is open immersion}. $$$$

Lean4

instance fromGlued_open_immersion : IsOpenImmersion 𝒰.fromGlued :=
  IsOpenImmersion.of_stalk_iso _ 𝒰.fromGlued_isOpenEmbedding

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

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

Разделы

Аффилиация

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