mkHom

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cofork.mkHom

Lean4

/-- Helper function for constructing morphisms between coequalizer coforks.
-/
@[simps]
def mkHom {s t : Cofork f g} (k : s.pt ⟶ t.pt) (w : s.π ≫ k = t.π) : s ⟶ t
    where
  hom := k
  w := by
    rintro ⟨_ | _⟩
    · simp [Cofork.app_zero_eq_comp_π_left, w]
    · exact w

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

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

Разделы

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

Аффилиация

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