hasPointwiseRightDerivedFunctorAt_iff_of_mem

English

Let F be a functor and W a morphism- property on C. For any X, Y and a morphism w: X → Y with w ∈ W, the pointwise right derived functor condition for F at X holds if and only if it holds at Y.

Русский

Пусть F — функтор, W — свойство морфизмов в C. Для любых объектов X, Y и морфизма w: X → Y, если w принадлежит W, то условие существования точечного правого полученного функторы для F в точке X эквивалентно условию в точке Y.

LaTeX

$$$\mathrm{HasPointwiseRightDerivedFunctorAt}(F,W,X) \iff \mathrm{HasPointwiseRightDerivedFunctorAt}(F,W,Y)$$$

Lean4

theorem hasPointwiseRightDerivedFunctorAt_iff_of_mem {X Y : C} (w : X ⟶ Y) (hw : W w) :
    F.HasPointwiseRightDerivedFunctorAt W X ↔ F.HasPointwiseRightDerivedFunctorAt W Y :=
  by
  simp only [F.hasPointwiseRightDerivedFunctorAt_iff W.Q W]
  exact hasPointwiseLeftKanExtensionAt_iff_of_iso W.Q F (Localization.isoOfHom W.Q W w hw)

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