e

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e

Lean4

/-- The structure isomorphism of a `CatCommSqOver` as a natural transformation. -/
abbrev e : fstFunctor F G X ⋙ (whiskeringRight X A B).obj F ≅ sndFunctor F G X ⋙ (whiskeringRight X C B).obj G :=
  NatIso.ofComponents (fun S ↦ S.iso)

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

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

Разделы

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

Аффилиация

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