yonedaULiftEquiv_symm_app_apply — Mathlib

English

Symmetry naturality on the right: J.yonedaEquiv.symm x ≫ f = J.yonedaEquiv.symm (f.val.app ⟨X⟩ x).

Русский

Симметрия натуральности справа: J.yonedaEquiv.symm x ≫ f = J.yonedaEquiv.symm (f.val.app ⟨X⟩ x).

LaTeX

$$$J.yonedaEquiv.symm x \;\; \gg f = J.yonedaEquiv.symm (f.\val.app \ { unop := X } x)$$$

Lean4

@[simp]
theorem yonedaULiftEquiv_symm_app_apply {X : C} {F : Sheaf J (Type (max v v'))} (x : F.val.obj (op X)) (Y : Cᵒᵖ)
    (f : Y.unop ⟶ X) : (J.yonedaULiftEquiv.symm x).val.app Y ⟨f⟩ = F.val.map f.op x :=
  rfl

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