instOfIsEmptyCarrierCarrierCommRingCat

Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.IsClosedImmersion.instOfIsEmptyCarrierCarrierCommRingCat

← MathLib Explorer

English

If X is empty, any morphism f: X → Y is a ClosedImmersion.

Русский

Если X пусто, любой морфизм f: X → Y является закрытым вложением.

LaTeX

$$$X\text{ empty} \Rightarrow IsClosedImmersion f$$$

Lean4

instance (priority := low) {X Y : Scheme.{u}} [IsEmpty X] (f : X ⟶ Y) : IsClosedImmersion f :=
  .of_isPreimmersion _ (by rw [Set.range_eq_empty]; exact isClosed_empty)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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