mk' — Mathlib

English

Given RF IsRightDerivedFunctor α W, we can construct a right derived functor for F: HasRightDerivedFunctor F W.

Русский

При наличии RF IsRightDerivedFunctor α W можно сконструировать правое производное функторa для F: HasRightDerivedFunctor F W.

LaTeX

$$HasRightDerivedFunctor F W$$

Lean4

theorem mk' [RF.IsRightDerivedFunctor α W] : HasRightDerivedFunctor F W :=
  by
  have := IsRightDerivedFunctor.isLeftKanExtension RF α W
  simpa only [hasRightDerivedFunctor_iff F L W] using HasLeftKanExtension.mk RF α

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