descOfIsLeftKanExtension_fac — Mathlib

English

The universal property of the left Kan extension gives a factorization: α followed by the whiskerLeft of F'.descOfIsLeftKanExtension α G β equals β.

Русский

Универсальное свойство левого канонического расширения задаёт факторизацию: α затем whiskerLeft L (F'.descOfIsLeftKanExtension α G β) равны β.

LaTeX

$$$ \\alpha \\circ \\mathrm{whiskerLeft}\\ L\\ (F'.IsLeftKanExtension α) \\mathrm{fac} \\ (G,\\beta) = \\beta$$$

Lean4

@[reassoc (attr := simp)]
theorem descOfIsLeftKanExtension_fac (G : D ⥤ H) (β : F ⟶ L ⋙ G) :
    α ≫ whiskerLeft L (F'.descOfIsLeftKanExtension α G β) = β :=
  (F'.isUniversalOfIsLeftKanExtension α).fac (LeftExtension.mk G β)

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