compHom

Mathlib.AlgebraicGeometry.RationalMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.PartialMap.compHom

Lean4

/-- The composition of a partial map and a morphism on the right. -/
@[simps]
def compHom (f : X.PartialMap Y) (g : Y ⟶ Z) : X.PartialMap Z
    where
  domain := f.domain
  dense_domain := f.dense_domain
  hom := f.hom ≫ g

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

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

Разделы

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

Аффилиация

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