mkPrecomp

Mathlib.CategoryTheory.Comma.StructuredArrow.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CostructuredArrow.mkPrecomp

Lean4

/-- Variant of `homMk'` where both objects are applications of `mk`. -/
@[simps]
def mkPrecomp (f : S.obj Y ⟶ T) (g : Y' ⟶ Y) : mk (S.map g ≫ f) ⟶ mk f
    where
  left := g
  right := 𝟙 _

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

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

Разделы

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

Аффилиация

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