isLimitConeOfAdj

Mathlib.CategoryTheory.Limits.HasLimits

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

Lean4

/-- The cones defined by `coneOfAdj` are limit cones. -/
@[simps]
def isLimitConeOfAdj (F : J ⥤ C) : IsLimit (coneOfAdj adj F)
    where
  lift s := adj.homEquiv _ _ s.π
  fac s
    j := by
    have eq := NatTrans.congr_app (adj.counit.naturality s.π) j
    have eq' := NatTrans.congr_app (adj.left_triangle_components s.pt) j
    dsimp at eq eq' ⊢
    rw [adj.homEquiv_unit, assoc, eq, reassoc_of% eq']
  uniq s m hm := (adj.homEquiv _ _).symm.injective (by ext j; simpa using hm j)

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

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

Разделы

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

Аффилиация

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