instIsDominantCompScheme

Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.instIsDominantCompScheme

English

If f: X → Y and g: Y → Z are dominant, then their composition f ≫ g is dominant.

Русский

Если f: X → Y и g: Y → Z доминируют, то композиция f ≫ g доминирует.

LaTeX

$$$\\mathrm{IsDominant}(f \\circ g)$$$

Lean4

instance [IsDominant f] [IsDominant g] : IsDominant (f ≫ g) :=
  ⟨g.denseRange.comp f.denseRange g.base.hom.2⟩

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

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

Разделы

Аффилиация

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