rightDerived_fac — Mathlib

English

For any G and β, the externalization of the right derived descendant along α with respect to G yields that α app X equals β app X after passing through the rightDerivedDesc.

Русский

Для каждого G и β, правая производнаяDescAlong α по отношению к G согласуется таким образом, что α.appX = β.appX через rightDerivedDesc.

LaTeX

$$[G: D ⥤ H], [β: F ⟶ L ⋙ G] : α.app X ≫ (RF.rightDerivedDesc α W G β).app (L.obj X) = β.app X$$

Lean4

@[reassoc (attr := simp)]
theorem rightDerived_fac (G : D ⥤ H) (β : F ⟶ L ⋙ G) : α ≫ whiskerLeft L (RF.rightDerivedDesc α W G β) = β :=
  have := IsRightDerivedFunctor.isLeftKanExtension RF α W
  RF.descOfIsLeftKanExtension_fac α G β

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