ofNatTrans

Mathlib.CategoryTheory.SmallObject.Iteration.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SmallObject.SuccStruct.ofNatTrans

Lean4

/-- Given a functor `Φ : C ⥤ C`, a natural transformation of the form `𝟭 C ⟶ Φ`
induces a successor structure on `C ⥤ C`. -/
@[simps]
def ofNatTrans {F : C ⥤ C} (ε : 𝟭 C ⟶ F) : SuccStruct (C ⥤ C)
    where
  succ G := G ⋙ F
  toSucc G := Functor.whiskerLeft G ε
  X₀ := 𝟭 C

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

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

Разделы

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

Аффилиация

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