precomp₂

Mathlib.CategoryTheory.Functor.KanExtension.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.LeftExtension.precomp₂

Lean4

/-- A variant of `LeftExtension.precomp` where we precompose, and then
"whisker" the diagram by a given natural transformation `(α : F₀ ⟶ L ⋙ F₁)` -/
@[simps!]
def precomp₂ {F₀ : C ⥤ H} {L : C ⥤ D} {F₁ : D ⥤ H} (L' : D ⥤ D') (α : F₀ ⟶ L ⋙ F₁) :
    L'.LeftExtension F₁ ⥤ (L ⋙ L').LeftExtension F₀ :=
  LeftExtension.precomp L' F₁ L ⋙ StructuredArrow.map α

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

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

Разделы

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

Аффилиация

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