transformObjComp

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

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

Lean4

/-- The construction `CatCommSqOver.transform` respects vertical composition
of `CatCospanTransform`s. -/
@[simps!]
def transformObjComp (X : Type u₁₀) [Category.{v₁₀} X] (ψ : CatCospanTransform F G F₁ G₁)
    (ψ' : CatCospanTransform F₁ G₁ F₂ G₂) :
    (transform X).obj (ψ.comp ψ') ≅ (transform X).obj ψ ⋙ (transform X).obj ψ' :=
  NatIso.ofComponents fun _ => CategoricalPullback.mkIso (Functor.associator _ _ _).symm (Functor.associator _ _ _).symm

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

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

Разделы

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

Аффилиация

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