descOfIsLeftKanExtension_fac_app — Mathlib

English

At the level of components, α.app X followed by the component at L.obj X of F'.descOfIsLeftKanExtension α G β equals β.app X.

Русский

На уровне компонент α.app X и компонент у F'.descOfIsLeftKanExtension α G β на L.obj X равны β.app X.

LaTeX

$$$ \\alpha.\\mathrm{app}\\ X \\circ (F'.descOfIsLeftKanExtension α G β).app (L.obj X) = β.\\mathrm{app}\\ X$$$

Lean4

@[reassoc (attr := simp)]
theorem descOfIsLeftKanExtension_fac_app (G : D ⥤ H) (β : F ⟶ L ⋙ G) (X : C) :
    α.app X ≫ (F'.descOfIsLeftKanExtension α G β).app (L.obj X) = β.app X :=
  NatTrans.congr_app (F'.descOfIsLeftKanExtension_fac α G β) X

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