map_yonedaULiftEquiv — Mathlib

English

Variant of map yonedaEquiv in the opposite category; equality with unop g.unop.

Русский

Вариант map yonedaEquiv в противоположной категории; равенство с unop g.unop.

LaTeX

$$$F.map g (J.yonedaULiftEquiv f) = f.val.app (op Y) ⟨g.unop⟩$$$

Lean4

/-- See also `map_yonedaEquiv'` for a more general version. -/
theorem map_yonedaULiftEquiv {X Y : C} {F : Sheaf J (Type (max v v'))} (f : J.yonedaULift.obj X ⟶ F) (g : Y ⟶ X) :
    F.val.map g.op (J.yonedaULiftEquiv f) = f.val.app (op Y) ⟨g⟩ := by
  rw [yonedaULiftEquiv_naturality, yonedaULiftEquiv_comp, yonedaULiftEquiv_yonedaULift_map]

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