instIsOpenImmersionTrans

Mathlib.AlgebraicGeometry.Cover.Directed

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.OpenCover.instIsOpenImmersionTrans

English

For an open cover 𝒰, each glue morphism between components is an open immersion.

Русский

Для открытого покрытия 𝒰 все согласующие морфизмы являются открытыми вложениями.

LaTeX

$$$\forall i, 𝒰.f i\; \text{открыто вложение}$$$

Lean4

instance {i j : 𝒰.I₀} (f : i ⟶ j) : IsOpenImmersion (𝒰.trans f) :=
  𝒰.property_trans f

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

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

Разделы

Аффилиация

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