isLeftDerivedFunctor_iff_isRightKanExtension

English

The η-facilitated factorization of derivedη commutes with applying F' after α and unit at G.

Русский

Разложение через derivedη совместимо с применением F' после α и единицы на G.

LaTeX

$$$$ G'.map (\\beta.app X_2) \\; \\ggg \\; (\\operatorname{derivedη}_{W_1, α, β}^{}) .app (L_1.obj X_1) = α.app (F.obj X_2) \\; \\ggg \\; L_1.map(\\mathrm{unit}.app X_2). $$$$

Lean4

theorem isLeftDerivedFunctor_iff_isRightKanExtension [L.IsLocalization W] :
    LF.IsLeftDerivedFunctor α W ↔ LF.IsRightKanExtension α :=
  by
  constructor
  · exact fun _ => IsLeftDerivedFunctor.isRightKanExtension LF α W
  · exact fun h => ⟨h⟩

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