yonedaEquiv_naturality' — Mathlib

English

Variant of Yoneda Naturality with a more general g; states the same naturality in a broader setting: F.map g (yonedaEquiv f) = yonedaEquiv (yoneda.map g.unop ≫ f).

Русский

Вариант натуральности Янеда с более общим g; сохраняет ту же зависимость: F.map g (yonedaEquiv f) = yonedaEquiv (yoneda.map g.unop ≫ f).

LaTeX

$$$F.map\ g\ (J.yonedaEquiv\ f) = J.yonedaEquiv\ (J.yoneda.map\ g.unop \gg f)$$$

Lean4

/-- Variant of `yonedaEquiv_naturality` with general `g`. This is technically strictly more general
than `yonedaEquiv_naturality`, but `yonedaEquiv_naturality` is sometimes preferable because it
can avoid the "motive is not type correct" error.
-/
theorem yonedaEquiv_naturality' {X Y : Cᵒᵖ} {F : Sheaf J (Type v)} (f : J.yoneda.obj (unop X) ⟶ F) (g : X ⟶ Y) :
    F.val.map g (J.yonedaEquiv f) = J.yonedaEquiv (J.yoneda.map g.unop ≫ f) :=
  J.yonedaEquiv_naturality _ _

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