comp

Mathlib.CategoryTheory.Category.Factorisation

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Factorisation.Hom.comp

Lean4

/-- Composition of morphisms in `Factorisation f`. -/
@[simps]
protected def comp {d₁ d₂ d₃ : Factorisation f} (f : Factorisation.Hom d₁ d₂) (g : Factorisation.Hom d₂ d₃) :
    Factorisation.Hom d₁ d₃ where
  h := f.h ≫ g.h
  ι_h := by rw [← Category.assoc, f.ι_h, g.ι_h]
  h_π := by rw [Category.assoc, g.h_π, f.h_π]

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

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

Разделы

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

Аффилиация

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