map_yonedaEquiv' — Mathlib

English

Variant of map YonedaEquiv with general g: maps through yonedaULift in opposite setting; equality F.map g (yonedaEquiv f) = f.val.app (Y) g.unop.

Русский

Вариант map YonedaEquiv с общим g: отображение через yonedaULift в противоположной установке; равенство F.map g (yonedaEquiv f) = f.val.app (Y) g.unop.

LaTeX

$$$F.map\ g (J.yonedaEquiv\ f) = f.val.app\ Y\ g.unop$$$

Lean4

/-- Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
can avoid the "motive is not type correct" error.
-/
theorem map_yonedaEquiv' {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) = f.val.app Y g.unop := by
  rw [yonedaEquiv_naturality', yonedaEquiv_comp, yonedaEquiv_yoneda_map]

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