lift₃NatTrans

Mathlib.CategoryTheory.Localization.Trifunctor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Localization.lift₃NatTrans

Lean4

/-- The natural transformation `F₁' ⟶ F₂'` of trifunctors induced by a
natural transformation `τ : F₁ ⟶ F₂` when `Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₁ F₁'`
and `Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ F₂ F₂'` hold. -/
noncomputable def lift₃NatTrans : F₁' ⟶ F₂' :=
  fullyFaithfulUncurry₃.preimage
    (liftNatTrans (L₁.prod (L₂.prod L₃)) (W₁.prod (W₂.prod W₃)) (uncurry₃.obj F₁) (uncurry₃.obj F₂) (uncurry₃.obj F₁')
      (uncurry₃.obj F₂') (uncurry₃.map τ))

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

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

Разделы

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

Аффилиация

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