mapRightEq

Mathlib.CategoryTheory.Comma.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comma.mapRightEq

Lean4

/-- Two equal natural transformations `R₁ ⟶ R₂` yield naturally isomorphic functors
`Comma L R₁ ⥤ Comma L R₂`. -/
@[simps!]
def mapRightEq (r r' : R₁ ⟶ R₂) (h : r = r') : mapRight L r ≅ mapRight L r' :=
  NatIso.ofComponents (fun X => isoMk (Iso.refl _) (Iso.refl _))

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

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

Разделы

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

Аффилиация

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