functorOfNatTransEq

Mathlib.CategoryTheory.Endofunctor.Algebra

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Endofunctor.Algebra.functorOfNatTransEq

Lean4

/-- If `α` and `β` are two equal natural transformations, then the functors of algebras induced by them
are isomorphic.
We define it like this as opposed to using `eq_to_iso` so that the components are nicer to prove
lemmas about.
-/
@[simps!]
def functorOfNatTransEq {F G : C ⥤ C} {α β : F ⟶ G} (h : α = β) : functorOfNatTrans α ≅ functorOfNatTrans β :=
  NatIso.ofComponents fun X => isoMk (Iso.refl _)

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

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

Разделы

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

Аффилиация

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