compHom

Mathlib.AlgebraicGeometry.RationalMap

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

Lean4

/-- The composition of a rational map and a morphism on the right. -/
def compHom (f : X ⤏ Y) (g : Y ⟶ Z) : X ⤏ Z :=
  by
  refine Quotient.map (PartialMap.compHom · g) ?_ f
  intro f₁ f₂ ⟨W, hW, hWl, hWr, e⟩
  refine ⟨W, hW, hWl, hWr, ?_⟩
  simp only [PartialMap.restrict_domain, PartialMap.restrict_hom, PartialMap.compHom_domain,
    PartialMap.compHom_hom] at e ⊢
  rw [reassoc_of% e]

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

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

Разделы

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

Аффилиация

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