instIsDominantιCoborderRange

Mathlib.AlgebraicGeometry.Morphisms.Immersion

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsDominantιCoborderRange

English

If f is an immersion, then the morphism coborderRange f → Y is dominant (its image is dense in Y).

Русский

Если f — вложение, то coborderRange f → Y доминирует (образ плотен в Y).

LaTeX

$$$\\text{IsDominant}(\\text{coborderRange}(f).\\ι)$$$

Lean4

instance [IsImmersion f] : IsDominant f.coborderRange.ι :=
  by
  rw [isDominant_iff, DenseRange, Scheme.Opens.range_ι]
  exact dense_coborder

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

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

Разделы

Аффилиация

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