liftOfIsRightKanExtension_fac — Mathlib

English

A universal lifting property holds: whiskerLeft L composed with F'.liftOfIsRightKanExtension α G β equals β.

Русский

Универсальное свойство подъема: композиция слева по L с F'.liftOfIsRightKanExtension α G β равна β.

LaTeX

$$$ \\mathrm{whiskerLeft}\,L\, (F'.liftOfIsRightKanExtension\, α\, G\, β) \\; \\circ \\; α = β$$$

Lean4

@[reassoc (attr := simp)]
theorem liftOfIsRightKanExtension_fac (G : D ⥤ H) (β : L ⋙ G ⟶ F) :
    whiskerLeft L (F'.liftOfIsRightKanExtension α G β) ≫ α = β :=
  (F'.isUniversalOfIsRightKanExtension α).fac (RightExtension.mk G β)

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