leftDerived_fac — Mathlib

English

If G is a functor D ⥤ H and β : L ⋙ G ⟶ F, then whiskerLeft L (LF.leftDerivedLift α W G β) followed by α equals β after applying L.

Русский

Если G : D ⥤ H и β : L ⋙ G ⟶ F, то после отбивки слева по L и затем применения α получаем β.

LaTeX

$$$$ \\mathrm{whiskerLeft}\; L\\; (\\mathrm{LF.leftDerivedLift}\\; α\\; W\\; G\\; β) \\; \\; \\; \\; \\; \\; \\; ∘ α = β. $$$$

Lean4

@[reassoc (attr := simp)]
theorem leftDerived_fac (G : D ⥤ H) (β : L ⋙ G ⟶ F) : whiskerLeft L (LF.leftDerivedLift α W G β) ≫ α = β :=
  have := IsLeftDerivedFunctor.isRightKanExtension LF α W
  LF.liftOfIsRightKanExtension_fac α G β

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